![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > mapdpglem25 | Structured version Visualization version GIF version |
Description: Lemma for mapdpg 41067. Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-Mar-2015.) |
Ref | Expression |
---|---|
mapdpg.h | β’ π» = (LHypβπΎ) |
mapdpg.m | β’ π = ((mapdβπΎ)βπ) |
mapdpg.u | β’ π = ((DVecHβπΎ)βπ) |
mapdpg.v | β’ π = (Baseβπ) |
mapdpg.s | β’ β = (-gβπ) |
mapdpg.z | β’ 0 = (0gβπ) |
mapdpg.n | β’ π = (LSpanβπ) |
mapdpg.c | β’ πΆ = ((LCDualβπΎ)βπ) |
mapdpg.f | β’ πΉ = (BaseβπΆ) |
mapdpg.r | β’ π = (-gβπΆ) |
mapdpg.j | β’ π½ = (LSpanβπΆ) |
mapdpg.k | β’ (π β (πΎ β HL β§ π β π»)) |
mapdpg.x | β’ (π β π β (π β { 0 })) |
mapdpg.y | β’ (π β π β (π β { 0 })) |
mapdpg.g | β’ (π β πΊ β πΉ) |
mapdpg.ne | β’ (π β (πβ{π}) β (πβ{π})) |
mapdpg.e | β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) |
mapdpgem25.h1 | β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) |
mapdpgem25.i1 | β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) |
Ref | Expression |
---|---|
mapdpglem25 | β’ (π β ((π½β{β}) = (π½β{π}) β§ (π½β{(πΊπ β)}) = (π½β{(πΊπ π)}))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mapdpgem25.h1 | . . . . 5 β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) | |
2 | 1 | simprd 495 | . . . 4 β’ (π β ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)}))) |
3 | 2 | simpld 494 | . . 3 β’ (π β (πβ(πβ{π})) = (π½β{β})) |
4 | mapdpgem25.i1 | . . . . 5 β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) | |
5 | 4 | simprd 495 | . . . 4 β’ (π β ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)}))) |
6 | 5 | simpld 494 | . . 3 β’ (π β (πβ(πβ{π})) = (π½β{π})) |
7 | 3, 6 | eqtr3d 2766 | . 2 β’ (π β (π½β{β}) = (π½β{π})) |
8 | 2 | simprd 495 | . . 3 β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})) |
9 | 5 | simprd 495 | . . 3 β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})) |
10 | 8, 9 | eqtr3d 2766 | . 2 β’ (π β (π½β{(πΊπ β)}) = (π½β{(πΊπ π)})) |
11 | 7, 10 | jca 511 | 1 β’ (π β ((π½β{β}) = (π½β{π}) β§ (π½β{(πΊπ β)}) = (π½β{(πΊπ π)}))) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 395 = wceq 1533 β wcel 2098 β wne 2932 β cdif 3937 {csn 4620 βcfv 6533 (class class class)co 7401 Basecbs 17143 0gc0g 17384 -gcsg 18855 LSpanclspn 20808 HLchlt 38710 LHypclh 39345 DVecHcdvh 40439 LCDualclcd 40947 mapdcmpd 40985 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1774 df-cleq 2716 |
This theorem is referenced by: mapdpglem26 41059 mapdpglem27 41060 |
Copyright terms: Public domain | W3C validator |