Metamath Proof Explorer

Theorem mapdh6lem1N

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

Ref Expression
Hypotheses mapdh.q ⊢ Q = 0 C
mapdh.i ⊢ I = x ∈ V ⟼ if 2 nd ⁡ x = 0 ˙ Q ι h ∈ D | M ⁡ N ⁡ 2 nd ⁡ x = J ⁡ h ∧ M ⁡ N ⁡ 1 st ⁡ 1 st ⁡ x - ˙ 2 nd ⁡ x = J ⁡ 2 nd ⁡ 1 st ⁡ x R h
mapdh.h ⊢ H = LHyp ⁡ K
mapdh.m ⊢ M = mapd ⁡ K ⁡ W
mapdh.u ⊢ U = DVecH ⁡ K ⁡ W
mapdh.v ⊢ V = Base U
mapdh.s ⊢ - ˙ = - U
mapdhc.o ⊢ 0 ˙ = 0 U
mapdh.n ⊢ N = LSpan ⁡ U
mapdh.c ⊢ C = LCDual ⁡ K ⁡ W
mapdh.d ⊢ D = Base C
mapdh.r ⊢ R = - C
mapdh.j ⊢ J = LSpan ⁡ C
mapdh.k ⊢ φ → K ∈ HL ∧ W ∈ H
mapdhc.f ⊢ φ → F ∈ D
mapdh.mn ⊢ φ → M ⁡ N ⁡ X = J ⁡ F
mapdhcl.x ⊢ φ → X ∈ V ∖ 0 ˙
mapdh.p ⊢ + ˙ = + U
mapdh.a ⊢ ✚ ˙ = + C
mapdhe6.y ⊢ φ → Y ∈ V ∖ 0 ˙
mapdhe6.z ⊢ φ → Z ∈ V ∖ 0 ˙
mapdhe6.xn ⊢ φ → ¬ X ∈ N ⁡ Y Z
mapdh6.yz ⊢ φ → N ⁡ Y ≠ N ⁡ Z
mapdh6.fg ⊢ φ → I ⁡ X F Y = G
mapdh6.fe ⊢ φ → I ⁡ X F Z = E
Assertion mapdh6lem1N ⊢ φ → M ⁡ N ⁡ X - ˙ Y + ˙ Z = J ⁡ F R G ✚ ˙ E

Proof

