Description: Part (7) of Baer p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-May-2015) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mapdh7.h | |- H = ( LHyp ` K ) |
|
| mapdh7.u | |- U = ( ( DVecH ` K ) ` W ) |
||
| mapdh7.v | |- V = ( Base ` U ) |
||
| mapdh7.s | |- .- = ( -g ` U ) |
||
| mapdh7.o | |- .0. = ( 0g ` U ) |
||
| mapdh7.n | |- N = ( LSpan ` U ) |
||
| mapdh7.c | |- C = ( ( LCDual ` K ) ` W ) |
||
| mapdh7.d | |- D = ( Base ` C ) |
||
| mapdh7.r | |- R = ( -g ` C ) |
||
| mapdh7.q | |- Q = ( 0g ` C ) |
||
| mapdh7.j | |- J = ( LSpan ` C ) |
||
| mapdh7.m | |- M = ( ( mapd ` K ) ` W ) |
||
| mapdh7.i | |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) |
||
| mapdh7.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| mapdh7.f | |- ( ph -> F e. D ) |
||
| mapdh7.mn | |- ( ph -> ( M ` ( N ` { u } ) ) = ( J ` { F } ) ) |
||
| mapdh7.x | |- ( ph -> u e. ( V \ { .0. } ) ) |
||
| mapdh7.y | |- ( ph -> v e. ( V \ { .0. } ) ) |
||
| mapdh7.z | |- ( ph -> w e. ( V \ { .0. } ) ) |
||
| mapdh7.ne | |- ( ph -> ( N ` { u } ) =/= ( N ` { v } ) ) |
||
| mapdh7.wn | |- ( ph -> -. w e. ( N ` { u , v } ) ) |
||
| mapdh7a | |- ( ph -> ( I ` <. u , F , v >. ) = G ) |
||
| Assertion | mapdh7cN | |- ( ph -> ( I ` <. v , G , u >. ) = F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mapdh7.h | |- H = ( LHyp ` K ) |
|
| 2 | mapdh7.u | |- U = ( ( DVecH ` K ) ` W ) |
|
| 3 | mapdh7.v | |- V = ( Base ` U ) |
|
| 4 | mapdh7.s | |- .- = ( -g ` U ) |
|
| 5 | mapdh7.o | |- .0. = ( 0g ` U ) |
|
| 6 | mapdh7.n | |- N = ( LSpan ` U ) |
|
| 7 | mapdh7.c | |- C = ( ( LCDual ` K ) ` W ) |
|
| 8 | mapdh7.d | |- D = ( Base ` C ) |
|
| 9 | mapdh7.r | |- R = ( -g ` C ) |
|
| 10 | mapdh7.q | |- Q = ( 0g ` C ) |
|
| 11 | mapdh7.j | |- J = ( LSpan ` C ) |
|
| 12 | mapdh7.m | |- M = ( ( mapd ` K ) ` W ) |
|
| 13 | mapdh7.i | |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) |
|
| 14 | mapdh7.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 15 | mapdh7.f | |- ( ph -> F e. D ) |
|
| 16 | mapdh7.mn | |- ( ph -> ( M ` ( N ` { u } ) ) = ( J ` { F } ) ) |
|
| 17 | mapdh7.x | |- ( ph -> u e. ( V \ { .0. } ) ) |
|
| 18 | mapdh7.y | |- ( ph -> v e. ( V \ { .0. } ) ) |
|
| 19 | mapdh7.z | |- ( ph -> w e. ( V \ { .0. } ) ) |
|
| 20 | mapdh7.ne | |- ( ph -> ( N ` { u } ) =/= ( N ` { v } ) ) |
|
| 21 | mapdh7.wn | |- ( ph -> -. w e. ( N ` { u , v } ) ) |
|
| 22 | mapdh7a | |- ( ph -> ( I ` <. u , F , v >. ) = G ) |
|
| 23 | 18 | eldifad | |- ( ph -> v e. V ) |
| 24 | 10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 17 23 20 | mapdhcl | |- ( ph -> ( I ` <. u , F , v >. ) e. D ) |
| 25 | 22 24 | eqeltrrd | |- ( ph -> G e. D ) |
| 26 | 10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 17 18 25 20 | mapdheq2 | |- ( ph -> ( ( I ` <. u , F , v >. ) = G -> ( I ` <. v , G , u >. ) = F ) ) |
| 27 | 22 26 | mpd | |- ( ph -> ( I ` <. v , G , u >. ) = F ) |