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