Metamath Proof Explorer


Theorem hdmap14lem8

Description: Part of proof of part 14 in Baer p. 49 lines 33-35. (Contributed by NM, 1-Jun-2015)

Ref Expression
Hypotheses hdmap14lem8.h H = LHyp K
hdmap14lem8.u U = DVecH K W
hdmap14lem8.v V = Base U
hdmap14lem8.q + ˙ = + U
hdmap14lem8.t · ˙ = U
hdmap14lem8.o 0 ˙ = 0 U
hdmap14lem8.n N = LSpan U
hdmap14lem8.r R = Scalar U
hdmap14lem8.b B = Base R
hdmap14lem8.c C = LCDual K W
hdmap14lem8.d ˙ = + C
hdmap14lem8.e ˙ = C
hdmap14lem8.p P = Scalar C
hdmap14lem8.a A = Base P
hdmap14lem8.s S = HDMap K W
hdmap14lem8.k φ K HL W H
hdmap14lem8.x φ X V 0 ˙
hdmap14lem8.y φ Y V 0 ˙
hdmap14lem8.f φ F B
hdmap14lem8.g φ G A
hdmap14lem8.i φ I A
hdmap14lem8.xx φ S F · ˙ X = G ˙ S X
hdmap14lem8.yy φ S F · ˙ Y = I ˙ S Y
hdmap14lem8.ne φ N X N Y
hdmap14lem8.j φ J A
hdmap14lem8.xy φ S F · ˙ X + ˙ Y = J ˙ S X + ˙ Y
Assertion hdmap14lem8 φ J ˙ S X ˙ J ˙ S Y = G ˙ S X ˙ I ˙ S Y

Proof

Step Hyp Ref Expression
1 hdmap14lem8.h H = LHyp K
2 hdmap14lem8.u U = DVecH K W
3 hdmap14lem8.v V = Base U
4 hdmap14lem8.q + ˙ = + U
5 hdmap14lem8.t · ˙ = U
6 hdmap14lem8.o 0 ˙ = 0 U
7 hdmap14lem8.n N = LSpan U
8 hdmap14lem8.r R = Scalar U
9 hdmap14lem8.b B = Base R
10 hdmap14lem8.c C = LCDual K W
11 hdmap14lem8.d ˙ = + C
12 hdmap14lem8.e ˙ = C
13 hdmap14lem8.p P = Scalar C
14 hdmap14lem8.a A = Base P
15 hdmap14lem8.s S = HDMap K W
16 hdmap14lem8.k φ K HL W H
17 hdmap14lem8.x φ X V 0 ˙
18 hdmap14lem8.y φ Y V 0 ˙
19 hdmap14lem8.f φ F B
20 hdmap14lem8.g φ G A
21 hdmap14lem8.i φ I A
22 hdmap14lem8.xx φ S F · ˙ X = G ˙ S X
23 hdmap14lem8.yy φ S F · ˙ Y = I ˙ S Y
24 hdmap14lem8.ne φ N X N Y
25 hdmap14lem8.j φ J A
26 hdmap14lem8.xy φ S F · ˙ X + ˙ Y = J ˙ S X + ˙ Y
27 1 10 16 lcdlmod φ C LMod
28 eqid Base C = Base C
29 17 eldifad φ X V
30 1 2 3 10 28 15 16 29 hdmapcl φ S X Base C
31 18 eldifad φ Y V
32 1 2 3 10 28 15 16 31 hdmapcl φ S Y Base C
33 28 11 13 12 14 lmodvsdi C LMod J A S X Base C S Y Base C J ˙ S X ˙ S Y = J ˙ S X ˙ J ˙ S Y
34 27 25 30 32 33 syl13anc φ J ˙ S X ˙ S Y = J ˙ S X ˙ J ˙ S Y
35 1 2 3 4 10 11 15 16 29 31 hdmapadd φ S X + ˙ Y = S X ˙ S Y
36 35 oveq2d φ J ˙ S X + ˙ Y = J ˙ S X ˙ S Y
37 1 2 16 dvhlmod φ U LMod
38 3 4 8 5 9 lmodvsdi U LMod F B X V Y V F · ˙ X + ˙ Y = F · ˙ X + ˙ F · ˙ Y
39 37 19 29 31 38 syl13anc φ F · ˙ X + ˙ Y = F · ˙ X + ˙ F · ˙ Y
40 39 fveq2d φ S F · ˙ X + ˙ Y = S F · ˙ X + ˙ F · ˙ Y
41 3 8 5 9 lmodvscl U LMod F B X V F · ˙ X V
42 37 19 29 41 syl3anc φ F · ˙ X V
43 3 8 5 9 lmodvscl U LMod F B Y V F · ˙ Y V
44 37 19 31 43 syl3anc φ F · ˙ Y V
45 1 2 3 4 10 11 15 16 42 44 hdmapadd φ S F · ˙ X + ˙ F · ˙ Y = S F · ˙ X ˙ S F · ˙ Y
46 22 23 oveq12d φ S F · ˙ X ˙ S F · ˙ Y = G ˙ S X ˙ I ˙ S Y
47 40 45 46 3eqtrd φ S F · ˙ X + ˙ Y = G ˙ S X ˙ I ˙ S Y
48 26 47 eqtr3d φ J ˙ S X + ˙ Y = G ˙ S X ˙ I ˙ S Y
49 36 48 eqtr3d φ J ˙ S X ˙ S Y = G ˙ S X ˙ I ˙ S Y
50 34 49 eqtr3d φ J ˙ S X ˙ J ˙ S Y = G ˙ S X ˙ I ˙ S Y