Metamath Proof Explorer

Theorem hdmapglem7b

Description: Lemma for hdmapg . (Contributed by NM, 14-Jun-2015)

Ref Expression
Hypotheses hdmapglem7.h 
|- H = ( LHyp ` K )
hdmapglem7.e 
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmapglem7.o 
|- O = ( ( ocH ` K ) ` W )
hdmapglem7.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapglem7.v 
|- V = ( Base ` U )
hdmapglem7.p 
|- .+ = ( +g ` U )
hdmapglem7.q 
|- .x. = ( .s ` U )
hdmapglem7.r 
|- R = ( Scalar ` U )
hdmapglem7.b 
|- B = ( Base ` R )
hdmapglem7.a 
|- .(+) = ( LSSum ` U )
hdmapglem7.n 
|- N = ( LSpan ` U )
hdmapglem7.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapglem7.x 
|- ( ph -> X e. V )
hdmapglem7.t 
|- .X. = ( .r ` R )
hdmapglem7.z 
|- .0. = ( 0g ` R )
hdmapglem7.c 
|- .+b = ( +g ` R )
hdmapglem7.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapglem7.g 
|- G = ( ( HGMap ` K ) ` W )
hdmapglem7b.u 
|- ( ph -> x e. ( O ` { E } ) )
hdmapglem7b.v 
|- ( ph -> y e. ( O ` { E } ) )
hdmapglem7b.k 
|- ( ph -> m e. B )
hdmapglem7b.l 
|- ( ph -> n e. B )
Assertion hdmapglem7b 
|- ( ph -> ( ( S ` ( ( m .x. E ) .+ x ) ) ` ( ( n .x. E ) .+ y ) ) = ( ( n .X. ( G ` m ) ) .+b ( ( S ` x ) ` y ) ) )

Proof

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 hdmapglem7b.u 
 |-  ( ph -> x e. ( O ` { E } ) )
20 hdmapglem7b.v 
 |-  ( ph -> y e. ( O ` { E } ) )
21 hdmapglem7b.k 
 |-  ( ph -> m e. B )
22 hdmapglem7b.l 
 |-  ( ph -> n e. B )
23 1 4 12 dvhlmod 
 |-  ( ph -> U e. LMod )
24 eqid 
 |-  ( Base ` K ) = ( Base ` K )
25 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
26 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
27 1 24 25 4 5 26 2 12 dvheveccl 
 |-  ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
28 27 eldifad 
 |-  ( ph -> E e. V )
29 5 8 7 9 lmodvscl 
 |-  ( ( U e. LMod /\ n e. B /\ E e. V ) -> ( n .x. E ) e. V )
30 23 22 28 29 syl3anc 
 |-  ( ph -> ( n .x. E ) e. V )
31 28 snssd 
 |-  ( ph -> { E } C_ V )
32 1 4 5 3 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) C_ V )
33 12 31 32 syl2anc 
 |-  ( ph -> ( O ` { E } ) C_ V )
34 33 20 sseldd 
 |-  ( ph -> y e. V )
35 5 6 lmodvacl 
 |-  ( ( U e. LMod /\ ( n .x. E ) e. V /\ y e. V ) -> ( ( n .x. E ) .+ y ) e. V )
36 23 30 34 35 syl3anc 
 |-  ( ph -> ( ( n .x. E ) .+ y ) e. V )
37 33 19 sseldd 
 |-  ( ph -> x e. V )
38 1 4 5 6 7 8 9 16 14 17 18 12 36 28 37 21 hdmapgln2 
 |-  ( ph -> ( ( S ` ( ( m .x. E ) .+ x ) ) ` ( ( n .x. E ) .+ y ) ) = ( ( ( ( S ` E ) ` ( ( n .x. E ) .+ y ) ) .X. ( G ` m ) ) .+b ( ( S ` x ) ` ( ( n .x. E ) .+ y ) ) ) )
