Metamath Proof Explorer

Theorem hgmapadd

Description: Part 15 of Baer p. 50 line 13. (Contributed by NM, 6-Jun-2015)

Ref Expression
Hypotheses hgmapadd.h 
|- H = ( LHyp ` K )
hgmapadd.u 
|- U = ( ( DVecH ` K ) ` W )
hgmapadd.r 
|- R = ( Scalar ` U )
hgmapadd.b 
|- B = ( Base ` R )
hgmapadd.p 
|- .+ = ( +g ` R )
hgmapadd.g 
|- G = ( ( HGMap ` K ) ` W )
hgmapadd.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hgmapadd.x 
|- ( ph -> X e. B )
hgmapadd.y 
|- ( ph -> Y e. B )
Assertion hgmapadd 
|- ( ph -> ( G ` ( X .+ Y ) ) = ( ( G ` X ) .+ ( G ` Y ) ) )

Proof

Step Hyp Ref Expression
1 hgmapadd.h 
 |-  H = ( LHyp ` K )
2 hgmapadd.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hgmapadd.r 
 |-  R = ( Scalar ` U )
4 hgmapadd.b 
 |-  B = ( Base ` R )
5 hgmapadd.p 
 |-  .+ = ( +g ` R )
6 hgmapadd.g 
 |-  G = ( ( HGMap ` K ) ` W )
7 hgmapadd.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 hgmapadd.x 
 |-  ( ph -> X e. B )
9 hgmapadd.y 
 |-  ( ph -> Y e. B )
10 eqid 
 |-  ( Base ` U ) = ( Base ` U )
11 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
12 1 2 10 11 7 dvh1dim 
 |-  ( ph -> E. t e. ( Base ` U ) t =/= ( 0g ` U ) )
13 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
14 1 13 7 lcdlmod 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. LMod )
15 14 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( LCDual ` K ) ` W ) e. LMod )
16 eqid 
 |-  ( Scalar ` ( ( LCDual ` K ) ` W ) ) = ( Scalar ` ( ( LCDual ` K ) ` W ) )
17 eqid 
 |-  ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) )
18 7 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
19 8 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> X e. B )
20 1 2 3 4 13 16 17 6 18 19 hgmapdcl 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( G ` X ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
21 1 2 3 4 13 16 17 6 7 9 hgmapdcl 
 |-  ( ph -> ( G ` Y ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
22 21 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( G ` Y ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
23 eqid 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
24 eqid 
 |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
25 simp2 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> t e. ( Base ` U ) )
26 1 2 10 13 23 24 18 25 hdmapcl 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` t ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
27 eqid 
 |-  ( +g ` ( ( LCDual ` K ) ` W ) ) = ( +g ` ( ( LCDual ` K ) ` W ) )
28 eqid 
 |-  ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` ( ( LCDual ` K ) ` W ) )
29 eqid 
 |-  ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) )
30 23 27 16 28 17 29 lmodvsdir 
 |-  ( ( ( ( LCDual ` K ) ` W ) e. LMod /\ ( ( G ` X ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) /\ ( G ` Y ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) /\ ( ( ( HDMap ` K ) ` W ) ` t ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) ) ) -> ( ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) = ( ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ( +g ` ( ( LCDual ` K ) ` W ) ) ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ) )
31 15 20 22 26 30 syl13anc 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) = ( ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ( +g ` ( ( LCDual ` K ) ` W ) ) ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ) )
32 1 2 7 dvhlmod 
 |-  ( ph -> U e. LMod )
33 32 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> U e. LMod )
34 9 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> Y e. B )
35 eqid 
 |-  ( +g ` U ) = ( +g ` U )
36 eqid 
 |-  ( .s ` U ) = ( .s ` U )
37 10 35 3 36 4 5 lmodvsdir 
 |-  ( ( U e. LMod /\ ( X e. B /\ Y e. B /\ t e. ( Base ` U ) ) ) -> ( ( X .+ Y ) ( .s ` U ) t ) = ( ( X ( .s ` U ) t ) ( +g ` U ) ( Y ( .s ` U ) t ) ) )
38 33 19 34 25 37 syl13anc 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( X .+ Y ) ( .s ` U ) t ) = ( ( X ( .s ` U ) t ) ( +g ` U ) ( Y ( .s ` U ) t ) ) )
39 38 fveq2d 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( ( X .+ Y ) ( .s ` U ) t ) ) = ( ( ( HDMap ` K ) ` W ) ` ( ( X ( .s ` U ) t ) ( +g ` U ) ( Y ( .s ` U ) t ) ) ) )
40 10 3 36 4 lmodvscl 
 |-  ( ( U e. LMod /\ X e. B /\ t e. ( Base ` U ) ) -> ( X ( .s ` U ) t ) e. ( Base ` U ) )
41 33 19 25 40 syl3anc 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( X ( .s ` U ) t ) e. ( Base ` U ) )
42 10 3 36 4 lmodvscl 
 |-  ( ( U e. LMod /\ Y e. B /\ t e. ( Base ` U ) ) -> ( Y ( .s ` U ) t ) e. ( Base ` U ) )
