:: RUSUB_4 semantic presentation begin theorem :: RUSUB_4:1 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rusub_3 :::"Lin"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rusub_3 :::"Lin"::: ) (Set (Var "B")))))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "w")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_rusub_3 :::"Lin"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) ")" ))))) ; theorem :: RUSUB_4:2 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#g1_bhsp_1 :::"UNITSTR"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_bhsp_1 :::"scalar"::: ) "of" (Set (Var "V"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k1_rusub_3 :::"Lin"::: ) (Set (Var "A")))) & (Bool (Set (Var "B")) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) )) "holds" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A")))) & (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "B")) ")" ))) & (Bool (Set ($#g1_bhsp_1 :::"UNITSTR"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_bhsp_1 :::"scalar"::: ) "of" (Set (Var "V"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k1_rusub_3 :::"Lin"::: ) (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ))) ")" )) ")" ))) ; definitionlet "V" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); attr "V" is :::"finite-dimensional"::: means :: RUSUB_4:def 1 (Bool "ex" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "V" "st" (Bool (Set (Var "A")) "is" ($#m1_rusub_3 :::"Basis"::: ) "of" "V")); end; :: deftheorem defines :::"finite-dimensional"::: RUSUB_4:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v1_rusub_4 :::"finite-dimensional"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "A")) "is" ($#m1_rusub_3 :::"Basis"::: ) "of" (Set (Var "V")))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_algstr_0 :::"left_complementable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) bbbadV9_RLVECT_1() ($#v1_bhsp_1 :::"strict"::: ) ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) ($#v1_rusub_4 :::"finite-dimensional"::: ) for ($#l1_bhsp_1 :::"UNITSTR"::: ) ; end; theorem :: RUSUB_4:3 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "st" (Bool (Bool (Set (Var "V")) "is" ($#v1_rusub_4 :::"finite-dimensional"::: ) )) "holds" (Bool "for" (Set (Var "I")) "being" ($#m1_rusub_3 :::"Basis"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Var "I")) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; theorem :: RUSUB_4:4 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v1_rusub_4 :::"finite-dimensional"::: ) ) & (Bool (Set (Var "A")) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; theorem :: RUSUB_4:5 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_rusub_3 :::"Basis"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v1_rusub_4 :::"finite-dimensional"::: ) )) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "B")))))) ; theorem :: RUSUB_4:6 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool (Set ($#k1_rusub_1 :::"(0)."::: ) (Set (Var "V"))) "is" ($#v1_rusub_4 :::"finite-dimensional"::: ) )) ; theorem :: RUSUB_4:7 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v1_rusub_4 :::"finite-dimensional"::: ) )) "holds" (Bool (Set (Var "W")) "is" ($#v1_rusub_4 :::"finite-dimensional"::: ) ))) ; registrationlet "V" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_algstr_0 :::"left_complementable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) bbbadV9_RLVECT_1() ($#v1_bhsp_1 :::"strict"::: ) ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) ($#v1_rusub_4 :::"finite-dimensional"::: ) for ($#m1_rusub_1 :::"Subspace"::: ) "of" "V"; end; registrationlet "V" be ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::); cluster -> ($#v1_rusub_4 :::"finite-dimensional"::: ) for ($#m1_rusub_1 :::"Subspace"::: ) "of" "V"; end; registrationlet "V" be ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_algstr_0 :::"left_complementable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) bbbadV9_RLVECT_1() ($#v1_bhsp_1 :::"strict"::: ) ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) ($#v1_rusub_4 :::"finite-dimensional"::: ) for ($#m1_rusub_1 :::"Subspace"::: ) "of" "V"; end; begin definitionlet "V" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); assume (Bool (Set (Const "V")) "is" ($#v1_rusub_4 :::"finite-dimensional"::: ) ) ; func :::"dim"::: "V" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: RUSUB_4:def 2 (Bool "for" (Set (Var "I")) "being" ($#m1_rusub_3 :::"Basis"::: ) "of" "V" "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "I"))))); end; :: deftheorem defines :::"dim"::: RUSUB_4:def 2 : (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) "st" (Bool (Bool (Set (Var "V")) "is" ($#v1_rusub_4 :::"finite-dimensional"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "I")) "being" ($#m1_rusub_3 :::"Basis"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "I"))))) ")" ))); theorem :: RUSUB_4:8 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V")))))) ; theorem :: RUSUB_4:9 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) )) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rusub_4 :::"dim"::: ) (Set "(" ($#k1_rusub_3 :::"Lin"::: ) (Set (Var "A")) ")" ))))) ; theorem :: RUSUB_4:10 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rusub_4 :::"dim"::: ) (Set "(" ($#k2_rusub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" )))) ; theorem :: RUSUB_4:11 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W")))) "iff" (Bool (Set ($#k2_rusub_1 :::"(Omega)."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rusub_1 :::"(Omega)."::: ) (Set (Var "W")))) ")" ))) ; theorem :: RUSUB_4:12 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool "(" (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set ($#k2_rusub_1 :::"(Omega)."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rusub_1 :::"(0)."::: ) (Set (Var "V")))) ")" )) ; theorem :: RUSUB_4:13 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool "(" (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set ($#k2_rusub_1 :::"(Omega)."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rusub_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) ")" )) ")" )) ; theorem :: RUSUB_4:14 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds" (Bool "(" (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Num 2)) "iff" (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#v1_rlvect_3 :::"linearly-independent"::: ) ) & (Bool (Set ($#k2_rusub_1 :::"(Omega)."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rusub_3 :::"Lin"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k7_domain_1 :::"}"::: ) ))) ")" )) ")" )) ; theorem :: RUSUB_4:15 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k1_rusub_4 :::"dim"::: ) (Set "(" (Set (Var "W1")) ($#k1_rusub_2 :::"+"::: ) (Set (Var "W2")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_rusub_4 :::"dim"::: ) (Set "(" (Set (Var "W1")) ($#k2_rusub_2 :::"/\"::: ) (Set (Var "W2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W2")) ")" ))))) ; theorem :: RUSUB_4:16 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set "(" (Set (Var "W1")) ($#k2_rusub_2 :::"/\"::: ) (Set (Var "W2")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set "(" ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V")) ")" ))))) ; theorem :: RUSUB_4:17 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rusub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W2")) ")" ))))) ; begin theorem :: RUSUB_4:18 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V")))) "iff" (Bool "ex" (Set (Var "W")) "being" ($#v1_bhsp_1 :::"strict"::: ) ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ")" )))) ; definitionlet "V" be ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "n" :::"Subspaces_of"::: "V" -> ($#m1_hidden :::"set"::: ) means :: RUSUB_4:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "W")) "being" ($#v1_bhsp_1 :::"strict"::: ) ($#m1_rusub_1 :::"Subspace"::: ) "of" "V" "st" (Bool "(" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) "n") ")" )) ")" )); end; :: deftheorem defines :::"Subspaces_of"::: RUSUB_4:def 3 : (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_rusub_4 :::"Subspaces_of"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "W")) "being" ($#v1_bhsp_1 :::"strict"::: ) ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )) ")" )) ")" )))); theorem :: RUSUB_4:19 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V"))))) "holds" (Bool "not" (Bool (Set (Set (Var "n")) ($#k2_rusub_4 :::"Subspaces_of"::: ) (Set (Var "V"))) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: RUSUB_4:20 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k1_rusub_4 :::"dim"::: ) (Set (Var "V"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "n")) ($#k2_rusub_4 :::"Subspaces_of"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: RUSUB_4:21 (Bool "for" (Set (Var "V")) "being" ($#v1_rusub_4 :::"finite-dimensional"::: ) ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k2_rusub_4 :::"Subspaces_of"::: ) (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "n")) ($#k2_rusub_4 :::"Subspaces_of"::: ) (Set (Var "V"))))))) ; begin definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "S" is :::"Affine"::: means :: RUSUB_4:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) "S"))); end; :: deftheorem defines :::"Affine"::: RUSUB_4:def 4 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_rusub_4 :::"Affine"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))) ")" ))); theorem :: RUSUB_4:22 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) "holds" (Bool "(" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "V"))) "is" ($#v2_rusub_4 :::"Affine"::: ) ) & (Bool (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "V"))) "is" ($#v2_rusub_4 :::"Affine"::: ) ) ")" )) ; theorem :: RUSUB_4:23 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v2_rusub_4 :::"Affine"::: ) ))) ; registrationlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V"))); cluster ($#v1_xboole_0 :::"empty"::: ) ($#v2_rusub_4 :::"Affine"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V"))); end; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "W" be ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"Up"::: "W" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: RUSUB_4:def 5 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W"); end; :: deftheorem defines :::"Up"::: RUSUB_4:def 5 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_rusub_4 :::"Up"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))))); definitionlet "V" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "W" be ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"Up"::: "W" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: RUSUB_4:def 6 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W"); end; :: deftheorem defines :::"Up"::: RUSUB_4:def 6 : (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rusub_4 :::"Up"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))))); theorem :: RUSUB_4:24 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k3_rusub_4 :::"Up"::: ) (Set (Var "W"))) "is" ($#v2_rusub_4 :::"Affine"::: ) ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))) ")" ))) ; theorem :: RUSUB_4:25 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "S" is :::"Subspace-like"::: means :: RUSUB_4:def 7 (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) "V") ($#r2_hidden :::"in"::: ) "S") & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "S")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) "S") ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Subspace-like"::: RUSUB_4:def 7 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_rusub_4 :::"Subspace-like"::: ) ) "iff" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" )) ")" ) ")" ) ")" ))); theorem :: RUSUB_4:26 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_rusub_4 :::"Subspace-like"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set (Var "A")) ")" ))) ")" ))) ; theorem :: RUSUB_4:27 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_rusub_4 :::"Up"::: ) (Set (Var "W"))) "is" ($#v3_rusub_4 :::"Subspace-like"::: ) ))) ; theorem :: RUSUB_4:28 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_rusub_3 :::"Lin"::: ) (Set (Var "A")) ")" ))))) ; theorem :: RUSUB_4:29 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rusub_4 :::"Up"::: ) (Set (Var "W"))) "is" ($#v3_rusub_4 :::"Subspace-like"::: ) ))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "M" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); let "v" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); func "v" :::"+"::: "M" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: RUSUB_4:def 8 "{" (Set "(" "v" ($#k1_algstr_0 :::"+"::: ) (Set (Var "u")) ")" ) where u "is" ($#m1_subset_1 :::"Element":::) "of" "V" : (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "M") "}" ; end; :: deftheorem defines :::"+"::: RUSUB_4:def 8 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "u")) ")" ) where u "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) : (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) "}" )))); theorem :: RUSUB_4:30 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_rusub_4 :::"Up"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "v")) ($#k3_rlsub_1 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M")))))))) ; theorem :: RUSUB_4:31 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M"))) "is" ($#v2_rusub_4 :::"Affine"::: ) )))) ; theorem :: RUSUB_4:32 (Bool "for" (Set (Var "V")) "being" ($#l1_bhsp_1 :::"RealUnitarySpace":::) (Bool "for" (Set (Var "W")) "being" ($#v1_bhsp_1 :::"strict"::: ) ($#m1_rusub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k4_rusub_4 :::"Up"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "v")) ($#k3_rusub_1 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M")))))))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "M", "N" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func "M" :::"+"::: "N" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: RUSUB_4:def 9 "{" (Set "(" (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v")) ")" ) where u, v "is" ($#m1_subset_1 :::"Element":::) "of" "V" : (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "M") & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) "N") ")" ) "}" ; end; :: deftheorem defines :::"+"::: RUSUB_4:def 9 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "M")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v")) ")" ) where u, v "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) : (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) ")" ) "}" ))); definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "M", "N" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); :: original: :::"+"::: redefine func "M" :::"+"::: "N" -> ($#m1_subset_1 :::"Subset":::) "of" "V"; commutativity (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")) "holds" (Bool (Set (Set (Var "M")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k6_rusub_4 :::"+"::: ) (Set (Var "M"))))) ; end; theorem :: RUSUB_4:33 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ($#k6_rusub_4 :::"+"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_rusub_4 :::"+"::: ) (Set (Var "M"))))))) ; theorem :: RUSUB_4:34 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "M")) "being" ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ($#k7_rusub_4 :::"+"::: ) (Set (Var "M"))) "is" ($#v2_rusub_4 :::"Affine"::: ) )))) ; theorem :: RUSUB_4:35 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "N"))) "is" ($#v2_rusub_4 :::"Affine"::: ) ))) ; theorem :: RUSUB_4:36 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#v2_rusub_4 :::"Affine"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "M")) ($#k7_rusub_4 :::"+"::: ) (Set (Var "N"))) "is" ($#v2_rusub_4 :::"Affine"::: ) ))) ;