:: PRVECT_1 semantic presentation begin theorem :: PRVECT_1:1 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "G"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "G"))))) ; theorem :: PRVECT_1:2 (Bool "for" (Set (Var "G")) "being" ($#l2_algstr_0 :::"AbGroup":::) "holds" (Bool (Set ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "G"))) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "G"))))) ; theorem :: PRVECT_1:3 (Bool "for" (Set (Var "GS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "GS"))) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "GS"))) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "GS"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "GS")))) & (Bool (Set ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "GS"))) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "GS"))))) "holds" (Bool (Set (Var "GS")) "is" ($#l2_algstr_0 :::"AbGroup":::))) ; theorem :: PRVECT_1:4 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "F"))))) ; theorem :: PRVECT_1:5 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "F"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "F"))))) ; begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "x", "y" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "D"))); :: original: :::".:"::: redefine func "F" :::".:"::: "(" "x" "," "y" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D"); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "n" be ($#m1_hidden :::"Nat":::); func :::"product"::: "(" "F" "," "n" ")" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D" ")" ) means :: PRVECT_1:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_prvect_1 :::".:"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))); end; :: deftheorem defines :::"product"::: PRVECT_1:def 1 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_prvect_1 :::"product"::: ) "(" (Set (Var "F")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) "holds" (Bool (Set (Set (Var "b4")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_prvect_1 :::".:"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) ")" ))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "D")); let "n" be ($#m1_hidden :::"Nat":::); func :::"product"::: "(" "F" "," "n" ")" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D" ")" ) means :: PRVECT_1:def 2 (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k4_finseqop :::"*"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"product"::: PRVECT_1:def 2 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_prvect_1 :::"product"::: ) "(" (Set (Var "F")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_finseqop :::"*"::: ) (Set (Var "x"))))) ")" ))))); theorem :: PRVECT_1:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set ($#k2_prvect_1 :::"product"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ) "is" ($#v1_binop_1 :::"commutative"::: ) )))) ; theorem :: PRVECT_1:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set ($#k2_prvect_1 :::"product"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ) "is" ($#v2_binop_1 :::"associative"::: ) )))) ; theorem :: PRVECT_1:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k2_prvect_1 :::"product"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" )))))) ; theorem :: PRVECT_1:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "C")) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k3_prvect_1 :::"product"::: ) "(" (Set (Var "C")) "," (Set (Var "n")) ")" ) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set ($#k2_prvect_1 :::"product"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" )))))) ; begin definitionlet "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); assume (Bool "(" (Bool (Set (Const "F")) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set (Const "F")) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set (Const "F")) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set (Const "F")) "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) ")" ) ; func "n" :::"-Group_over"::: "F" -> ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"AbGroup":::) equals :: PRVECT_1:def 3 (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ")" ) "," (Set "(" ($#k2_prvect_1 :::"product"::: ) "(" (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "F") "," "n" ")" ")" ) "," (Set "(" "n" ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "F" ")" ) ")" ) "#)" ); end; :: deftheorem defines :::"-Group_over"::: PRVECT_1:def 3 : (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set (Var "F")) "is" ($#v13_algstr_0 :::"right_complementable"::: ) )) "holds" (Bool (Set (Set (Var "n")) ($#k4_prvect_1 :::"-Group_over"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ")" ) "," (Set "(" ($#k2_prvect_1 :::"product"::: ) "(" (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "F"))) "," (Set (Var "n")) ")" ")" ) "," (Set "(" (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ")" ) "#)" )))); registrationlet "F" be ($#l2_algstr_0 :::"AbGroup":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k4_prvect_1 :::"-Group_over"::: ) "F") -> ($#v8_algstr_0 :::"strict"::: ) ; end; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_hidden :::"Nat":::); func "n" :::"-Mult_over"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") "," (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ")" ) means :: PRVECT_1:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "F" (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F")) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "F") ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" )))); end; :: deftheorem defines :::"-Mult_over"::: PRVECT_1:def 4 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_prvect_1 :::"-Mult_over"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "v")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F")))) "holds" (Bool (Set (Set (Var "b3")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "F"))) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" )))) ")" )))); definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_hidden :::"Nat":::); func "n" :::"-VectSp_over"::: "F" -> ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "F" means :: PRVECT_1:def 5 (Bool "(" (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set "n" ($#k4_prvect_1 :::"-Group_over"::: ) "F")) & (Bool (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "n" ($#k5_prvect_1 :::"-Mult_over"::: ) "F")) ")" ); end; :: deftheorem defines :::"-VectSp_over"::: PRVECT_1:def 5 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_prvect_1 :::"-VectSp_over"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b3"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "b3"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_prvect_1 :::"-Group_over"::: ) (Set (Var "F")))) & (Bool (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_prvect_1 :::"-Mult_over"::: ) (Set (Var "F")))) ")" ) ")" )))); registrationlet "F" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k6_prvect_1 :::"-VectSp_over"::: ) "F") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_vectsp_1 :::"strict"::: ) ; end; theorem :: PRVECT_1:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "D"))) "st" (Bool (Bool (Set (Var "H")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "H")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" (Set (Var "G")) ($#k1_prvect_1 :::".:"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "H")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "t1")) ")" ")" ) "," (Set "(" (Set (Var "H")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "t2")) ")" ")" ) ")" ))))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "v" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "D"))); :: original: :::"[;]"::: redefine func "F" :::"[;]"::: "(" "x" "," "v" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D"); end; registrationlet "F" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k6_prvect_1 :::"-VectSp_over"::: ) "F") -> ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ; end; begin definitionmode Domain-Sequence is ($#v2_relat_1 :::"non-empty"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinSequence":::); end; scheme :: PRVECT_1:sch 1 NEFinSeqLambda{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinSequence":::), F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set F1 "(" ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set F1 "(" ")" )) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "i")) ")" )) ")" ) ")" )) proof end; definitionlet "a" be ($#v2_relat_1 :::"non-empty"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Function":::); let "f" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set (Const "a"))); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "a"))); :: original: :::"."::: redefine func "f" :::"."::: "i" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "a" ($#k1_funct_1 :::"."::: ) "i"); end; begin definitionlet "a" be ($#v2_relat_1 :::"non-empty"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Function":::); mode :::"BinOps"::: "of" "a" -> ($#m1_hidden :::"Function":::) means :: PRVECT_1:def 6 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "a")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) "a") "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" "a" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ); mode :::"UnOps"::: "of" "a" -> ($#m1_hidden :::"Function":::) means :: PRVECT_1:def 7 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "a")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) "a") "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" "a" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"BinOps"::: PRVECT_1:def 6 : (Bool "for" (Set (Var "a")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set (Var "a"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ) ")" ))); :: deftheorem defines :::"UnOps"::: PRVECT_1:def 7 : (Bool "for" (Set (Var "a")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set (Var "a"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ) ")" ))); registrationlet "a" be ($#m1_hidden :::"Domain-Sequence":::); cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_prvect_1 :::"BinOps"::: ) "of" "a"; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m2_prvect_1 :::"UnOps"::: ) "of" "a"; end; theorem :: PRVECT_1:11 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set (Var "a"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ) ")" ))) ; theorem :: PRVECT_1:12 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set (Var "a"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ")" ) ")" ) ")" ))) ; definitionlet "a" be ($#m1_hidden :::"Domain-Sequence":::); let "b" be ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set (Const "a")); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "a"))); :: original: :::"."::: redefine func "b" :::"."::: "i" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" "a" ($#k1_funct_1 :::"."::: ) "i" ")" ); end; definitionlet "a" be ($#m1_hidden :::"Domain-Sequence":::); let "u" be ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set (Const "a")); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "a"))); :: original: :::"."::: redefine func "u" :::"."::: "i" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" "a" ($#k1_funct_1 :::"."::: ) "i" ")" ); end; theorem :: PRVECT_1:13 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "d")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "a")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set (Var "a"))) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set "(" (Set (Var "d")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "d9")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))))) ")" )) "holds" (Bool (Set (Var "d")) ($#r2_funct_2 :::"="::: ) (Set (Var "d9"))))) ; theorem :: PRVECT_1:14 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "u")) "being" ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set (Var "a")) "holds" (Bool "(" (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k3_funct_6 :::"rngs"::: ) (Set (Var "u")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "a")))) ")" ))) ; definitionlet "a" be ($#m1_hidden :::"Domain-Sequence":::); let "u" be ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set (Const "a")); :: original: :::"Frege"::: redefine func :::"Frege"::: "u" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) "a" ")" ); end; theorem :: PRVECT_1:15 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "u")) "being" ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set (Var "a")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set (Var "a"))) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set "(" (Set "(" ($#k11_prvect_1 :::"Frege"::: ) (Set (Var "u")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "u")) ($#k10_prvect_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k8_prvect_1 :::"."::: ) (Set (Var "i")) ")" ))))))) ; definitionlet "F" be ($#v4_funct_1 :::"functional"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "F")); let "f", "g" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "F")); :: original: :::"."::: redefine func "b" :::"."::: "(" "f" "," "g" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "F"; end; theorem :: PRVECT_1:16 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "d")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "a")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set (Var "a"))) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set "(" (Set (Var "d")) ($#k12_prvect_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "d9")) ($#k12_prvect_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))))) ")" )) "holds" (Bool (Set (Var "d")) ($#r8_binop_1 :::"="::: ) (Set (Var "d9"))))) ; definitionlet "a" be ($#m1_hidden :::"Domain-Sequence":::); let "b" be ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set (Const "a")); func :::"[:":::"b":::":]"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) "a" ")" ) means :: PRVECT_1:def 8 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) "a") (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) "a") "holds" (Bool (Set (Set "(" it ($#k12_prvect_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "b" ($#k9_prvect_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k8_prvect_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "g")) ($#k8_prvect_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )))); end; :: deftheorem defines :::"[:"::: PRVECT_1:def 8 : (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "b")) "being" ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set (Var "a")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "a")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k13_prvect_1 :::"[:"::: ) (Set (Var "b")) ($#k13_prvect_1 :::":]"::: ) )) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set (Var "a"))) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set "(" (Set (Var "b3")) ($#k12_prvect_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k9_prvect_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k8_prvect_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "g")) ($#k8_prvect_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )))) ")" )))); theorem :: PRVECT_1:17 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "b")) "being" ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set (Var "a")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set (Var "b")) ($#k9_prvect_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_binop_1 :::"commutative"::: ) ) ")" )) "holds" (Bool (Set ($#k13_prvect_1 :::"[:"::: ) (Set (Var "b")) ($#k13_prvect_1 :::":]"::: ) ) "is" ($#v1_binop_1 :::"commutative"::: ) ))) ; theorem :: PRVECT_1:18 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "b")) "being" ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set (Var "a")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set (Var "b")) ($#k9_prvect_1 :::"."::: ) (Set (Var "i"))) "is" ($#v2_binop_1 :::"associative"::: ) ) ")" )) "holds" (Bool (Set ($#k13_prvect_1 :::"[:"::: ) (Set (Var "b")) ($#k13_prvect_1 :::":]"::: ) ) "is" ($#v2_binop_1 :::"associative"::: ) ))) ; theorem :: PRVECT_1:19 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "b")) "being" ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set (Var "a")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set (Var "a"))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set (Var "f")) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Set (Var "b")) ($#k9_prvect_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool (Set (Var "f")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k13_prvect_1 :::"[:"::: ) (Set (Var "b")) ($#k13_prvect_1 :::":]"::: ) ))))) ; theorem :: PRVECT_1:20 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Domain-Sequence":::) (Bool "for" (Set (Var "b")) "being" ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set (Var "a")) (Bool "for" (Set (Var "u")) "being" ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set (Var "a")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))) "holds" (Bool "(" (Bool (Set (Set (Var "u")) ($#k10_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set (Set (Var "b")) ($#k9_prvect_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "b")) ($#k9_prvect_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" ) ")" )) "holds" (Bool (Set ($#k11_prvect_1 :::"Frege"::: ) (Set (Var "u"))) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set ($#k13_prvect_1 :::"[:"::: ) (Set (Var "b")) ($#k13_prvect_1 :::":]"::: ) ))))) ; begin definitionlet "F" be ($#m1_hidden :::"Relation":::); attr "F" is :::"AbGroup-yielding"::: means :: PRVECT_1:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "F"))) "holds" (Bool (Set (Var "x")) "is" ($#l2_algstr_0 :::"AbGroup":::))); end; :: deftheorem defines :::"AbGroup-yielding"::: PRVECT_1:def 9 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_prvect_1 :::"AbGroup-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "x")) "is" ($#l2_algstr_0 :::"AbGroup":::))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_FINSET_1() ($#v4_card_3 :::"countable"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_prvect_1 :::"AbGroup-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode Group-Sequence is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_prvect_1 :::"AbGroup-yielding"::: ) ($#m1_hidden :::"FinSequence":::); end; definitionlet "g" be ($#m1_hidden :::"Group-Sequence":::); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "g"))); :: original: :::"."::: redefine func "g" :::"."::: "i" -> ($#l2_algstr_0 :::"AbGroup":::); end; definitionlet "g" be ($#m1_hidden :::"Group-Sequence":::); func :::"carr"::: "g" -> ($#m1_hidden :::"Domain-Sequence":::) means :: PRVECT_1:def 10 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "g")) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) "g") "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" "g" ($#k14_prvect_1 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"carr"::: PRVECT_1:def 10 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Group-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Domain-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k15_prvect_1 :::"carr"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g"))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "g")) ($#k14_prvect_1 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ) ")" ))); definitionlet "g" be ($#m1_hidden :::"Group-Sequence":::); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) (Set (Const "g")) ")" )); :: original: :::"."::: redefine func "g" :::"."::: "i" -> ($#l2_algstr_0 :::"AbGroup":::); end; definitionlet "g" be ($#m1_hidden :::"Group-Sequence":::); func :::"addop"::: "g" -> ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set ($#k15_prvect_1 :::"carr"::: ) "g") means :: PRVECT_1:def 11 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) "g" ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) "g" ")" )) "holds" (Bool (Set it ($#k9_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" "g" ($#k16_prvect_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); func :::"complop"::: "g" -> ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set ($#k15_prvect_1 :::"carr"::: ) "g") means :: PRVECT_1:def 12 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) "g" ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) "g" ")" )) "holds" (Bool (Set it ($#k10_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_funct_2 :::"="::: ) (Set ($#k5_vectsp_1 :::"comp"::: ) (Set "(" "g" ($#k16_prvect_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); func :::"zeros"::: "g" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) "g" ")" )) means :: PRVECT_1:def 13 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) "g" ")" )) "holds" (Bool (Set it ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" "g" ($#k16_prvect_1 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"addop"::: PRVECT_1:def 11 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Group-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_prvect_1 :::"BinOps"::: ) "of" (Set ($#k15_prvect_1 :::"carr"::: ) (Set (Var "g"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k17_prvect_1 :::"addop"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) (Set (Var "g")) ")" )) "holds" (Bool (Set (Set (Var "b2")) ($#k9_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_funct_2 :::"="::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" (Set (Var "g")) ($#k16_prvect_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"complop"::: PRVECT_1:def 12 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Group-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_prvect_1 :::"UnOps"::: ) "of" (Set ($#k15_prvect_1 :::"carr"::: ) (Set (Var "g"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k18_prvect_1 :::"complop"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) (Set (Var "g")) ")" )) "holds" (Bool (Set (Set (Var "b2")) ($#k10_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_funct_2 :::"="::: ) (Set ($#k5_vectsp_1 :::"comp"::: ) (Set "(" (Set (Var "g")) ($#k16_prvect_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"zeros"::: PRVECT_1:def 13 : (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Group-Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) (Set (Var "g")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k19_prvect_1 :::"zeros"::: ) (Set (Var "g")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) (Set (Var "g")) ")" )) "holds" (Bool (Set (Set (Var "b2")) ($#k8_prvect_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" (Set (Var "g")) ($#k16_prvect_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" ))); definitionlet "G" be ($#m1_hidden :::"Group-Sequence":::); func :::"product"::: "G" -> ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"AbGroup":::) equals :: PRVECT_1:def 14 (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) "G" ")" ) ")" ) "," (Set ($#k13_prvect_1 :::"[:"::: ) (Set "(" ($#k17_prvect_1 :::"addop"::: ) "G" ")" ) ($#k13_prvect_1 :::":]"::: ) ) "," (Set "(" ($#k19_prvect_1 :::"zeros"::: ) "G" ")" ) "#)" ); end; :: deftheorem defines :::"product"::: PRVECT_1:def 14 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"Group-Sequence":::) "holds" (Bool (Set ($#k20_prvect_1 :::"product"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" ($#k15_prvect_1 :::"carr"::: ) (Set (Var "G")) ")" ) ")" ) "," (Set ($#k13_prvect_1 :::"[:"::: ) (Set "(" ($#k17_prvect_1 :::"addop"::: ) (Set (Var "G")) ")" ) ($#k13_prvect_1 :::":]"::: ) ) "," (Set "(" ($#k19_prvect_1 :::"zeros"::: ) (Set (Var "G")) ")" ) "#)" )));