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 |
12
|
3ad2ant1 |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> ( K e. HL /\ W e. H ) ) |
19 |
13
|
3ad2ant1 |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> X e. ( V \ { .0. } ) ) |
20 |
14
|
3ad2ant1 |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> Y e. ( V \ { .0. } ) ) |
21 |
15
|
3ad2ant1 |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> G e. F ) |
22 |
16
|
3ad2ant1 |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
23 |
17
|
3ad2ant1 |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) ) |
24 |
|
simp2l |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> h e. F ) |
25 |
|
simp3l |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) |
26 |
24 25
|
jca |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) ) |
27 |
|
simp2r |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> i e. F ) |
28 |
|
simp3r |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) |
29 |
27 28
|
jca |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) |
30 |
|
eqid |
|- ( Scalar ` U ) = ( Scalar ` U ) |
31 |
|
eqid |
|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) ) |
32 |
|
eqid |
|- ( .s ` C ) = ( .s ` C ) |
33 |
|
eqid |
|- ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) ) |
34 |
1 2 3 4 5 6 7 8 9 10 11 18 19 20 21 22 23 26 29 30 31 32 33
|
mapdpglem26 |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> E. u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) h = ( u ( .s ` C ) i ) ) |
35 |
1 2 3 4 5 6 7 8 9 10 11 18 19 20 21 22 23 26 29 30 31 32 33
|
mapdpglem27 |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> E. v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) |
36 |
|
reeanv |
|- ( E. u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) E. v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) <-> ( E. u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) h = ( u ( .s ` C ) i ) /\ E. v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) |
37 |
34 35 36
|
sylanbrc |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> E. u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) E. v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) |
38 |
18
|
3ad2ant1 |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> ( K e. HL /\ W e. H ) ) |
39 |
19
|
3ad2ant1 |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> X e. ( V \ { .0. } ) ) |
40 |
20
|
3ad2ant1 |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> Y e. ( V \ { .0. } ) ) |
41 |
21
|
3ad2ant1 |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> G e. F ) |
42 |
22
|
3ad2ant1 |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
43 |
23
|
3ad2ant1 |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) ) |
44 |
|
simp12l |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> h e. F ) |
45 |
|
simp13l |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) |
46 |
44 45
|
jca |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> ( h e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) ) ) |
47 |
|
simp12r |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> i e. F ) |
48 |
|
simp13r |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) |
49 |
47 48
|
jca |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> ( i e. F /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) |
50 |
|
eldifi |
|- ( v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) -> v e. ( Base ` ( Scalar ` U ) ) ) |
51 |
50
|
adantl |
|- ( ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) -> v e. ( Base ` ( Scalar ` U ) ) ) |
52 |
51
|
3ad2ant2 |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> v e. ( Base ` ( Scalar ` U ) ) ) |
53 |
|
simp3l |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> h = ( u ( .s ` C ) i ) ) |
54 |
|
simp3r |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) |
55 |
|
eldifi |
|- ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) -> u e. ( Base ` ( Scalar ` U ) ) ) |
56 |
55
|
adantr |
|- ( ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) -> u e. ( Base ` ( Scalar ` U ) ) ) |
57 |
56
|
3ad2ant2 |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> u e. ( Base ` ( Scalar ` U ) ) ) |
58 |
1 2 3 4 5 6 7 8 9 10 11 38 39 40 41 42 43 46 49 30 31 32 33 52 53 54 57
|
mapdpglem31 |
|- ( ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) /\ ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) /\ ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) ) -> h = i ) |
59 |
58
|
3exp |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> ( ( u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) /\ v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ) -> ( ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) -> h = i ) ) ) |
60 |
59
|
rexlimdvv |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> ( E. u e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) E. v e. ( ( Base ` ( Scalar ` U ) ) \ { ( 0g ` ( Scalar ` U ) ) } ) ( h = ( u ( .s ` C ) i ) /\ ( G R h ) = ( v ( .s ` C ) ( G R i ) ) ) -> h = i ) ) |
61 |
37 60
|
mpd |
|- ( ( ph /\ ( h e. F /\ i e. F ) /\ ( ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) /\ ( ( M ` ( N ` { Y } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R i ) } ) ) ) ) -> h = i ) |