Step |
Hyp |
Ref |
Expression |
1 |
|
hdmapglem7.h |
|- H = ( LHyp ` K ) |
2 |
|
hdmapglem7.e |
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. |
3 |
|
hdmapglem7.o |
|- O = ( ( ocH ` K ) ` W ) |
4 |
|
hdmapglem7.u |
|- U = ( ( DVecH ` K ) ` W ) |
5 |
|
hdmapglem7.v |
|- V = ( Base ` U ) |
6 |
|
hdmapglem7.p |
|- .+ = ( +g ` U ) |
7 |
|
hdmapglem7.q |
|- .x. = ( .s ` U ) |
8 |
|
hdmapglem7.r |
|- R = ( Scalar ` U ) |
9 |
|
hdmapglem7.b |
|- B = ( Base ` R ) |
10 |
|
hdmapglem7.a |
|- .(+) = ( LSSum ` U ) |
11 |
|
hdmapglem7.n |
|- N = ( LSpan ` U ) |
12 |
|
hdmapglem7.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
13 |
|
hdmapglem7.x |
|- ( ph -> X e. V ) |
14 |
|
hdmapglem7.t |
|- .X. = ( .r ` R ) |
15 |
|
hdmapglem7.z |
|- .0. = ( 0g ` R ) |
16 |
|
hdmapglem7.c |
|- .+b = ( +g ` R ) |
17 |
|
hdmapglem7.s |
|- S = ( ( HDMap ` K ) ` W ) |
18 |
|
hdmapglem7.g |
|- G = ( ( HGMap ` K ) ` W ) |
19 |
|
hdmapglem7.y |
|- ( ph -> Y e. V ) |
20 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
hdmapglem7a |
|- ( ph -> E. u e. ( O ` { E } ) E. k e. B X = ( ( k .x. E ) .+ u ) ) |
21 |
1 2 3 4 5 6 7 8 9 10 11 12 19
|
hdmapglem7a |
|- ( ph -> E. v e. ( O ` { E } ) E. l e. B Y = ( ( l .x. E ) .+ v ) ) |
22 |
12
|
ad2antrr |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( K e. HL /\ W e. H ) ) |
23 |
1 4 12
|
dvhlmod |
|- ( ph -> U e. LMod ) |
24 |
8
|
lmodring |
|- ( U e. LMod -> R e. Ring ) |
25 |
23 24
|
syl |
|- ( ph -> R e. Ring ) |
26 |
25
|
ad2antrr |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> R e. Ring ) |
27 |
|
simplrr |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> k e. B ) |
28 |
|
simprr |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> l e. B ) |
29 |
1 4 8 9 18 22 28
|
hgmapcl |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` l ) e. B ) |
30 |
9 14
|
ringcl |
|- ( ( R e. Ring /\ k e. B /\ ( G ` l ) e. B ) -> ( k .X. ( G ` l ) ) e. B ) |
31 |
26 27 29 30
|
syl3anc |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( k .X. ( G ` l ) ) e. B ) |
32 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
33 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
34 |
|
eqid |
|- ( 0g ` U ) = ( 0g ` U ) |
35 |
1 32 33 4 5 34 2 12
|
dvheveccl |
|- ( ph -> E e. ( V \ { ( 0g ` U ) } ) ) |
36 |
35
|
eldifad |
|- ( ph -> E e. V ) |
37 |
36
|
snssd |
|- ( ph -> { E } C_ V ) |
38 |
1 4 5 3
|
dochssv |
|- ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) C_ V ) |
39 |
12 37 38
|
syl2anc |
|- ( ph -> ( O ` { E } ) C_ V ) |
40 |
39
|
ad2antrr |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( O ` { E } ) C_ V ) |
41 |
|
simplrl |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> u e. ( O ` { E } ) ) |
42 |
40 41
|
sseldd |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> u e. V ) |
43 |
|
simprl |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> v e. ( O ` { E } ) ) |
44 |
40 43
|
sseldd |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> v e. V ) |
45 |
1 4 5 8 9 17 22 42 44
|
hdmapipcl |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( ( S ` v ) ` u ) e. B ) |
46 |
1 4 8 9 16 18 22 31 45
|
hgmapadd |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( k .X. ( G ` l ) ) .+b ( ( S ` v ) ` u ) ) ) = ( ( G ` ( k .X. ( G ` l ) ) ) .+b ( G ` ( ( S ` v ) ` u ) ) ) ) |
47 |
1 4 8 9 14 18 22 27 29
|
hgmapmul |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( k .X. ( G ` l ) ) ) = ( ( G ` ( G ` l ) ) .X. ( G ` k ) ) ) |
48 |
1 4 8 9 18 22 28
|
hgmapvv |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( G ` l ) ) = l ) |
49 |
48
|
oveq1d |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( ( G ` ( G ` l ) ) .X. ( G ` k ) ) = ( l .X. ( G ` k ) ) ) |
50 |
47 49
|
eqtrd |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( k .X. ( G ` l ) ) ) = ( l .X. ( G ` k ) ) ) |
51 |
|
eqid |
|- ( -g ` U ) = ( -g ` U ) |
52 |
1 2 3 4 5 6 51 7 8 9 14 15 17 18 22 41 43 27 27
|
hdmapglem5 |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( S ` v ) ` u ) ) = ( ( S ` u ) ` v ) ) |
53 |
50 52
|
oveq12d |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( ( G ` ( k .X. ( G ` l ) ) ) .+b ( G ` ( ( S ` v ) ` u ) ) ) = ( ( l .X. ( G ` k ) ) .+b ( ( S ` u ) ` v ) ) ) |
54 |
46 53
|
eqtrd |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( k .X. ( G ` l ) ) .+b ( ( S ` v ) ` u ) ) ) = ( ( l .X. ( G ` k ) ) .+b ( ( S ` u ) ` v ) ) ) |
55 |
13
|
ad2antrr |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> X e. V ) |
56 |
1 2 3 4 5 6 7 8 9 10 11 22 55 14 15 16 17 18 43 41 28 27
|
hdmapglem7b |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) = ( ( k .X. ( G ` l ) ) .+b ( ( S ` v ) ` u ) ) ) |
57 |
56
|
fveq2d |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) = ( G ` ( ( k .X. ( G ` l ) ) .+b ( ( S ` v ) ` u ) ) ) ) |
58 |
1 2 3 4 5 6 7 8 9 10 11 22 55 14 15 16 17 18 41 43 27 28
|
hdmapglem7b |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( ( S ` ( ( k .x. E ) .+ u ) ) ` ( ( l .x. E ) .+ v ) ) = ( ( l .X. ( G ` k ) ) .+b ( ( S ` u ) ` v ) ) ) |
59 |
54 57 58
|
3eqtr4d |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) = ( ( S ` ( ( k .x. E ) .+ u ) ) ` ( ( l .x. E ) .+ v ) ) ) |
60 |
59
|
3adantl3 |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) ) -> ( G ` ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) = ( ( S ` ( ( k .x. E ) .+ u ) ) ` ( ( l .x. E ) .+ v ) ) ) |
61 |
60
|
3adant3 |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( G ` ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) = ( ( S ` ( ( k .x. E ) .+ u ) ) ` ( ( l .x. E ) .+ v ) ) ) |
62 |
|
simp3 |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> Y = ( ( l .x. E ) .+ v ) ) |
63 |
62
|
fveq2d |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( S ` Y ) = ( S ` ( ( l .x. E ) .+ v ) ) ) |
64 |
|
simp13 |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> X = ( ( k .x. E ) .+ u ) ) |
65 |
63 64
|
fveq12d |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( ( S ` Y ) ` X ) = ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) |
66 |
65
|
fveq2d |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( G ` ( ( S ` ( ( l .x. E ) .+ v ) ) ` ( ( k .x. E ) .+ u ) ) ) ) |
67 |
64
|
fveq2d |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( S ` X ) = ( S ` ( ( k .x. E ) .+ u ) ) ) |
68 |
67 62
|
fveq12d |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( ( S ` X ) ` Y ) = ( ( S ` ( ( k .x. E ) .+ u ) ) ` ( ( l .x. E ) .+ v ) ) ) |
69 |
61 66 68
|
3eqtr4d |
|- ( ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) /\ ( v e. ( O ` { E } ) /\ l e. B ) /\ Y = ( ( l .x. E ) .+ v ) ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) ) |
70 |
69
|
3exp |
|- ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) -> ( ( v e. ( O ` { E } ) /\ l e. B ) -> ( Y = ( ( l .x. E ) .+ v ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) ) ) ) |
71 |
70
|
rexlimdvv |
|- ( ( ph /\ ( u e. ( O ` { E } ) /\ k e. B ) /\ X = ( ( k .x. E ) .+ u ) ) -> ( E. v e. ( O ` { E } ) E. l e. B Y = ( ( l .x. E ) .+ v ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) ) ) |
72 |
71
|
3exp |
|- ( ph -> ( ( u e. ( O ` { E } ) /\ k e. B ) -> ( X = ( ( k .x. E ) .+ u ) -> ( E. v e. ( O ` { E } ) E. l e. B Y = ( ( l .x. E ) .+ v ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) ) ) ) ) |
73 |
72
|
rexlimdvv |
|- ( ph -> ( E. u e. ( O ` { E } ) E. k e. B X = ( ( k .x. E ) .+ u ) -> ( E. v e. ( O ` { E } ) E. l e. B Y = ( ( l .x. E ) .+ v ) -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) ) ) ) |
74 |
20 21 73
|
mp2d |
|- ( ph -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) ) |