Metamath Proof Explorer


Theorem hdmap1l6lem1

Description: Lemma for hdmap1l6 . Part (6) in Baer p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015)

Ref Expression
Hypotheses hdmap1l6.h H = LHyp K
hdmap1l6.u U = DVecH K W
hdmap1l6.v V = Base U
hdmap1l6.p + ˙ = + U
hdmap1l6.s - ˙ = - U
hdmap1l6c.o 0 ˙ = 0 U
hdmap1l6.n N = LSpan U
hdmap1l6.c C = LCDual K W
hdmap1l6.d D = Base C
hdmap1l6.a ˙ = + C
hdmap1l6.r R = - C
hdmap1l6.q Q = 0 C
hdmap1l6.l L = LSpan C
hdmap1l6.m M = mapd K W
hdmap1l6.i I = HDMap1 K W
hdmap1l6.k φ K HL W H
hdmap1l6.f φ F D
hdmap1l6cl.x φ X V 0 ˙
hdmap1l6.mn φ M N X = L F
hdmap1l6e.y φ Y V 0 ˙
hdmap1l6e.z φ Z V 0 ˙
hdmap1l6e.xn φ ¬ X N Y Z
hdmap1l6.yz φ N Y N Z
hdmap1l6.fg φ I X F Y = G
hdmap1l6.fe φ I X F Z = E
Assertion hdmap1l6lem1 φ M N X - ˙ Y + ˙ Z = L F R G ˙ E

Proof