43 33 34 25 42 syl3anc 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( Y ( .s ` U ) t ) e. ( Base ` U ) )
44 1 2 10 35 13 27 24 18 41 43 hdmapadd 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( ( X ( .s ` U ) t ) ( +g ` U ) ( Y ( .s ` U ) t ) ) ) = ( ( ( ( HDMap ` K ) ` W ) ` ( X ( .s ` U ) t ) ) ( +g ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` ( Y ( .s ` U ) t ) ) ) )
45 1 2 10 36 3 4 13 28 24 6 18 25 19 hgmapvs 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( X ( .s ` U ) t ) ) = ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) )
46 1 2 10 36 3 4 13 28 24 6 18 25 34 hgmapvs 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( Y ( .s ` U ) t ) ) = ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) )
47 45 46 oveq12d 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` ( X ( .s ` U ) t ) ) ( +g ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` ( Y ( .s ` U ) t ) ) ) = ( ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ( +g ` ( ( LCDual ` K ) ` W ) ) ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ) )
48 39 44 47 3eqtrrd 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( G ` X ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ( +g ` ( ( LCDual ` K ) ` W ) ) ( ( G ` Y ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) ) = ( ( ( HDMap ` K ) ` W ) ` ( ( X .+ Y ) ( .s ` U ) t ) ) )
49 3 4 5 lmodacl 
 |-  ( ( U e. LMod /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
50 32 8 9 49 syl3anc 
 |-  ( ph -> ( X .+ Y ) e. B )
51 50 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( X .+ Y ) e. B )
52 1 2 10 36 3 4 13 28 24 6 18 25 51 hgmapvs 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` ( ( X .+ Y ) ( .s ` U ) t ) ) = ( ( G ` ( X .+ Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) )
53 31 48 52 3eqtrrd 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( G ` ( X .+ Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) = ( ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) )
54 eqid 
 |-  ( 0g ` ( ( LCDual ` K ) ` W ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) )
55 1 13 7 lcdlvec 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. LVec )
56 55 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( LCDual ` K ) ` W ) e. LVec )
57 1 2 3 4 13 16 17 6 7 50 hgmapdcl 
 |-  ( ph -> ( G ` ( X .+ Y ) ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
58 57 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( G ` ( X .+ Y ) ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
59 1 2 3 4 13 16 17 6 7 8 hgmapdcl 
 |-  ( ph -> ( G ` X ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
60 16 17 29 lmodacl 
 |-  ( ( ( ( LCDual ` K ) ` W ) e. LMod /\ ( G ` X ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) /\ ( G ` Y ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ) -> ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
61 14 59 21 60 syl3anc 
 |-  ( ph -> ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
62 61 3ad2ant1 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) e. ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) )
63 simp3 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> t =/= ( 0g ` U ) )
64 1 2 10 11 13 54 24 18 25 hdmapeq0 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` t ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> t = ( 0g ` U ) ) )
65 64 necon3bid 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( ( HDMap ` K ) ` W ) ` t ) =/= ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> t =/= ( 0g ` U ) ) )
66 63 65 mpbird 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( HDMap ` K ) ` W ) ` t ) =/= ( 0g ` ( ( LCDual ` K ) ` W ) ) )
67 23 28 16 17 54 56 58 62 26 66 lvecvscan2 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( ( ( G ` ( X .+ Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) = ( ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` t ) ) <-> ( G ` ( X .+ Y ) ) = ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ) )
68 53 67 mpbid 
 |-  ( ( ph /\ t e. ( Base ` U ) /\ t =/= ( 0g ` U ) ) -> ( G ` ( X .+ Y ) ) = ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) )
69 68 rexlimdv3a 
 |-  ( ph -> ( E. t e. ( Base ` U ) t =/= ( 0g ` U ) -> ( G ` ( X .+ Y ) ) = ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) ) )
70 12 69 mpd 
 |-  ( ph -> ( G ` ( X .+ Y ) ) = ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) )
71 1 2 3 5 13 16 29 7 lcdsadd 
 |-  ( ph -> ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = .+ )
72 71 oveqd 
 |-  ( ph -> ( ( G ` X ) ( +g ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) ( G ` Y ) ) = ( ( G ` X ) .+ ( G ` Y ) ) )
73 70 72 eqtrd 
 |-  ( ph -> ( G ` ( X .+ Y ) ) = ( ( G ` X ) .+ ( G ` Y ) ) )