Home | Metamath
Proof Explorer Theorem List (p. 401 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mapdcnvcl 40001 | Closure of the converse of the map defined by df-mapd 39974. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) β β’ (π β (β‘πβπ) β π) | ||
Theorem | mapdcl 40002 | Closure the value of the map defined by df-mapd 39974. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) β ran π) | ||
Theorem | mapdcnvid1N 40003 | Converse of the value of the map defined by df-mapd 39974. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (β‘πβ(πβπ)) = π) | ||
Theorem | mapdsord 40004 | Strong ordering property of themap defined by df-mapd 39974. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ) β (πβπ) β π β π)) | ||
Theorem | mapdcl2 40005 | The mapping of a subspace of vector space H is a subspace in the dual space of functionals with closed kernels. (Contributed by NM, 31-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (LSubSpβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ ) β π) | ||
Theorem | mapdcnvid2 40006 | Value of the converse of the map defined by df-mapd 39974. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) β β’ (π β (πβ(β‘πβπ)) = π) | ||
Theorem | mapdcnvordN 40007 | Ordering property of the converse of the map defined by df-mapd 39974. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β ((β‘πβπ) β (β‘πβπ) β π β π)) | ||
Theorem | mapdcnv11N 40008 | The converse of the map defined by df-mapd 39974 is one-to-one. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β ((β‘πβπ) = (β‘πβπ) β π = π)) | ||
Theorem | mapdcv 40009 | Covering property of the converse of the map defined by df-mapd 39974. (Contributed by NM, 14-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ π· = ((LCDualβπΎ)βπ) & β’ πΈ = ( βL βπ·) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (πβπ)πΈ(πβπ))) | ||
Theorem | mapdincl 40010 | Closure of dual subspace intersection for the map defined by df-mapd 39974. (Contributed by NM, 12-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β (π β© π) β ran π) | ||
Theorem | mapdin 40011 | Subspace intersection is preserved by the map defined by df-mapd 39974. Part of property (e) in [Baer] p. 40. (Contributed by NM, 12-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ(π β© π)) = ((πβπ) β© (πβπ))) | ||
Theorem | mapdlsmcl 40012 | Closure of dual subspace sum for the map defined by df-mapd 39974. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (LSSumβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β (π β π) β ran π) | ||
Theorem | mapdlsm 40013 | Subspace sum is preserved by the map defined by df-mapd 39974. Part of property (e) in [Baer] p. 40. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (LSSumβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ(π β π)) = ((πβπ) β (πβπ))) | ||
Theorem | mapd0 40014 | Projectivity map of the zero subspace. Part of property (f) in [Baer] p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ 0 = (0gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β (πβ{π}) = { 0 }) | ||
Theorem | mapdcnvatN 40015 | Atoms are preserved by the map defined by df-mapd 39974. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π΅ = (LSAtomsβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (β‘πβπ) β π΄) | ||
Theorem | mapdat 40016 | Atoms are preserved by the map defined by df-mapd 39974. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π΅ = (LSAtomsβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΄) β β’ (π β (πβπ) β π΅) | ||
Theorem | mapdspex 40017* | The map of a span equals the dual span of some vector (functional). (Contributed by NM, 15-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π΅ = (BaseβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β βπ β π΅ (πβ(πβ{π})) = (π½β{π})) | ||
Theorem | mapdn0 40018 | Transfer nonzero property from domain to range of projectivity mapd. (Contributed by NM, 12-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ 0 = (0gβπ) & β’ π = (0gβπΆ) & β’ (π β π β (π β { 0 })) β β’ (π β πΉ β (π· β {π})) | ||
Theorem | mapdncol 40019 | Transfer non-colinearity from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΊ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (π½β{πΉ}) β (π½β{πΊ})) | ||
Theorem | mapdindp 40020 | Transfer (part of) vector independence condition from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΊ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β π β π) & β’ (π β πΈ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΈ})) & β’ (π β Β¬ π β (πβ{π, π})) β β’ (π β Β¬ πΉ β (π½β{πΊ, πΈ})) | ||
Theorem | mapdpglem1 40021 | Lemma for mapdpg 40055. Baer p. 44, last line: "(F(x-y))* <= (Fx)*+(Fy)*." (Contributed by NM, 15-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) β β’ (π β (πβ(πβ{(π β π)})) β ((πβ(πβ{π})) β (πβ(πβ{π})))) | ||
Theorem | mapdpglem2 40022* | Lemma for mapdpg 40055. Baer p. 45, lines 1 and 2: "we have (F(x-y))* = Gt where t necessarily belongs to (Fx)*+(Fy)*." (We scope $d π‘π locally to avoid clashes with later substitutions into π.) (Contributed by NM, 15-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) β β’ (π β βπ‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))(πβ(πβ{(π β π)})) = (π½β{π‘})) | ||
Theorem | mapdpglem2a 40023* | Lemma for mapdpg 40055. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) β β’ (π β π‘ β πΉ) | ||
Theorem | mapdpglem3 40024* | Lemma for mapdpg 40055. Baer p. 45, line 3: "infer ... the existence of a number g in G and of an element z in (Fy)* such that t = gx'-z." (We scope $d ππ€π§π locally to avoid clashes with later substitutions into π.) (Contributed by NM, 18-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β βπ β π΅ βπ§ β (πβ(πβ{π}))π‘ = ((π Β· πΊ)π π§)) | ||
Theorem | mapdpglem4N 40025* | Lemma for mapdpg 40055. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (π β π) β π) | ||
Theorem | mapdpglem5N 40026* | Lemma for mapdpg 40055. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) β β’ (π β π‘ β (0gβπΆ)) | ||
Theorem | mapdpglem6 40027* | Lemma for mapdpg 40055. Baer p. 45, line 4: "If g were 0, then t would be in (Fy)*..." (Contributed by NM, 18-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π = 0 ) β β’ (π β π‘ β (πβ(πβ{π}))) | ||
Theorem | mapdpglem8 40028* | Lemma for mapdpg 40055. Baer p. 45, line 4: "...so that (F(x-y))* <= (Fy)*. This would imply that F(x-y) <= F(y)..." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π = 0 ) β β’ (π β (πβ{(π β π)}) β (πβ{π})) | ||
Theorem | mapdpglem9 40029* | Lemma for mapdpg 40055. Baer p. 45, line 4: "...so that x would consequently belong to Fy." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π = 0 ) β β’ (π β π β (πβ{π})) | ||
Theorem | mapdpglem10 40030* | Lemma for mapdpg 40055. Baer p. 45, line 6: "Hence Fx=Fy, an impossibility." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π = 0 ) β β’ (π β (πβ{π}) = (πβ{π})) | ||
Theorem | mapdpglem11 40031* | Lemma for mapdpg 40055. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) β β’ (π β π β 0 ) | ||
Theorem | mapdpglem12 40032* | Lemma for mapdpg 40055. TODO: Can some commonality with mapdpglem6 40027 through mapdpglem11 40031 be exploited? Also, some consolidation of small lemmas here could be done. (Contributed by NM, 18-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π§ = (0gβπΆ)) β β’ (π β π‘ β (πβ(πβ{π}))) | ||
Theorem | mapdpglem13 40033* | Lemma for mapdpg 40055. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π§ = (0gβπΆ)) β β’ (π β (πβ{(π β π)}) β (πβ{π})) | ||
Theorem | mapdpglem14 40034* | Lemma for mapdpg 40055. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π§ = (0gβπΆ)) β β’ (π β π β (πβ{π})) | ||
Theorem | mapdpglem15 40035* | Lemma for mapdpg 40055. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π§ = (0gβπΆ)) β β’ (π β (πβ{π}) = (πβ{π})) | ||
Theorem | mapdpglem16 40036* | Lemma for mapdpg 40055. Baer p. 45, line 7: "Likewise we see that z =/= 0." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π§ β (0gβπΆ)) | ||
Theorem | mapdpglem17N 40037* | Lemma for mapdpg 40055. Baer p. 45, line 7: "Hence we may form y' = g^-1 z." (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β πΈ β πΉ) | ||
Theorem | mapdpglem18 40038* | Lemma for mapdpg 40055. Baer p. 45, line 7: "Then y =/= 0..." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β πΈ β (0gβπΆ)) | ||
Theorem | mapdpglem19 40039* | Lemma for mapdpg 40055. Baer p. 45, line 8: "...is in (Fy)*..." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β πΈ β (πβ(πβ{π}))) | ||
Theorem | mapdpglem20 40040* | Lemma for mapdpg 40055. Baer p. 45, line 8: "...so that (Fy)*=Gy'." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β (πβ(πβ{π})) = (π½β{πΈ})) | ||
Theorem | mapdpglem21 40041* | Lemma for mapdpg 40055. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β (((invrβπ΄)βπ) Β· π‘) = (πΊπ πΈ)) | ||
Theorem | mapdpglem22 40042* | Lemma for mapdpg 40055. Baer p. 45, line 9: "(F(x-y))* = ... = G(x'-y')." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΊπ πΈ)})) | ||
Theorem | mapdpglem23 40043* | Lemma for mapdpg 40055. Baer p. 45, line 10: "and so y' meets all our requirements." Our β is Baer's y'. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β ββ β πΉ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)}))) | ||
Theorem | mapdpglem30a 40044 | Lemma for mapdpg 40055. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β πΊ β (0gβπΆ)) | ||
Theorem | mapdpglem30b 40045 | Lemma for mapdpg 40055. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) β β’ (π β π β (0gβπΆ)) | ||
Theorem | mapdpglem25 40046 | Lemma for mapdpg 40055. Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) β β’ (π β ((π½β{β}) = (π½β{π}) β§ (π½β{(πΊπ β)}) = (π½β{(πΊπ π)}))) | ||
Theorem | mapdpglem26 40047* | Lemma for mapdpg 40055. Baer p. 45 line 14: "Consequently there exist numbers u,v in G neither of which is 0 such that y = uy'' and..." (We scope $d π’π locally to avoid clashes with later substitutions into π.) (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) β β’ (π β βπ’ β (π΅ β {π})β = (π’ Β· π)) | ||
Theorem | mapdpglem27 40048* | Lemma for mapdpg 40055. Baer p. 45 line 16: "v(x'-y'') = x'-y'" (with equality swapped). (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) β β’ (π β βπ£ β (π΅ β {π})(πΊπ β) = (π£ Β· (πΊπ π))) | ||
Theorem | mapdpglem29 40049* | Lemma for mapdpg 40055. Baer p. 45 line 16: "But Gx' and Gy'' are distinct points and so x' and y'' are independent elements in B. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) & β’ (π β π£ β π΅) & β’ (π β β = (π’ Β· π)) & β’ (π β (πΊπ β) = (π£ Β· (πΊπ π))) β β’ (π β (π½β{πΊ}) β (π½β{π})) | ||
Theorem | mapdpglem28 40050* | Lemma for mapdpg 40055. Baer p. 45 line 18: "vx'-vy'' = x'-uy''". (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) & β’ (π β π£ β π΅) & β’ (π β β = (π’ Β· π)) & β’ (π β (πΊπ β) = (π£ Β· (πΊπ π))) β β’ (π β ((π£ Β· πΊ)π (π£ Β· π)) = (πΊπ (π’ Β· π))) | ||
Theorem | mapdpglem30 40051* | Lemma for mapdpg 40055. Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 40050, using lvecindp2 20523) that v = 1 and v = u...". TODO: would it be shorter to have only the π£ = (1rβπ΄) part and use mapdpglem28.u2 in mapdpglem31 40052? (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) & β’ (π β π£ β π΅) & β’ (π β β = (π’ Β· π)) & β’ (π β (πΊπ β) = (π£ Β· (πΊπ π))) & β’ (π β π’ β π΅) β β’ (π β (π£ = (1rβπ΄) β§ π£ = π’)) | ||
Theorem | mapdpglem31 40052* | Lemma for mapdpg 40055. Baer p. 45 line 19: "...and we have consequently that y' = y'', as we claimed." (Contributed by NM, 23-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) & β’ (π β π£ β π΅) & β’ (π β β = (π’ Β· π)) & β’ (π β (πΊπ β) = (π£ Β· (πΊπ π))) & β’ (π β π’ β π΅) β β’ (π β β = π) | ||
Theorem | mapdpglem24 40053* | Lemma for mapdpg 40055. Existence part - consolidate hypotheses in mapdpglem23 40043. (Contributed by NM, 21-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β ββ β πΉ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)}))) | ||
Theorem | mapdpglem32 40054* | Lemma for mapdpg 40055. Uniqueness part - consolidate hypotheses in mapdpglem31 40052. (Contributed by NM, 23-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ ((π β§ (β β πΉ β§ π β πΉ) β§ (((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})) β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) β β = π) | ||
Theorem | mapdpg 40055* | Part 1 of proof of the first fundamental theorem of projective geometry. Part (1) in [Baer] p. 44. Our notation corresponds to Baer's as follows: π for *, πβ{} for F(), π½β{} for G(), π for x, πΊ for x', π for y, β for y'. TODO: Rename variables per mapdhval 40073. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β β!β β πΉ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)}))) | ||
Theorem | baerlem3lem1 40056 | Lemma for baerlem3 40062. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π = ((π Β· π) + (π Β· π))) & β’ (π β π = ((π Β· (π β π)) + (π Β· (π β π)))) β β’ (π β π = (π Β· (π β π))) | ||
Theorem | baerlem5alem1 40057 | Lemma for baerlem5a 40063. (Contributed by NM, 13-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π = ((π Β· (π β π)) + (π Β· π))) & β’ (π β π = ((π Β· (π β π)) + (π Β· π))) β β’ (π β π = (π Β· (π β (π + π)))) | ||
Theorem | baerlem5blem1 40058 | Lemma for baerlem5b 40064. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π = ((π Β· π) + (π Β· π))) & β’ (π β π = ((π Β· (π β (π + π))) + (π Β· π))) β β’ (π β π = ((πΌβπ) Β· (π + π))) | ||
Theorem | baerlem3lem2 40059 | Lemma for baerlem3 40062. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) β β’ (π β (πβ{(π β π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β π)}) β (πβ{(π β π)})))) | ||
Theorem | baerlem5alem2 40060 | Lemma for baerlem5a 40063. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) β β’ (π β (πβ{(π β (π + π))}) = (((πβ{(π β π)}) β (πβ{π})) β© ((πβ{(π β π)}) β (πβ{π})))) | ||
Theorem | baerlem5blem2 40061 | Lemma for baerlem5b 40064. (Contributed by NM, 13-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) β β’ (π β (πβ{(π + π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π})))) | ||
Theorem | baerlem3 40062 | An equality that holds when π, π, π are independent (non-colinear) vectors. Part (3) in [Baer] p. 45. TODO fix ref. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) β β’ (π β (πβ{(π β π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β π)}) β (πβ{(π β π)})))) | ||
Theorem | baerlem5a 40063 | An equality that holds when π, π, π are independent (non-colinear) vectors. First equation of part (5) in [Baer] p. 46. (Contributed by NM, 10-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β (πβ{(π β (π + π))}) = (((πβ{(π β π)}) β (πβ{π})) β© ((πβ{(π β π)}) β (πβ{π})))) | ||
Theorem | baerlem5b 40064 | An equality that holds when π, π, π are independent (non-colinear) vectors. Second equation of part (5) in [Baer] p. 46. (Contributed by NM, 13-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β (πβ{(π + π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π})))) | ||
Theorem | baerlem5amN 40065 | An equality that holds when π, π, π are independent (non-colinear) vectors. Subtraction version of first equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 40067 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β (πβ{(π β (π β π))}) = (((πβ{(π β π)}) β (πβ{π})) β© ((πβ{(π + π)}) β (πβ{π})))) | ||
Theorem | baerlem5bmN 40066 | An equality that holds when π, π, π are independent (non-colinear) vectors. Subtraction version of second equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 40067 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β (πβ{(π β π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π β π))}) β (πβ{π})))) | ||
Theorem | baerlem5abmN 40067 | An equality that holds when π, π, π are independent (non-colinear) vectors. Subtraction versions of first and second equations of part (5) in [Baer] p. 46, conjoined to share commonality in their proofs. TODO: Delete if not needed. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β ((πβ{(π β (π β π))}) = (((πβ{(π β π)}) β (πβ{π})) β© ((πβ{(π + π)}) β (πβ{π}))) β§ (πβ{(π β π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π β π))}) β (πβ{π}))))) | ||
Theorem | mapdindp0 40068 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) & β’ (π β (π + π) β 0 ) β β’ (π β (πβ{(π + π)}) = (πβ{π})) | ||
Theorem | mapdindp1 40069 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πβ{π}) β (πβ{(π + π)})) | ||
Theorem | mapdindp2 40070 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β Β¬ π€ β (πβ{π, (π + π)})) | ||
Theorem | mapdindp3 40071 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πβ{π}) β (πβ{(π€ + π)})) | ||
Theorem | mapdindp4 40072 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β Β¬ π β (πβ{π, (π€ + π)})) | ||
Theorem | mapdhval 40073* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ (π β π β π΄) & β’ (π β πΉ β π΅) & β’ (π β π β πΈ) β β’ (π β (πΌββ¨π, πΉ, πβ©) = if(π = 0 , π, (β©β β π· ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ β)}))))) | ||
Theorem | mapdhval0 40074* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ 0 = (0gβπ) & β’ (π β π β π΄) & β’ (π β πΉ β π΅) β β’ (π β (πΌββ¨π, πΉ, 0 β©) = π) | ||
Theorem | mapdhval2 40075* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ (π β π β π΄) & β’ (π β πΉ β π΅) & β’ (π β π β (π β { 0 })) β β’ (π β (πΌββ¨π, πΉ, πβ©) = (β©β β π· ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ β)})))) | ||
Theorem | mapdhcl 40076* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β π) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) | ||
Theorem | mapdheq 40077* | Lemmma for ~? mapdh . The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 4-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β π·) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β ((πβ(πβ{π})) = (π½β{πΊ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ πΊ)})))) | ||
Theorem | mapdheq2 40078* | Lemmma for ~? mapdh . One direction of part (2) in [Baer] p. 45. (Contributed by NM, 4-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β π·) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β (πΌββ¨π, πΊ, πβ©) = πΉ)) | ||
Theorem | mapdheq2biN 40079* | Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 40078 seems to require an additional hypothesis not mentioned in Baer. TODO fix ref. TODO: We probably don't need this; delete if never used. (Contributed by NM, 4-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β π·) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β (πΌββ¨π, πΊ, πβ©) = πΉ)) | ||
Theorem | mapdheq4lem 40080* | Lemma for mapdheq4 40081. Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΊπ πΈ)})) | ||
Theorem | mapdheq4 40081* | Lemma for ~? mapdh . Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πΌββ¨π, πΊ, πβ©) = πΈ) | ||
Theorem | mapdh6lem1N 40082* | Lemma for mapdh6N 40096. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πβ(πβ{(π β (π + π))})) = (π½β{(πΉπ (πΊ β πΈ))})) | ||
Theorem | mapdh6lem2N 40083* | Lemma for mapdh6N 40096. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πβ(πβ{(π + π)})) = (π½β{(πΊ β πΈ)})) | ||
Theorem | mapdh6aN 40084* | Lemma for mapdh6N 40096. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6b0N 40085* | Lemmma for mapdh6N 40096. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ((πβ{π}) β© (πβ{π, π})) = { 0 }) β β’ (π β Β¬ π β (πβ{π, π})) | ||
Theorem | mapdh6bN 40086* | Lemmma for mapdh6N 40096. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π = 0 ) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6cN 40087* | Lemmma for mapdh6N 40096. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β π) & β’ (π β π = 0 ) & β’ (π β Β¬ π β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6dN 40088* | Lemmma for mapdh6N 40096. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π€ + (π + π))β©) = ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©))) | ||
Theorem | mapdh6eN 40089* | Lemmma for mapdh6N 40096. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, ((π€ + π) + π)β©) = ((πΌββ¨π, πΉ, (π€ + π)β©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6fN 40090* | Lemmma for mapdh6N 40096. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π€ + π)β©) = ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6gN 40091* | Lemmma for mapdh6N 40096. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©)) = (((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, πβ©)) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6hN 40092* | Lemmma for mapdh6N 40096. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6iN 40093* | Lemmma for mapdh6N 40096. Eliminate auxiliary vector π€. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6jN 40094* | Lemmma for mapdh6N 40096. Eliminate (πβ{π}) = (πβ{π}) hypothesis. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6kN 40095* | Lemmma for mapdh6N 40096. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6N 40096* | Part (6) of [Baer] p. 47 line 6. Note that we use Β¬ π β (πβ{π, π}) which is equivalent to Baer's "Fx β© (Fy + Fz)" by lspdisjb 20510. TODO: If disjoint variable conditions with πΌ and π become a problem later, use cbv* theorems on πΌ variables here to get rid of them. Maybe reorder hypotheses in lemmas to the more consistent order of this theorem, so they can be shared with this theorem. TODO: may be deleted (with its lemmas), if not needed, in view of hdmap1l6 40170. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh7eN 40097* | Part (7) of [Baer] p. 48 line 10 (5 of 6 cases). (Note: 1 of 6 and 2 of 6 are hypotheses a and b.) (Contributed by NM, 2-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π’})) = (π½β{πΉ})) & β’ (π β π’ β (π β { 0 })) & β’ (π β π£ β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π’}) β (πβ{π£})) & β’ (π β Β¬ π€ β (πβ{π’, π£})) & β’ (π β (πΌββ¨π’, πΉ, π€β©) = πΈ) β β’ (π β (πΌββ¨π€, πΈ, π’β©) = πΉ) | ||
Theorem | mapdh7cN 40098* | Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π’})) = (π½β{πΉ})) & β’ (π β π’ β (π β { 0 })) & β’ (π β π£ β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π’}) β (πβ{π£})) & β’ (π β Β¬ π€ β (πβ{π’, π£})) & β’ (π β (πΌββ¨π’, πΉ, π£β©) = πΊ) β β’ (π β (πΌββ¨π£, πΊ, π’β©) = πΉ) | ||
Theorem | mapdh7dN 40099* | Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π’})) = (π½β{πΉ})) & β’ (π β π’ β (π β { 0 })) & β’ (π β π£ β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π’}) β (πβ{π£})) & β’ (π β Β¬ π€ β (πβ{π’, π£})) & β’ (π β (πΌββ¨π’, πΉ, π£β©) = πΊ) & β’ (π β (πΌββ¨π’, πΉ, π€β©) = πΈ) β β’ (π β (πΌββ¨π£, πΊ, π€β©) = πΈ) | ||
Theorem | mapdh7fN 40100* | Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π’})) = (π½β{πΉ})) & β’ (π β π’ β (π β { 0 })) & β’ (π β π£ β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π’}) β (πβ{π£})) & β’ (π β Β¬ π€ β (πβ{π’, π£})) & β’ (π β (πΌββ¨π’, πΉ, π£β©) = πΊ) & β’ (π β (πΌββ¨π’, πΉ, π€β©) = πΈ) β β’ (π β (πΌββ¨π€, πΈ, π£β©) = πΊ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |