List of theorems referencing the symbol DOT_PROD

(173) Theorem 134: [Cartesian product with a null set] (N •PROD 0 = 0) & (0 •PROD N = 0)
(174) Theorem 135: [Members of Cartesian products] (X in (S •PROD T)) •imp ((car(X) in S) & (cdr(X) in T))
(175) Theorem 136: [Subsets of Cartesian products] (Y •incin (S •PROD T)) •eq (Is_map(Y) & (domain(Y) •incin S) & (range(Y) •incin T))
(176) Theorem 137: [Image of Cartesian product by a singleton] (U in Z) •imp (((Z •PROD {V})~[U]) = V)
(177) Theorem 138: [Cartesian product disjointness] (A * B = 0) •imp ((X •PROD A) * (Y •PROD B) = 0)
(178) Theorem 139: [Cartesian modified associativity] (F = {[[[x,y],z],[x,[y,z]]]: x in A, y in B, z in C}) •imp (one_1_map(F) & (domain(F) = ((A •PROD B) •PROD C)) & (range(F) = (A •PROD (B •PROD C))))
(179) Theorem 140: [Cartesian modified commutativity] (F = {[[x,y],[y,x]]: x in A, y in B}) •imp (one_1_map(F) & (domain(F) = (A •PROD B)) & (range(F) = (B •PROD A)))
(194) Theorem 155: [Associative Law for Cardinals] #((A •PROD B) •PROD C) = #(A •PROD (B •PROD C))
(195) Theorem 156: [Commutative Law for Cardinals] #(A •PROD B) = #(B •PROD A)
(262) Theorem 216: [Cardinality of Cartesian product by a singleton, 2] #({C} •PROD N) = #N
(263) Theorem 217: [Cardinality of Cartesian product by a singleton, 3] #(N •PROD {C}) = #N
(264) Theorem 218: [Cardinality of a Cartesian product union] (A /= B) •imp (#N •PLUS #M = #((N •PROD {A}) + (M •PROD {B})))
(271) Theorem 225: [Arithmetic multiplication lemma 3] #(N •PROD M) = #(#N •PROD #M)
(272) Theorem 226: [Arithmetic multiplication lemma 4] #(N •PROD M) = #(N •PROD #M)
(273) Theorem 227: [Arithmetic multiplication lemma 5] #(N •PROD M) = #(#N •PROD M)
(289) Theorem 242: [Monotonicity of multiplication] (M /= 0) •imp (#(N •PROD M) incs #N)
(290) Theorem 243: [Distributivity lemma] (A /= B) •imp (N •PLUS M = #((N •PROD {A}) + (M •PROD {B})))
(294) Theorem 247: [Rules for intersection and union of Cartesian products] ((A •PROD X) * (B •PROD X) = (A * B) •PROD X) & ((A •PROD X) + (B •PROD X) = (A + B) •PROD X) & (((X •PROD A) * (X •PROD B)) = X •PROD (A * B)) & (((X •PROD A) + (X •PROD B)) = X •PROD (A + B))
(295) Theorem 248: [Cartesian product monotonicity] ((A •incin B) & (C •incin D)) •imp ((A •PROD C) •incin (B •PROD D))
(296) Theorem 249: [Intersection of Cartesian products] ((A •PROD C) * (B •PROD D) = (A * B) •PROD (C * D))
(301) Theorem 254: [The Cartesian product of two finite sets is finite] (Finite(N) & Finite(M)) •imp Finite(N •PROD M)
(387) Theorem subseq.3: Svm(g) & (g •incin (domain(f) •PROD range(f))) & (domain(g) in (next(Za) * next(domain(f))))
(425) Theorem product_order_1: [The first component of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(car(X))
(426) Theorem product_order_2: [The second component of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(cdr(X))
(427) Theorem product_order_3: [The maximum of the components of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(car(X) + cdr(X))
(428) Theorem product_order_4: ((X in o1 •PROD o2) & (Y in o1 •PROD o2)) •imp ((Ord1p2_thryvar(X,Y) or Ord1p2_thryvar(Y,X) or X = Y) & (not Ord1p2_thryvar(X,X)))
(429) Theorem product_order_5: ((X in o1 •PROD o2) & (Y in o1 •PROD o2) & (Z in o1 •PROD o2) & Ord1p2_thryvar(X,Y) & Ord1p2_thryvar(Y,Z)) •imp Ord1p2_thryvar(X,Z)
(430) Theorem product_order_6: ((T •incin (o1 •PROD o2)) & (T /= 0)) •imp (EXISTS x in T | (FORALL y in t | (Ord1p2_thryvar(x,y) or (x = y))))
(435) Theorem 342: [The cardinality of a non-null Cartesian product is at least the cardinality of its first factor] (T /= 0) •imp (#S •incin #(S •PROD T))
(436) Theorem 343: (Ord(O1) & Ord(O2)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f), y in domain(f) | (x in y) •eq (((car(f~[x]) + cdr(f~[x])) in (car(f~[y]) + cdr(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) in car(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) = car(f~[y])) & (cdr(f~[x]) in cdr(f~[y]))))))
(437) Theorem 344: (Card(O1) & Card(O2) & (not Finite(O1 + O2))) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f) | (EXISTS y in (O1 + O2) | range(f •ON x) •incin (y •PROD y))))
(438) Theorem 345: [Cardinal Doubling Theorem] (not Finite(S)) •imp (#(S •PROD {0,1}) = #S)
(441) Theorem 348: [Cardinal Square Theorem] (not Finite(S)) •imp (#(S •PROD S) = #S)
(675) Theorem 524: (X in Ra) •imp ((Za •PROD {X}) in RaCauchy)
(676) Theorem 525: (X in Ra) •imp (Ras_ABS(Za •PROD {X}) = (Za •PROD {Ra_ABS(X)}))
(855) Theorem 702: (X in Ra) •imp (Ra_is_nonneg(X) •eq Ra_eqseq(Za •PROD {Ra_ABS(X)},Za •PROD {X}))
(856) Theorem 703: (X in Ra) •imp (R_is_nonneg(Cauchy_to_Re(Za •PROD {X})) •eq (ReRa(Ra_ABS(X)) = ReRa(X)))
(914) Theorem 759: (BoundedClosedRe(S) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T})) & (FORALL ends in T | ends in (Re •PROD Re))) •imp (EXISTS T1 | (T1 •incin T) & Finite(T1) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T1})))