:: ANPROJ_1 semantic presentation begin definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "p", "q" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); pred :::"are_Prop"::: "p" "," "q" means :: ANPROJ_1:def 1 (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) "p") ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) "q")) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); reflexivity (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; symmetry (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")) "st" (Bool (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) "holds" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; end; :: deftheorem defines :::"are_Prop"::: ANPROJ_1:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "q"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ))); theorem :: ANPROJ_1:1 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "q"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")))) ")" )) ")" ))) ; theorem :: ANPROJ_1:2 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "u")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "u"))) & (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "q")))) "holds" (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "q"))))) ; theorem :: ANPROJ_1:3 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) "iff" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "u", "v", "w" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); pred "u" "," "v" "," "w" :::"are_LinDep"::: means :: ANPROJ_1:def 2 (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) "u" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) "v" ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) "w" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "V")) & (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )); end; :: deftheorem defines :::"are_LinDep"::: ANPROJ_1:def 2 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ")" ))); theorem :: ANPROJ_1:4 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "u1")) "," (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "w")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "u1"))) & (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "v")) "," (Set (Var "v1"))) & (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "w")) "," (Set (Var "w1"))) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) "holds" (Bool (Set (Var "u1")) "," (Set (Var "v1")) "," (Set (Var "w1")) ($#r2_anproj_1 :::"are_LinDep"::: ) ))) ; theorem :: ANPROJ_1:5 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) "holds" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "u")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "w")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" ))) ; theorem :: ANPROJ_1:6 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "v")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "w")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "v")) "," (Set (Var "w"))))) "holds" (Bool "(" (Bool (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))) ")" ))) ; theorem :: ANPROJ_1:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "q")))) & (Bool (Set (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ))) & (Bool (Bool "not" (Set (Var "p")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "q")) "is" ($#v9_struct_0 :::"zero"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )))) ; theorem :: ANPROJ_1:8 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "c2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))) ")" )))) ; theorem :: ANPROJ_1:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "q")))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "q")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a1")) ($#k8_real_1 :::"*"::: ) (Set (Var "b2")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "a2")) ($#k8_real_1 :::"*"::: ) (Set (Var "b1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "p")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "q")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "v")))) & (Bool (Bool "not" (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))))) ; theorem :: ANPROJ_1:10 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) "or" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" )) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) ))) ; theorem :: ANPROJ_1:11 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "v"))) "or" (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "w")) "," (Set (Var "u"))) "or" (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "v")) "," (Set (Var "w"))) ")" )) "holds" (Bool (Set (Var "w")) "," (Set (Var "u")) "," (Set (Var "v")) ($#r2_anproj_1 :::"are_LinDep"::: ) ))) ; theorem :: ANPROJ_1:12 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) ))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "u")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "v")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "w")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "v")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "v")) "," (Set (Var "w")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "w")) "," (Set (Var "u")))) ")" ))) ; theorem :: ANPROJ_1:13 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "q"))))) ; theorem :: ANPROJ_1:14 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "q")))) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "u")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "v")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Bool "not" (Set (Var "p")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "q")) "is" ($#v9_struct_0 :::"zero"::: ) ))) "holds" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) ))) ; theorem :: ANPROJ_1:15 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "p")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "q")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Bool "not" (Set (Var "y")) "is" ($#v9_struct_0 :::"zero"::: ) )) ")" )))) ; theorem :: ANPROJ_1:16 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "q")))) & (Bool (Bool "not" (Set (Var "p")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "q")) "is" ($#v9_struct_0 :::"zero"::: ) ))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "y")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "y")))) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "v")) "," (Set (Var "y")))) ")" ))))) ; theorem :: ANPROJ_1:17 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r2_anproj_1 :::"are_LinDep"::: ) ))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "u")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "v")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "v"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "y")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) ")" ))))) ; theorem :: ANPROJ_1:18 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "q")) "," (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "q")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "q")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "p")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "v")) "," (Set (Var "y")) "," (Set (Var "p")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "u")) "," (Set (Var "y")) "," (Set (Var "r")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "r")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) & (Bool (Bool "not" (Set (Var "p")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "q")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "r")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) )) & (Bool (Bool "not" (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ))) "holds" (Bool (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) ($#r2_anproj_1 :::"are_LinDep"::: ) ))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"Proportionality_as_EqRel_of"::: "V" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "(" ($#k8_struct_0 :::"NonZero"::: ) "V" ")" ) means :: ANPROJ_1:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_struct_0 :::"NonZero"::: ) "V")) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k8_struct_0 :::"NonZero"::: ) "V")) & (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "v"))) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Proportionality_as_EqRel_of"::: ANPROJ_1:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "(" ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_anproj_1 :::"Proportionality_as_EqRel_of"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "V")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "V")))) & (Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "v"))) ")" )) ")" ) ")" )) ")" ))); theorem :: ANPROJ_1:19 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_anproj_1 :::"Proportionality_as_EqRel_of"::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V"))) & (Bool (Set (Var "y")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V"))) ")" ))) ; theorem :: ANPROJ_1:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_anproj_1 :::"Proportionality_as_EqRel_of"::: ) (Set (Var "V")))) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "u")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "v")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "u")) "," (Set (Var "v"))) ")" ) ")" ))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "v" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); func :::"Dir"::: "v" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_struct_0 :::"NonZero"::: ) "V" ")" ) equals :: ANPROJ_1:def 4 (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_anproj_1 :::"Proportionality_as_EqRel_of"::: ) "V" ")" ) "," "v" ")" ); end; :: deftheorem defines :::"Dir"::: ANPROJ_1:def 4 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_anproj_1 :::"Proportionality_as_EqRel_of"::: ) (Set (Var "V")) ")" ) "," (Set (Var "v")) ")" )))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"ProjectivePoints"::: "V" -> ($#m1_hidden :::"set"::: ) means :: ANPROJ_1:def 5 (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k8_struct_0 :::"NonZero"::: ) "V" ")" ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_anproj_1 :::"Proportionality_as_EqRel_of"::: ) "V" ")" ))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" )); end; :: deftheorem defines :::"ProjectivePoints"::: ANPROJ_1:def 5 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_anproj_1 :::"ProjectivePoints"::: ) (Set (Var "V")))) "iff" (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k8_struct_0 :::"NonZero"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_anproj_1 :::"Proportionality_as_EqRel_of"::: ) (Set (Var "V")) ")" ))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" )) ")" ))); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) bbbadV12_ALGSTR_0() bbbadV13_ALGSTR_0() ($#v1_rlvect_1 :::"strict"::: ) ($#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() for ($#l1_rlvect_1 :::"RLSStruct"::: ) ; end; registrationlet "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k3_anproj_1 :::"ProjectivePoints"::: ) "V") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ANPROJ_1:21 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) "is" ($#v9_struct_0 :::"zero"::: ) ))) "holds" (Bool (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "p"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_anproj_1 :::"ProjectivePoints"::: ) (Set (Var "V")))))) ; theorem :: ANPROJ_1:22 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "q")) "is" ($#v9_struct_0 :::"zero"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "q")))) "iff" (Bool ($#r1_anproj_1 :::"are_Prop"::: ) (Set (Var "p")) "," (Set (Var "q"))) ")" ))) ; definitionlet "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"ProjectiveCollinearity"::: "V" -> ($#m1_collsp :::"Relation3"::: ) "of" (Set ($#k3_anproj_1 :::"ProjectivePoints"::: ) "V") means :: ANPROJ_1:def 6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "p")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "q")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "r")))) & (Bool (Bool "not" (Set (Var "p")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "q")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "r")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" )) ")" )); end; :: deftheorem defines :::"ProjectiveCollinearity"::: ANPROJ_1:def 6 : (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_collsp :::"Relation3"::: ) "of" (Set ($#k3_anproj_1 :::"ProjectivePoints"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_anproj_1 :::"ProjectiveCollinearity"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "p")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "q")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "r")))) & (Bool (Bool "not" (Set (Var "p")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "q")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "r")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" )) ")" )) ")" ))); definitionlet "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"ProjectiveSpace"::: "V" -> ($#v1_collsp :::"strict"::: ) ($#l1_collsp :::"CollStr"::: ) equals :: ANPROJ_1:def 7 (Set ($#g1_collsp :::"CollStr"::: ) "(#" (Set "(" ($#k3_anproj_1 :::"ProjectivePoints"::: ) "V" ")" ) "," (Set "(" ($#k4_anproj_1 :::"ProjectiveCollinearity"::: ) "V" ")" ) "#)" ); end; :: deftheorem defines :::"ProjectiveSpace"::: ANPROJ_1:def 7 : (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#g1_collsp :::"CollStr"::: ) "(#" (Set "(" ($#k3_anproj_1 :::"ProjectivePoints"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k4_anproj_1 :::"ProjectiveCollinearity"::: ) (Set (Var "V")) ")" ) "#)" ))); registrationlet "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k5_anproj_1 :::"ProjectiveSpace"::: ) "V") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_collsp :::"strict"::: ) ; end; theorem :: ANPROJ_1:23 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_anproj_1 :::"ProjectivePoints"::: ) (Set (Var "V")))) & (Bool (Set "the" ($#u1_collsp :::"Collinearity"::: ) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_anproj_1 :::"ProjectiveCollinearity"::: ) (Set (Var "V")))) ")" )) ; theorem :: ANPROJ_1:24 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "st" (Bool (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_collsp :::"Collinearity"::: ) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" )))) "holds" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "p")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "q")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "r")))) & (Bool (Bool "not" (Set (Var "p")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "q")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "r")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" )))) ; theorem :: ANPROJ_1:25 (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "u")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "v")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Bool "not" (Set (Var "w")) "is" ($#v9_struct_0 :::"zero"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set "(" ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "u")) ")" ) "," (Set "(" ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "w")) ")" ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_collsp :::"Collinearity"::: ) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" ))) "iff" (Bool (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#r2_anproj_1 :::"are_LinDep"::: ) ) ")" ))) ; theorem :: ANPROJ_1:26 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_anproj_1 :::"ProjectiveSpace"::: ) (Set (Var "V")) ")" )) "iff" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Bool "not" (Set (Var "u")) "is" ($#v9_struct_0 :::"zero"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_anproj_1 :::"Dir"::: ) (Set (Var "u")))) ")" )) ")" ))) ;