Description: Lemma for mapdpg . Baer p. 45, line 6: "Hence Fx=Fy, an impossibility." (Contributed by NM, 20-Mar-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mapdpglem.h | |- H = ( LHyp ` K ) |
|
| mapdpglem.m | |- M = ( ( mapd ` K ) ` W ) |
||
| mapdpglem.u | |- U = ( ( DVecH ` K ) ` W ) |
||
| mapdpglem.v | |- V = ( Base ` U ) |
||
| mapdpglem.s | |- .- = ( -g ` U ) |
||
| mapdpglem.n | |- N = ( LSpan ` U ) |
||
| mapdpglem.c | |- C = ( ( LCDual ` K ) ` W ) |
||
| mapdpglem.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| mapdpglem.x | |- ( ph -> X e. V ) |
||
| mapdpglem.y | |- ( ph -> Y e. V ) |
||
| mapdpglem1.p | |- .(+) = ( LSSum ` C ) |
||
| mapdpglem2.j | |- J = ( LSpan ` C ) |
||
| mapdpglem3.f | |- F = ( Base ` C ) |
||
| mapdpglem3.te | |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) ) |
||
| mapdpglem3.a | |- A = ( Scalar ` U ) |
||
| mapdpglem3.b | |- B = ( Base ` A ) |
||
| mapdpglem3.t | |- .x. = ( .s ` C ) |
||
| mapdpglem3.r | |- R = ( -g ` C ) |
||
| mapdpglem3.g | |- ( ph -> G e. F ) |
||
| mapdpglem3.e | |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) ) |
||
| mapdpglem4.q | |- Q = ( 0g ` U ) |
||
| mapdpglem.ne | |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
||
| mapdpglem4.jt | |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) |
||
| mapdpglem4.z | |- .0. = ( 0g ` A ) |
||
| mapdpglem4.g4 | |- ( ph -> g e. B ) |
||
| mapdpglem4.z4 | |- ( ph -> z e. ( M ` ( N ` { Y } ) ) ) |
||
| mapdpglem4.t4 | |- ( ph -> t = ( ( g .x. G ) R z ) ) |
||
| mapdpglem4.xn | |- ( ph -> X =/= Q ) |
||
| mapdpglem4.g0 | |- ( ph -> g = .0. ) |
||
| Assertion | mapdpglem10 | |- ( ph -> ( N ` { X } ) = ( N ` { Y } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mapdpglem.h | |- H = ( LHyp ` K ) |
|
| 2 | mapdpglem.m | |- M = ( ( mapd ` K ) ` W ) |
|
| 3 | mapdpglem.u | |- U = ( ( DVecH ` K ) ` W ) |
|
| 4 | mapdpglem.v | |- V = ( Base ` U ) |
|
| 5 | mapdpglem.s | |- .- = ( -g ` U ) |
|
| 6 | mapdpglem.n | |- N = ( LSpan ` U ) |
|
| 7 | mapdpglem.c | |- C = ( ( LCDual ` K ) ` W ) |
|
| 8 | mapdpglem.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 9 | mapdpglem.x | |- ( ph -> X e. V ) |
|
| 10 | mapdpglem.y | |- ( ph -> Y e. V ) |
|
| 11 | mapdpglem1.p | |- .(+) = ( LSSum ` C ) |
|
| 12 | mapdpglem2.j | |- J = ( LSpan ` C ) |
|
| 13 | mapdpglem3.f | |- F = ( Base ` C ) |
|
| 14 | mapdpglem3.te | |- ( ph -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) ) |
|
| 15 | mapdpglem3.a | |- A = ( Scalar ` U ) |
|
| 16 | mapdpglem3.b | |- B = ( Base ` A ) |
|
| 17 | mapdpglem3.t | |- .x. = ( .s ` C ) |
|
| 18 | mapdpglem3.r | |- R = ( -g ` C ) |
|
| 19 | mapdpglem3.g | |- ( ph -> G e. F ) |
|
| 20 | mapdpglem3.e | |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) ) |
|
| 21 | mapdpglem4.q | |- Q = ( 0g ` U ) |
|
| 22 | mapdpglem.ne | |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
|
| 23 | mapdpglem4.jt | |- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) |
|
| 24 | mapdpglem4.z | |- .0. = ( 0g ` A ) |
|
| 25 | mapdpglem4.g4 | |- ( ph -> g e. B ) |
|
| 26 | mapdpglem4.z4 | |- ( ph -> z e. ( M ` ( N ` { Y } ) ) ) |
|
| 27 | mapdpglem4.t4 | |- ( ph -> t = ( ( g .x. G ) R z ) ) |
|
| 28 | mapdpglem4.xn | |- ( ph -> X =/= Q ) |
|
| 29 | mapdpglem4.g0 | |- ( ph -> g = .0. ) |
|
| 30 | 1 3 8 | dvhlvec | |- ( ph -> U e. LVec ) |
| 31 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 | mapdpglem9 | |- ( ph -> X e. ( N ` { Y } ) ) |
| 32 | 4 21 6 30 10 31 28 | lspsneleq | |- ( ph -> ( N ` { X } ) = ( N ` { Y } ) ) |