Description: Lemma for mapdpg . Baer p. 45 line 18: "vx'-vy'' = x'-uy''". (Contributed by NM, 22-Mar-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mapdpg.h | |- H = ( LHyp ` K ) |
|
| mapdpg.m | |- M = ( ( mapd ` K ) ` W ) |
||
| mapdpg.u | |- U = ( ( DVecH ` K ) ` W ) |
||
| mapdpg.v | |- V = ( Base ` U ) |
||
| mapdpg.s | |- .- = ( -g ` U ) |
||
| mapdpg.z | |- .0. = ( 0g ` U ) |
||
| mapdpg.n | |- N = ( LSpan ` U ) |
||
| mapdpg.c | |- C = ( ( LCDual ` K ) ` W ) |
||
| mapdpg.f | |- F = ( Base ` C ) |
||
| mapdpg.r | |- R = ( -g ` C ) |
||
| mapdpg.j | |- J = ( LSpan ` C ) |
||
| mapdpg.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| mapdpg.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
||
| mapdpg.y | |- ( ph -> Y e. ( V \ { .0. } ) ) |
||
| mapdpg.g | |- ( ph -> G e. F ) |
||
| mapdpg.ne | |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
||
| mapdpg.e | |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) ) |
||
| mapdpgem25.h1 | |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) ) |
||
| mapdpgem25.i1 | |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) |
||
| mapdpglem26.a | |- A = ( Scalar ` U ) |
||
| mapdpglem26.b | |- B = ( Base ` A ) |
||
| mapdpglem26.t | |- .x. = ( .s ` C ) |
||
| mapdpglem26.o | |- O = ( 0g ` A ) |
||
| mapdpglem28.ve | |- ( ph -> v e. B ) |
||
| mapdpglem28.u1 | |- ( ph -> h = ( u .x. i ) ) |
||
| mapdpglem28.u2 | |- ( ph -> ( G R h ) = ( v .x. ( G R i ) ) ) |
||
| Assertion | mapdpglem28 | |- ( ph -> ( ( v .x. G ) R ( v .x. i ) ) = ( G R ( u .x. i ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mapdpg.h | |- H = ( LHyp ` K ) |
|
| 2 | mapdpg.m | |- M = ( ( mapd ` K ) ` W ) |
|
| 3 | mapdpg.u | |- U = ( ( DVecH ` K ) ` W ) |
|
| 4 | mapdpg.v | |- V = ( Base ` U ) |
|
| 5 | mapdpg.s | |- .- = ( -g ` U ) |
|
| 6 | mapdpg.z | |- .0. = ( 0g ` U ) |
|
| 7 | mapdpg.n | |- N = ( LSpan ` U ) |
|
| 8 | mapdpg.c | |- C = ( ( LCDual ` K ) ` W ) |
|
| 9 | mapdpg.f | |- F = ( Base ` C ) |
|
| 10 | mapdpg.r | |- R = ( -g ` C ) |
|
| 11 | mapdpg.j | |- J = ( LSpan ` C ) |
|
| 12 | mapdpg.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 13 | mapdpg.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
|
| 14 | mapdpg.y | |- ( ph -> Y e. ( V \ { .0. } ) ) |
|
| 15 | mapdpg.g | |- ( ph -> G e. F ) |
|
| 16 | mapdpg.ne | |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
|
| 17 | mapdpg.e | |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) ) |
|
| 18 | mapdpgem25.h1 | |- ( ph -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) ) |
|
| 19 | mapdpgem25.i1 | |- ( ph -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) |
|
| 20 | mapdpglem26.a | |- A = ( Scalar ` U ) |
|
| 21 | mapdpglem26.b | |- B = ( Base ` A ) |
|
| 22 | mapdpglem26.t | |- .x. = ( .s ` C ) |
|
| 23 | mapdpglem26.o | |- O = ( 0g ` A ) |
|
| 24 | mapdpglem28.ve | |- ( ph -> v e. B ) |
|
| 25 | mapdpglem28.u1 | |- ( ph -> h = ( u .x. i ) ) |
|
| 26 | mapdpglem28.u2 | |- ( ph -> ( G R h ) = ( v .x. ( G R i ) ) ) |
|
| 27 | 25 | oveq2d | |- ( ph -> ( G R h ) = ( G R ( u .x. i ) ) ) |
| 28 | eqid | |- ( Scalar ` C ) = ( Scalar ` C ) |
|
| 29 | eqid | |- ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) ) |
|
| 30 | 1 8 12 | lcdlmod | |- ( ph -> C e. LMod ) |
| 31 | 1 3 20 21 8 28 29 12 | lcdsbase | |- ( ph -> ( Base ` ( Scalar ` C ) ) = B ) |
| 32 | 24 31 | eleqtrrd | |- ( ph -> v e. ( Base ` ( Scalar ` C ) ) ) |
| 33 | 19 | simpld | |- ( ph -> i e. F ) |
| 34 | 9 22 28 29 10 30 32 15 33 | lmodsubdi | |- ( ph -> ( v .x. ( G R i ) ) = ( ( v .x. G ) R ( v .x. i ) ) ) |
| 35 | 26 27 34 | 3eqtr3rd | |- ( ph -> ( ( v .x. G ) R ( v .x. i ) ) = ( G R ( u .x. i ) ) ) |