![]() |
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 40219. 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 497 | . . . 4 β’ (π β ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)}))) |
3 | 2 | simpld 496 | . . 3 β’ (π β (πβ(πβ{π})) = (π½β{β})) |
4 | mapdpgem25.i1 | . . . . 5 β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) | |
5 | 4 | simprd 497 | . . . 4 β’ (π β ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)}))) |
6 | 5 | simpld 496 | . . 3 β’ (π β (πβ(πβ{π})) = (π½β{π})) |
7 | 3, 6 | eqtr3d 2775 | . 2 β’ (π β (π½β{β}) = (π½β{π})) |
8 | 2 | simprd 497 | . . 3 β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})) |
9 | 5 | simprd 497 | . . 3 β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})) |
10 | 8, 9 | eqtr3d 2775 | . 2 β’ (π β (π½β{(πΊπ β)}) = (π½β{(πΊπ π)})) |
11 | 7, 10 | jca 513 | 1 β’ (π β ((π½β{β}) = (π½β{π}) β§ (π½β{(πΊπ β)}) = (π½β{(πΊπ π)}))) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 397 = wceq 1542 β wcel 2107 β wne 2940 β cdif 3911 {csn 4590 βcfv 6500 (class class class)co 7361 Basecbs 17091 0gc0g 17329 -gcsg 18758 LSpanclspn 20476 HLchlt 37862 LHypclh 38497 DVecHcdvh 39591 LCDualclcd 40099 mapdcmpd 40137 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 |
This theorem is referenced by: mapdpglem26 40211 mapdpglem27 40212 |
Copyright terms: Public domain | W3C validator |