Metamath Proof Explorer

Theorem hdmaprnlem3eN

Description: Lemma for hdmaprnN . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmaprnlem1.h ⊢ H = LHyp ⁡ K
hdmaprnlem1.u ⊢ U = DVecH ⁡ K ⁡ W
hdmaprnlem1.v ⊢ V = Base U
hdmaprnlem1.n ⊢ N = LSpan ⁡ U
hdmaprnlem1.c ⊢ C = LCDual ⁡ K ⁡ W
hdmaprnlem1.l ⊢ L = LSpan ⁡ C
hdmaprnlem1.m ⊢ M = mapd ⁡ K ⁡ W
hdmaprnlem1.s ⊢ S = HDMap ⁡ K ⁡ W
hdmaprnlem1.k ⊢ φ → K ∈ HL ∧ W ∈ H
hdmaprnlem1.se ⊢ φ → s ∈ D ∖ Q
hdmaprnlem1.ve ⊢ φ → v ∈ V
hdmaprnlem1.e ⊢ φ → M ⁡ N ⁡ v = L ⁡ s
hdmaprnlem1.ue ⊢ φ → u ∈ V
hdmaprnlem1.un ⊢ φ → ¬ u ∈ N ⁡ v
hdmaprnlem1.d ⊢ D = Base C
hdmaprnlem1.q ⊢ Q = 0 C
hdmaprnlem1.o ⊢ 0 ˙ = 0 U
hdmaprnlem1.a ⊢ ✚ ˙ = + C
hdmaprnlem3e.p ⊢ + ˙ = + U
Assertion hdmaprnlem3eN ⊢ φ → ∃ t ∈ N ⁡ v ∖ 0 ˙ L ⁡ S ⁡ u ✚ ˙ s = M ⁡ N ⁡ u + ˙ t

Proof

