Metamath Proof Explorer


Theorem hdmap14lem10

Description: Part of proof of part 14 in Baer p. 49 line 38. (Contributed by NM, 3-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
Assertion hdmap14lem10 φ G = I

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 eqid LSpan C = LSpan C
26 1 2 16 dvhlmod φ U LMod
27 17 eldifad φ X V
28 18 eldifad φ Y V
29 3 4 lmodvacl U LMod X V Y V X + ˙ Y V
30 26 27 28 29 syl3anc φ X + ˙ Y V
31 1 2 3 5 8 9 10 12 25 13 14 15 16 30 19 hdmap14lem2a φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y
32 16 3ad2ant1 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y K HL W H
33 17 3ad2ant1 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y X V 0 ˙
34 18 3ad2ant1 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y Y V 0 ˙
35 19 3ad2ant1 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y F B
36 20 3ad2ant1 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y G A
37 21 3ad2ant1 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y I A
38 22 3ad2ant1 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y S F · ˙ X = G ˙ S X
39 23 3ad2ant1 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y S F · ˙ Y = I ˙ S Y
40 24 3ad2ant1 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y N X N Y
41 simp2 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y g A
42 simp3 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y
43 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 32 33 34 35 36 37 38 39 40 41 42 hdmap14lem9 φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y G = I
44 43 rexlimdv3a φ g A S F · ˙ X + ˙ Y = g ˙ S X + ˙ Y G = I
45 31 44 mpd φ G = I