Step Hyp Ref Expression
1 mapdh.q ⊢ Q = 0 C
2 mapdh.i ⊢ I = x ∈ V ⟼ if 2 nd ⁡ x = 0 ˙ Q ι h ∈ D | M ⁡ N ⁡ 2 nd ⁡ x = J ⁡ h ∧ M ⁡ N ⁡ 1 st ⁡ 1 st ⁡ x - ˙ 2 nd ⁡ x = J ⁡ 2 nd ⁡ 1 st ⁡ x R h
3 mapdh.h ⊢ H = LHyp ⁡ K
4 mapdh.m ⊢ M = mapd ⁡ K ⁡ W
5 mapdh.u ⊢ U = DVecH ⁡ K ⁡ W
6 mapdh.v ⊢ V = Base U
7 mapdh.s ⊢ - ˙ = - U
8 mapdhc.o ⊢ 0 ˙ = 0 U
9 mapdh.n ⊢ N = LSpan ⁡ U
10 mapdh.c ⊢ C = LCDual ⁡ K ⁡ W
11 mapdh.d ⊢ D = Base C
12 mapdh.r ⊢ R = - C
13 mapdh.j ⊢ J = LSpan ⁡ C
14 mapdh.k ⊢ φ → K ∈ HL ∧ W ∈ H
15 mapdhc.f ⊢ φ → F ∈ D
16 mapdh.mn ⊢ φ → M ⁡ N ⁡ X = J ⁡ F
17 mapdhcl.x ⊢ φ → X ∈ V ∖ 0 ˙
18 mapdh.p ⊢ + ˙ = + U
19 mapdh.a ⊢ ✚ ˙ = + C
20 mapdhe6.y ⊢ φ → Y ∈ V ∖ 0 ˙
21 mapdhe6.z ⊢ φ → Z ∈ V ∖ 0 ˙
22 mapdhe6.xn ⊢ φ → ¬ X ∈ N ⁡ Y Z
23 mapdh6.yz ⊢ φ → N ⁡ Y ≠ N ⁡ Z
24 mapdh6.fg ⊢ φ → I ⁡ X F Y = G
25 mapdh6.fe ⊢ φ → I ⁡ X F Z = E
26 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
27 3 5 14 dvhlmod ⊢ φ → U ∈ LMod
28 17 eldifad ⊢ φ → X ∈ V
29 20 eldifad ⊢ φ → Y ∈ V
30 6 7 lmodvsubcl ⊢ U ∈ LMod ∧ X ∈ V ∧ Y ∈ V → X - ˙ Y ∈ V
31 27 28 29 30 syl3anc ⊢ φ → X - ˙ Y ∈ V
32 6 26 9 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 6 26 9 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 6 7 lmodvsubcl ⊢ U ∈ LMod ∧ X ∈ V ∧ Z ∈ V → X - ˙ Z ∈ V
41 27 28 34 40 syl3anc ⊢ φ → X - ˙ Z ∈ V
42 6 26 9 lspsncl ⊢ U ∈ LMod ∧ X - ˙ Z ∈ V → N ⁡ X - ˙ Z ∈ LSubSp ⁡ U
43 27 41 42 syl2anc ⊢ φ → N ⁡ X - ˙ Z ∈ LSubSp ⁡ U
44 6 26 9 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 3 4 5 26 14 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 3 4 5 26 37 10 49 14 33 36 mapdlsm ⊢ φ → M ⁡ N ⁡ X - ˙ Y LSSum ⁡ U N ⁡ Z = M ⁡ N ⁡ X - ˙ Y LSSum ⁡ C M ⁡ N ⁡ Z
51 3 4 5 26 37 10 49 14 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 3 5 14 dvhlvec ⊢ φ → U ∈ LVec
54 6 8 9 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 4 5 6 7 8 9 10 11 12 13 14 15 16 17 29 55 mapdhcl ⊢ φ → I ⁡ X F Y ∈ D
57 24 56 eqeltrrd ⊢ φ → G ∈ D
58 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 20 57 55 mapdheq ⊢ φ → I ⁡ X F Y = G ↔ M ⁡ N ⁡ Y = J ⁡ G ∧ M ⁡ N ⁡ X - ˙ Y = J ⁡ F R G
59 24 58 mpbid ⊢ φ → M ⁡ N ⁡ Y = J ⁡ G ∧ M ⁡ N ⁡ X - ˙ Y = J ⁡ F R G
60 59 simprd ⊢ φ → M ⁡ N ⁡ X - ˙ Y = J ⁡ F R G
61 6 8 9 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 4 5 6 7 8 9 10 11 12 13 14 15 16 17 34 62 mapdhcl ⊢ φ → I ⁡ X F Z ∈ D
64 25 63 eqeltrrd ⊢ φ → E ∈ D
65 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 21 64 62 mapdheq ⊢ φ → I ⁡ X F Z = E ↔ M ⁡ N ⁡ Z = J ⁡ E ∧ M ⁡ N ⁡ X - ˙ Z = J ⁡ F R E
66 25 65 mpbid ⊢ φ → M ⁡ N ⁡ Z = J ⁡ E ∧ M ⁡ N ⁡ X - ˙ Z = J ⁡ F R E
67 66 simpld ⊢ φ → M ⁡ N ⁡ Z = J ⁡ E
68 60 67 oveq12d ⊢ φ → M ⁡ N ⁡ X - ˙ Y LSSum ⁡ C M ⁡ N ⁡ Z = J ⁡ F R G LSSum ⁡ C J ⁡ E
69 66 simprd ⊢ φ → M ⁡ N ⁡ X - ˙ Z = J ⁡ F R E
70 59 simpld ⊢ φ → M ⁡ N ⁡ Y = J ⁡ G
71 69 70 oveq12d ⊢ φ → M ⁡ N ⁡ X - ˙ Z LSSum ⁡ C M ⁡ N ⁡ Y = J ⁡ F R E LSSum ⁡ C J ⁡ G
72 68 71 ineq12d ⊢ φ → M ⁡ N ⁡ X - ˙ Y LSSum ⁡ C M ⁡ N ⁡ Z ∩ M ⁡ N ⁡ X - ˙ Z LSSum ⁡ C M ⁡ N ⁡ Y = J ⁡ F R G LSSum ⁡ C J ⁡ E ∩ J ⁡ F R E LSSum ⁡ C J ⁡ G
73 52 72 eqtrd ⊢ φ → M ⁡ N ⁡ X - ˙ Y LSSum ⁡ U N ⁡ Z ∩ M ⁡ N ⁡ X - ˙ Z LSSum ⁡ U N ⁡ Y = J ⁡ F R G LSSum ⁡ C J ⁡ E ∩ J ⁡ F R E LSSum ⁡ C J ⁡ G
74 48 73 eqtrd ⊢ φ → M ⁡ N ⁡ X - ˙ Y LSSum ⁡ U N ⁡ Z ∩ N ⁡ X - ˙ Z LSSum ⁡ U N ⁡ Y = J ⁡ F R G LSSum ⁡ C J ⁡ E ∩ J ⁡ F R E LSSum ⁡ C J ⁡ G
75 6 7 8 37 9 53 28 22 23 20 21 18 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 3 10 14 lcdlvec ⊢ φ → C ∈ LVec
78 3 4 5 6 9 10 11 13 14 15 16 28 29 57 70 34 64 67 22 mapdindp ⊢ φ → ¬ F ∈ J ⁡ G E
79 3 4 5 6 9 10 11 13 14 57 70 29 34 64 67 23 mapdncol ⊢ φ → J ⁡ G ≠ J ⁡ E
80 3 4 5 6 9 10 11 13 14 57 70 8 1 20 mapdn0 ⊢ φ → G ∈ D ∖ Q
81 3 4 5 6 9 10 11 13 14 64 67 8 1 21 mapdn0 ⊢ φ → E ∈ D ∖ Q
82 11 12 1 49 13 77 15 78 79 80 81 19 baerlem5a ⊢ φ → J ⁡ F R G ✚ ˙ E = J ⁡ F R G LSSum ⁡ C J ⁡ E ∩ J ⁡ F R E LSSum ⁡ C J ⁡ G
83 74 76 82 3eqtr4d ⊢ φ → M ⁡ N ⁡ X - ˙ Y + ˙ Z = J ⁡ F R G ✚ ˙ E