Step Hyp Ref Expression
1 hdmaprnlem1.h ⊢ H = LHyp ⁡ K
2 hdmaprnlem1.u ⊢ U = DVecH ⁡ K ⁡ W
3 hdmaprnlem1.v ⊢ V = Base U
4 hdmaprnlem1.n ⊢ N = LSpan ⁡ U
5 hdmaprnlem1.c ⊢ C = LCDual ⁡ K ⁡ W
6 hdmaprnlem1.l ⊢ L = LSpan ⁡ C
7 hdmaprnlem1.m ⊢ M = mapd ⁡ K ⁡ W
8 hdmaprnlem1.s ⊢ S = HDMap ⁡ K ⁡ W
9 hdmaprnlem1.k ⊢ φ → K ∈ HL ∧ W ∈ H
10 hdmaprnlem1.se ⊢ φ → s ∈ D ∖ Q
11 hdmaprnlem1.ve ⊢ φ → v ∈ V
12 hdmaprnlem1.e ⊢ φ → M ⁡ N ⁡ v = L ⁡ s
13 hdmaprnlem1.ue ⊢ φ → u ∈ V
14 hdmaprnlem1.un ⊢ φ → ¬ u ∈ N ⁡ v
15 hdmaprnlem1.d ⊢ D = Base C
16 hdmaprnlem1.q ⊢ Q = 0 C
17 hdmaprnlem1.o ⊢ 0 ˙ = 0 U
18 hdmaprnlem1.a ⊢ ✚ ˙ = + C
19 hdmaprnlem3e.p ⊢ + ˙ = + U
20 eqid ⊢ LSAtoms ⁡ U = LSAtoms ⁡ U
21 1 2 9 dvhlvec ⊢ φ → U ∈ LVec
22 eqid ⊢ LSAtoms ⁡ C = LSAtoms ⁡ C
23 1 5 9 lcdlmod ⊢ φ → C ∈ LMod
24 1 2 3 5 15 8 9 13 hdmapcl ⊢ φ → S ⁡ u ∈ D
25 10 eldifad ⊢ φ → s ∈ D
26 15 18 lmodvacl ⊢ C ∈ LMod ∧ S ⁡ u ∈ D ∧ s ∈ D → S ⁡ u ✚ ˙ s ∈ D
27 23 24 25 26 syl3anc ⊢ φ → S ⁡ u ✚ ˙ s ∈ D
28 1 2 3 4 5 6 7 8 9 10 11 12 13 14 hdmaprnlem1N ⊢ φ → L ⁡ S ⁡ u ≠ L ⁡ s
29 15 18 16 6 23 24 25 28 lmodindp1 ⊢ φ → S ⁡ u ✚ ˙ s ≠ Q
30 eldifsn ⊢ S ⁡ u ✚ ˙ s ∈ D ∖ Q ↔ S ⁡ u ✚ ˙ s ∈ D ∧ S ⁡ u ✚ ˙ s ≠ Q
31 27 29 30 sylanbrc ⊢ φ → S ⁡ u ✚ ˙ s ∈ D ∖ Q
32 15 6 16 22 23 31 lsatlspsn ⊢ φ → L ⁡ S ⁡ u ✚ ˙ s ∈ LSAtoms ⁡ C
33 1 7 2 20 5 22 9 32 mapdcnvatN ⊢ φ → M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s ∈ LSAtoms ⁡ U
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hdmaprnlem3uN ⊢ φ → N ⁡ u ≠ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s
35 34 necomd ⊢ φ → M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s ≠ N ⁡ u
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hdmaprnlem3N ⊢ φ → N ⁡ v ≠ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s
37 36 necomd ⊢ φ → M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s ≠ N ⁡ v
38 eqid ⊢ LSubSp ⁡ C = LSubSp ⁡ C
39 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
40 1 2 9 dvhlmod ⊢ φ → U ∈ LMod
41 3 39 4 lspsncl ⊢ U ∈ LMod ∧ u ∈ V → N ⁡ u ∈ LSubSp ⁡ U
42 40 13 41 syl2anc ⊢ φ → N ⁡ u ∈ LSubSp ⁡ U
43 1 7 2 39 5 38 9 42 mapdcl2 ⊢ φ → M ⁡ N ⁡ u ∈ LSubSp ⁡ C
44 3 39 4 lspsncl ⊢ U ∈ LMod ∧ v ∈ V → N ⁡ v ∈ LSubSp ⁡ U
45 40 11 44 syl2anc ⊢ φ → N ⁡ v ∈ LSubSp ⁡ U
46 1 7 2 39 5 38 9 45 mapdcl2 ⊢ φ → M ⁡ N ⁡ v ∈ LSubSp ⁡ C
47 eqid ⊢ LSSum ⁡ C = LSSum ⁡ C
48 38 47 lsmcl ⊢ C ∈ LMod ∧ M ⁡ N ⁡ u ∈ LSubSp ⁡ C ∧ M ⁡ N ⁡ v ∈ LSubSp ⁡ C → M ⁡ N ⁡ u LSSum ⁡ C M ⁡ N ⁡ v ∈ LSubSp ⁡ C
49 23 43 46 48 syl3anc ⊢ φ → M ⁡ N ⁡ u LSSum ⁡ C M ⁡ N ⁡ v ∈ LSubSp ⁡ C
50 38 lsssssubg ⊢ C ∈ LMod → LSubSp ⁡ C ⊆ SubGrp ⁡ C
51 23 50 syl ⊢ φ → LSubSp ⁡ C ⊆ SubGrp ⁡ C
52 51 43 sseldd ⊢ φ → M ⁡ N ⁡ u ∈ SubGrp ⁡ C
53 51 46 sseldd ⊢ φ → M ⁡ N ⁡ v ∈ SubGrp ⁡ C
54 15 6 lspsnid ⊢ C ∈ LMod ∧ S ⁡ u ∈ D → S ⁡ u ∈ L ⁡ S ⁡ u
55 23 24 54 syl2anc ⊢ φ → S ⁡ u ∈ L ⁡ S ⁡ u
56 1 2 3 4 5 6 7 8 9 13 hdmap10 ⊢ φ → M ⁡ N ⁡ u = L ⁡ S ⁡ u
57 55 56 eleqtrrd ⊢ φ → S ⁡ u ∈ M ⁡ N ⁡ u
58 eqimss2 ⊢ M ⁡ N ⁡ v = L ⁡ s → L ⁡ s ⊆ M ⁡ N ⁡ v
59 12 58 syl ⊢ φ → L ⁡ s ⊆ M ⁡ N ⁡ v
60 15 38 6 23 46 25 ellspsn5b ⊢ φ → s ∈ M ⁡ N ⁡ v ↔ L ⁡ s ⊆ M ⁡ N ⁡ v
61 59 60 mpbird ⊢ φ → s ∈ M ⁡ N ⁡ v
62 18 47 lsmelvali ⊢ M ⁡ N ⁡ u ∈ SubGrp ⁡ C ∧ M ⁡ N ⁡ v ∈ SubGrp ⁡ C ∧ S ⁡ u ∈ M ⁡ N ⁡ u ∧ s ∈ M ⁡ N ⁡ v → S ⁡ u ✚ ˙ s ∈ M ⁡ N ⁡ u LSSum ⁡ C M ⁡ N ⁡ v
63 52 53 57 61 62 syl22anc ⊢ φ → S ⁡ u ✚ ˙ s ∈ M ⁡ N ⁡ u LSSum ⁡ C M ⁡ N ⁡ v
64 38 6 23 49 63 ellspsn5 ⊢ φ → L ⁡ S ⁡ u ✚ ˙ s ⊆ M ⁡ N ⁡ u LSSum ⁡ C M ⁡ N ⁡ v
65 eqid ⊢ LSSum ⁡ U = LSSum ⁡ U
66 1 7 2 39 65 5 47 9 42 45 mapdlsm ⊢ φ → M ⁡ N ⁡ u LSSum ⁡ U N ⁡ v = M ⁡ N ⁡ u LSSum ⁡ C M ⁡ N ⁡ v
67 64 66 sseqtrrd ⊢ φ → L ⁡ S ⁡ u ✚ ˙ s ⊆ M ⁡ N ⁡ u LSSum ⁡ U N ⁡ v
68 15 38 6 lspsncl ⊢ C ∈ LMod ∧ S ⁡ u ✚ ˙ s ∈ D → L ⁡ S ⁡ u ✚ ˙ s ∈ LSubSp ⁡ C
69 23 27 68 syl2anc ⊢ φ → L ⁡ S ⁡ u ✚ ˙ s ∈ LSubSp ⁡ C
70 1 7 5 38 9 mapdrn2 ⊢ φ → ran ⁡ M = LSubSp ⁡ C
71 69 70 eleqtrrd ⊢ φ → L ⁡ S ⁡ u ✚ ˙ s ∈ ran ⁡ M
72 39 65 lsmcl ⊢ U ∈ LMod ∧ N ⁡ u ∈ LSubSp ⁡ U ∧ N ⁡ v ∈ LSubSp ⁡ U → N ⁡ u LSSum ⁡ U N ⁡ v ∈ LSubSp ⁡ U
73 40 42 45 72 syl3anc ⊢ φ → N ⁡ u LSSum ⁡ U N ⁡ v ∈ LSubSp ⁡ U
74 1 7 2 39 9 73 mapdcl ⊢ φ → M ⁡ N ⁡ u LSSum ⁡ U N ⁡ v ∈ ran ⁡ M
75 1 7 9 71 74 mapdcnvordN ⊢ φ → M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s ⊆ M -1 ⁡ M ⁡ N ⁡ u LSSum ⁡ U N ⁡ v ↔ L ⁡ S ⁡ u ✚ ˙ s ⊆ M ⁡ N ⁡ u LSSum ⁡ U N ⁡ v
76 67 75 mpbird ⊢ φ → M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s ⊆ M -1 ⁡ M ⁡ N ⁡ u LSSum ⁡ U N ⁡ v
77 3 4 65 40 13 11 lsmpr ⊢ φ → N ⁡ u v = N ⁡ u LSSum ⁡ U N ⁡ v
78 1 7 2 39 9 73 mapdcnvid1N ⊢ φ → M -1 ⁡ M ⁡ N ⁡ u LSSum ⁡ U N ⁡ v = N ⁡ u LSSum ⁡ U N ⁡ v
79 77 78 eqtr4d ⊢ φ → N ⁡ u v = M -1 ⁡ M ⁡ N ⁡ u LSSum ⁡ U N ⁡ v
80 76 79 sseqtrrd ⊢ φ → M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s ⊆ N ⁡ u v
81 3 19 17 4 20 21 33 13 11 35 37 80 lsatfixedN ⊢ φ → ∃ t ∈ N ⁡ v ∖ 0 ˙ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t
82 simpr ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t
83 9 ad2antrr ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → K ∈ HL ∧ W ∈ H
84 40 ad2antrr ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → U ∈ LMod
85 13 ad2antrr ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → u ∈ V
86 10 ad2antrr ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → s ∈ D ∖ Q
87 11 ad2antrr ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → v ∈ V
88 12 ad2antrr ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → M ⁡ N ⁡ v = L ⁡ s
89 14 ad2antrr ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → ¬ u ∈ N ⁡ v
90 simplr ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → t ∈ N ⁡ v ∖ 0 ˙
91 1 2 3 4 5 6 7 8 83 86 87 88 85 89 15 16 17 18 90 hdmaprnlem4tN ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → t ∈ V
92 3 19 lmodvacl ⊢ U ∈ LMod ∧ u ∈ V ∧ t ∈ V → u + ˙ t ∈ V
93 84 85 91 92 syl3anc ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → u + ˙ t ∈ V
94 3 39 4 lspsncl ⊢ U ∈ LMod ∧ u + ˙ t ∈ V → N ⁡ u + ˙ t ∈ LSubSp ⁡ U
95 84 93 94 syl2anc ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → N ⁡ u + ˙ t ∈ LSubSp ⁡ U
96 1 7 2 39 83 95 mapdcnvid1N ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → M -1 ⁡ M ⁡ N ⁡ u + ˙ t = N ⁡ u + ˙ t
97 82 96 eqtr4d ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = M -1 ⁡ M ⁡ N ⁡ u + ˙ t
98 71 ad2antrr ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → L ⁡ S ⁡ u ✚ ˙ s ∈ ran ⁡ M
99 1 7 2 39 83 95 mapdcl ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → M ⁡ N ⁡ u + ˙ t ∈ ran ⁡ M
100 1 7 83 98 99 mapdcnv11N ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = M -1 ⁡ M ⁡ N ⁡ u + ˙ t ↔ L ⁡ S ⁡ u ✚ ˙ s = M ⁡ N ⁡ u + ˙ t
101 97 100 mpbid ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ ∧ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → L ⁡ S ⁡ u ✚ ˙ s = M ⁡ N ⁡ u + ˙ t
102 101 ex ⊢ φ ∧ t ∈ N ⁡ v ∖ 0 ˙ → M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → L ⁡ S ⁡ u ✚ ˙ s = M ⁡ N ⁡ u + ˙ t
103 102 reximdva ⊢ φ → ∃ t ∈ N ⁡ v ∖ 0 ˙ M -1 ⁡ L ⁡ S ⁡ u ✚ ˙ s = N ⁡ u + ˙ t → ∃ t ∈ N ⁡ v ∖ 0 ˙ L ⁡ S ⁡ u ✚ ˙ s = M ⁡ N ⁡ u + ˙ t
104 81 103 mpd ⊢ φ → ∃ t ∈ N ⁡ v ∖ 0 ˙ L ⁡ S ⁡ u ✚ ˙ s = M ⁡ N ⁡ u + ˙ t