Step Hyp Ref Expression
1 hdmap1l6.h H = LHyp K
2 hdmap1l6.u U = DVecH K W
3 hdmap1l6.v V = Base U
4 hdmap1l6.p + ˙ = + U
5 hdmap1l6.s - ˙ = - U
6 hdmap1l6c.o 0 ˙ = 0 U
7 hdmap1l6.n N = LSpan U
8 hdmap1l6.c C = LCDual K W
9 hdmap1l6.d D = Base C
10 hdmap1l6.a ˙ = + C
11 hdmap1l6.r R = - C
12 hdmap1l6.q Q = 0 C
13 hdmap1l6.l L = LSpan C
14 hdmap1l6.m M = mapd K W
15 hdmap1l6.i I = HDMap1 K W
16 hdmap1l6.k φ K HL W H
17 hdmap1l6.f φ F D
18 hdmap1l6cl.x φ X V 0 ˙
19 hdmap1l6.mn φ M N X = L F
20 hdmap1l6e.y φ Y V 0 ˙
21 hdmap1l6e.z φ Z V 0 ˙
22 hdmap1l6e.xn φ ¬ X N Y Z
23 hdmap1l6.yz φ N Y N Z
24 hdmap1l6.fg φ I X F Y = G
25 hdmap1l6.fe φ I X F Z = E
26 eqid LSubSp U = LSubSp U
27 1 2 16 dvhlmod φ U LMod
28 18 eldifad φ X V
29 20 eldifad φ Y V
30 3 5 lmodvsubcl U LMod X V Y V X - ˙ Y V
31 27 28 29 30 syl3anc φ X - ˙ Y V
32 3 26 7 lspsncl U LMod X - ˙ Y V N X - ˙ Y LSubSp U
33 27 31 32 syl2anc φ N X - ˙ Y LSubSp U
34 21 eldifad φ Z V
35 3 26 7 lspsncl U LMod Z V N Z LSubSp U
36 27 34 35 syl2anc φ N Z LSubSp U
37 eqid LSSum U = LSSum U
38 26 37 lsmcl U LMod N X - ˙ Y LSubSp U N Z LSubSp U N X - ˙ Y LSSum U N Z LSubSp U
39 27 33 36 38 syl3anc φ N X - ˙ Y LSSum U N Z LSubSp U
40 3 5 lmodvsubcl U LMod X V Z V X - ˙ Z V
41 27 28 34 40 syl3anc φ X - ˙ Z V
42 3 26 7 lspsncl U LMod X - ˙ Z V N X - ˙ Z LSubSp U
43 27 41 42 syl2anc φ N X - ˙ Z LSubSp U
44 3 26 7 lspsncl U LMod Y V N Y LSubSp U
45 27 29 44 syl2anc φ N Y LSubSp U
46 26 37 lsmcl U LMod N X - ˙ Z LSubSp U N Y LSubSp U N X - ˙ Z LSSum U N Y LSubSp U
47 27 43 45 46 syl3anc φ N X - ˙ Z LSSum U N Y LSubSp U
48 1 14 2 26 16 39 47 mapdin φ M N X - ˙ Y LSSum U N Z N X - ˙ Z LSSum U N Y = M N X - ˙ Y LSSum U N Z M N X - ˙ Z LSSum U N Y
49 eqid LSSum C = LSSum C
50 1 14 2 26 37 8 49 16 33 36 mapdlsm φ M N X - ˙ Y LSSum U N Z = M N X - ˙ Y LSSum C M N Z
51 1 14 2 26 37 8 49 16 43 45 mapdlsm φ M N X - ˙ Z LSSum U N Y = M N X - ˙ Z LSSum C M N Y
52 50 51 ineq12d φ M N X - ˙ Y LSSum U N Z M N X - ˙ Z LSSum U N Y = M N X - ˙ Y LSSum C M N Z M N X - ˙ Z LSSum C M N Y
53 1 2 16 dvhlvec φ U LVec
54 3 6 7 53 29 21 28 23 22 lspindp2 φ N X N Y ¬ Z N X Y
55 54 simpld φ N X N Y
56 1 2 3 6 7 8 9 13 14 15 16 17 19 55 18 29 hdmap1cl φ I X F Y D
57 24 56 eqeltrrd φ G D
58 1 2 3 5 6 7 8 9 11 13 14 15 16 18 17 20 57 55 19 hdmap1eq φ I X F Y = G M N Y = L G M N X - ˙ Y = L F R G
59 24 58 mpbid φ M N Y = L G M N X - ˙ Y = L F R G
60 59 simprd φ M N X - ˙ Y = L F R G
61 3 6 7 53 20 34 28 23 22 lspindp1 φ N X N Z ¬ Y N X Z
62 61 simpld φ N X N Z
63 1 2 3 6 7 8 9 13 14 15 16 17 19 62 18 34 hdmap1cl φ I X F Z D
64 25 63 eqeltrrd φ E D
65 1 2 3 5 6 7 8 9 11 13 14 15 16 18 17 21 64 62 19 hdmap1eq φ I X F Z = E M N Z = L E M N X - ˙ Z = L F R E
66 25 65 mpbid φ M N Z = L E M N X - ˙ Z = L F R E
67 66 simpld φ M N Z = L E
68 60 67 oveq12d φ M N X - ˙ Y LSSum C M N Z = L F R G LSSum C L E
69 66 simprd φ M N X - ˙ Z = L F R E
70 59 simpld φ M N Y = L G
71 69 70 oveq12d φ M N X - ˙ Z LSSum C M N Y = L F R E LSSum C L G
72 68 71 ineq12d φ M N X - ˙ Y LSSum C M N Z M N X - ˙ Z LSSum C M N Y = L F R G LSSum C L E L F R E LSSum C L G
73 52 72 eqtrd φ M N X - ˙ Y LSSum U N Z M N X - ˙ Z LSSum U N Y = L F R G LSSum C L E L F R E LSSum C L G
74 48 73 eqtrd φ M N X - ˙ Y LSSum U N Z N X - ˙ Z LSSum U N Y = L F R G LSSum C L E L F R E LSSum C L G
75 3 5 6 37 7 53 28 22 23 20 21 4 baerlem5a φ N X - ˙ Y + ˙ Z = N X - ˙ Y LSSum U N Z N X - ˙ Z LSSum U N Y
76 75 fveq2d φ M N X - ˙ Y + ˙ Z = M N X - ˙ Y LSSum U N Z N X - ˙ Z LSSum U N Y
77 1 8 16 lcdlvec φ C LVec
78 1 14 2 3 7 8 9 13 16 17 19 28 29 57 70 34 64 67 22 mapdindp φ ¬ F L G E
79 1 14 2 3 7 8 9 13 16 57 70 29 34 64 67 23 mapdncol φ L G L E
80 1 14 2 3 7 8 9 13 16 57 70 6 12 20 mapdn0 φ G D Q
81 1 14 2 3 7 8 9 13 16 64 67 6 12 21 mapdn0 φ E D Q
82 9 11 12 49 13 77 17 78 79 80 81 10 baerlem5a φ L F R G ˙ E = L F R G LSSum C L E L F R E LSSum C L G
83 74 76 82 3eqtr4d φ M N X - ˙ Y + ˙ Z = L F R G ˙ E