39 1 4 5 6 7 8 9 16 14 17 12 28 34 28 22 hdmapln1 
 |-  ( ph -> ( ( S ` E ) ` ( ( n .x. E ) .+ y ) ) = ( ( n .X. ( ( S ` E ) ` E ) ) .+b ( ( S ` E ) ` y ) ) )
40 eqid 
 |-  ( ( HVMap ` K ) ` W ) = ( ( HVMap ` K ) ` W )
41 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
42 1 2 40 17 12 4 8 41 hdmapevec2 
 |-  ( ph -> ( ( S ` E ) ` E ) = ( 1r ` R ) )
43 42 oveq2d 
 |-  ( ph -> ( n .X. ( ( S ` E ) ` E ) ) = ( n .X. ( 1r ` R ) ) )
44 8 lmodring 
 |-  ( U e. LMod -> R e. Ring )
45 23 44 syl 
 |-  ( ph -> R e. Ring )
46 9 14 41 ringridm 
 |-  ( ( R e. Ring /\ n e. B ) -> ( n .X. ( 1r ` R ) ) = n )
47 45 22 46 syl2anc 
 |-  ( ph -> ( n .X. ( 1r ` R ) ) = n )
48 43 47 eqtrd 
 |-  ( ph -> ( n .X. ( ( S ` E ) ` E ) ) = n )
49 1 2 3 4 5 8 9 14 15 17 12 20 hdmapinvlem1 
 |-  ( ph -> ( ( S ` E ) ` y ) = .0. )
50 48 49 oveq12d 
 |-  ( ph -> ( ( n .X. ( ( S ` E ) ` E ) ) .+b ( ( S ` E ) ` y ) ) = ( n .+b .0. ) )
51 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
52 45 51 syl 
 |-  ( ph -> R e. Grp )
53 9 16 15 grprid 
 |-  ( ( R e. Grp /\ n e. B ) -> ( n .+b .0. ) = n )
54 52 22 53 syl2anc 
 |-  ( ph -> ( n .+b .0. ) = n )
55 39 50 54 3eqtrd 
 |-  ( ph -> ( ( S ` E ) ` ( ( n .x. E ) .+ y ) ) = n )
56 55 oveq1d 
 |-  ( ph -> ( ( ( S ` E ) ` ( ( n .x. E ) .+ y ) ) .X. ( G ` m ) ) = ( n .X. ( G ` m ) ) )
57 1 4 5 6 7 8 9 16 14 17 12 28 34 37 22 hdmapln1 
 |-  ( ph -> ( ( S ` x ) ` ( ( n .x. E ) .+ y ) ) = ( ( n .X. ( ( S ` x ) ` E ) ) .+b ( ( S ` x ) ` y ) ) )
58 1 2 3 4 5 8 9 14 15 17 12 19 hdmapinvlem2 
 |-  ( ph -> ( ( S ` x ) ` E ) = .0. )
59 58 oveq2d 
 |-  ( ph -> ( n .X. ( ( S ` x ) ` E ) ) = ( n .X. .0. ) )
60 9 14 15 ringrz 
 |-  ( ( R e. Ring /\ n e. B ) -> ( n .X. .0. ) = .0. )
61 45 22 60 syl2anc 
 |-  ( ph -> ( n .X. .0. ) = .0. )
62 59 61 eqtrd 
 |-  ( ph -> ( n .X. ( ( S ` x ) ` E ) ) = .0. )
63 62 oveq1d 
 |-  ( ph -> ( ( n .X. ( ( S ` x ) ` E ) ) .+b ( ( S ` x ) ` y ) ) = ( .0. .+b ( ( S ` x ) ` y ) ) )
64 1 4 5 8 9 17 12 34 37 hdmapipcl 
 |-  ( ph -> ( ( S ` x ) ` y ) e. B )
65 9 16 15 grplid 
 |-  ( ( R e. Grp /\ ( ( S ` x ) ` y ) e. B ) -> ( .0. .+b ( ( S ` x ) ` y ) ) = ( ( S ` x ) ` y ) )
66 52 64 65 syl2anc 
 |-  ( ph -> ( .0. .+b ( ( S ` x ) ` y ) ) = ( ( S ` x ) ` y ) )
67 57 63 66 3eqtrd 
 |-  ( ph -> ( ( S ` x ) ` ( ( n .x. E ) .+ y ) ) = ( ( S ` x ) ` y ) )
68 56 67 oveq12d 
 |-  ( ph -> ( ( ( ( S ` E ) ` ( ( n .x. E ) .+ y ) ) .X. ( G ` m ) ) .+b ( ( S ` x ) ` ( ( n .x. E ) .+ y ) ) ) = ( ( n .X. ( G ` m ) ) .+b ( ( S ` x ) ` y ) ) )
69 38 68 eqtrd 
 |-  ( ph -> ( ( S ` ( ( m .x. E ) .+ x ) ) ` ( ( n .x. E ) .+ y ) ) = ( ( n .X. ( G ` m ) ) .+b ( ( S ` x ) ` y ) ) )