Metamath Proof Explorer


Theorem hdmap14lem9

Description: Part of proof of part 14 in Baer p. 49 line 38. (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 hdmap14lem9 φ 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 hdmap14lem8.j φ J A
26 hdmap14lem8.xy φ S F · ˙ X + ˙ Y = J ˙ S X + ˙ Y
27 eqid Base C = Base C
28 eqid 0 C = 0 C
29 eqid LSpan C = LSpan C
30 1 10 16 lcdlvec φ C LVec
31 1 2 3 6 10 28 27 15 16 17 hdmapnzcl φ S X Base C 0 C
32 1 2 3 6 10 28 27 15 16 18 hdmapnzcl φ S Y Base C 0 C
33 eqid LSubSp U = LSubSp U
34 eqid mapd K W = mapd K W
35 1 2 16 dvhlmod φ U LMod
36 17 eldifad φ X V
37 3 33 7 lspsncl U LMod X V N X LSubSp U
38 35 36 37 syl2anc φ N X LSubSp U
39 18 eldifad φ Y V
40 3 33 7 lspsncl U LMod Y V N Y LSubSp U
41 35 39 40 syl2anc φ N Y LSubSp U
42 1 2 33 34 16 38 41 mapd11 φ mapd K W N X = mapd K W N Y N X = N Y
43 42 necon3bid φ mapd K W N X mapd K W N Y N X N Y
44 24 43 mpbird φ mapd K W N X mapd K W N Y
45 1 2 3 7 10 29 34 15 16 36 hdmap10 φ mapd K W N X = LSpan C S X
46 1 2 3 7 10 29 34 15 16 39 hdmap10 φ mapd K W N Y = LSpan C S Y
47 44 45 46 3netr3d φ LSpan C S X LSpan C S Y
48 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 hdmap14lem8 φ J ˙ S X ˙ J ˙ S Y = G ˙ S X ˙ I ˙ S Y
49 27 11 13 14 12 28 29 30 31 32 25 25 20 21 47 48 lvecindp2 φ J = G J = I
50 49 simpld φ J = G
51 49 simprd φ J = I
52 50 51 eqtr3d φ G = I