Metamath Proof Explorer


Theorem hdmap14lem1a

Description: Prior to part 14 in Baer p. 49, line 25. (Contributed by NM, 31-May-2015)

Ref Expression
Hypotheses hdmap14lem1a.h H = LHyp K
hdmap14lem1a.u U = DVecH K W
hdmap14lem1a.v V = Base U
hdmap14lem1a.t · ˙ = U
hdmap14lem1a.r R = Scalar U
hdmap14lem1a.b B = Base R
hdmap14lem1a.c C = LCDual K W
hdmap14lem2a.e ˙ = C
hdmap14lem1a.l L = LSpan C
hdmap14lem2a.p P = Scalar C
hdmap14lem2a.a A = Base P
hdmap14lem1a.s S = HDMap K W
hdmap14lem1a.k φ K HL W H
hdmap14lem3a.x φ X V
hdmap14lem1a.f φ F B
hdmap14lem1a.z 0 ˙ = 0 R
hdmap14lem1a.fn φ F 0 ˙
Assertion hdmap14lem1a φ L S X = L S F · ˙ X

Proof

Step Hyp Ref Expression
1 hdmap14lem1a.h H = LHyp K
2 hdmap14lem1a.u U = DVecH K W
3 hdmap14lem1a.v V = Base U
4 hdmap14lem1a.t · ˙ = U
5 hdmap14lem1a.r R = Scalar U
6 hdmap14lem1a.b B = Base R
7 hdmap14lem1a.c C = LCDual K W
8 hdmap14lem2a.e ˙ = C
9 hdmap14lem1a.l L = LSpan C
10 hdmap14lem2a.p P = Scalar C
11 hdmap14lem2a.a A = Base P
12 hdmap14lem1a.s S = HDMap K W
13 hdmap14lem1a.k φ K HL W H
14 hdmap14lem3a.x φ X V
15 hdmap14lem1a.f φ F B
16 hdmap14lem1a.z 0 ˙ = 0 R
17 hdmap14lem1a.fn φ F 0 ˙
18 1 2 13 dvhlvec φ U LVec
19 eqid LSpan U = LSpan U
20 3 5 4 6 16 19 lspsnvs U LVec F B F 0 ˙ X V LSpan U F · ˙ X = LSpan U X
21 18 15 17 14 20 syl121anc φ LSpan U F · ˙ X = LSpan U X
22 21 fveq2d φ mapd K W LSpan U F · ˙ X = mapd K W LSpan U X
23 eqid mapd K W = mapd K W
24 1 2 13 dvhlmod φ U LMod
25 3 5 4 6 lmodvscl U LMod F B X V F · ˙ X V
26 24 15 14 25 syl3anc φ F · ˙ X V
27 1 2 3 19 7 9 23 12 13 26 hdmap10 φ mapd K W LSpan U F · ˙ X = L S F · ˙ X
28 1 2 3 19 7 9 23 12 13 14 hdmap10 φ mapd K W LSpan U X = L S X
29 22 27 28 3eqtr3rd φ L S X = L S F · ˙ X