Metamath Proof Explorer

Theorem hdmaprnlem16N

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

Ref Expression
Hypotheses hdmaprnlem15.h ⊢ H = LHyp ⁡ K
hdmaprnlem15.u ⊢ U = DVecH ⁡ K ⁡ W
hdmaprnlem15.v ⊢ V = Base U
hdmaprnlem15.n ⊢ N = LSpan ⁡ U
hdmaprnlem15.c ⊢ C = LCDual ⁡ K ⁡ W
hdmaprnlem15.d ⊢ D = Base C
hdmaprnlem15.q ⊢ 0 ˙ = 0 C
hdmaprnlem15.l ⊢ L = LSpan ⁡ C
hdmaprnlem15.m ⊢ M = mapd ⁡ K ⁡ W
hdmaprnlem15.s ⊢ S = HDMap ⁡ K ⁡ W
hdmaprnlem15.k ⊢ φ → K ∈ HL ∧ W ∈ H
hdmaprnlem16.se ⊢ φ → s ∈ D ∖ 0 ˙
Assertion hdmaprnlem16N ⊢ φ → s ∈ ran ⁡ S

Proof

Step Hyp Ref Expression
1 hdmaprnlem15.h ⊢ H = LHyp ⁡ K
2 hdmaprnlem15.u ⊢ U = DVecH ⁡ K ⁡ W
3 hdmaprnlem15.v ⊢ V = Base U
4 hdmaprnlem15.n ⊢ N = LSpan ⁡ U
5 hdmaprnlem15.c ⊢ C = LCDual ⁡ K ⁡ W
6 hdmaprnlem15.d ⊢ D = Base C
7 hdmaprnlem15.q ⊢ 0 ˙ = 0 C
8 hdmaprnlem15.l ⊢ L = LSpan ⁡ C
9 hdmaprnlem15.m ⊢ M = mapd ⁡ K ⁡ W
10 hdmaprnlem15.s ⊢ S = HDMap ⁡ K ⁡ W
11 hdmaprnlem15.k ⊢ φ → K ∈ HL ∧ W ∈ H
12 hdmaprnlem16.se ⊢ φ → s ∈ D ∖ 0 ˙
13 1 2 11 dvhlmod ⊢ φ → U ∈ LMod
14 eqid ⊢ LSAtoms ⁡ U = LSAtoms ⁡ U
15 eqid ⊢ LSAtoms ⁡ C = LSAtoms ⁡ C
16 1 5 11 lcdlmod ⊢ φ → C ∈ LMod
17 6 8 7 15 16 12 lsatlspsn ⊢ φ → L ⁡ s ∈ LSAtoms ⁡ C
18 1 9 2 14 5 15 11 17 mapdcnvatN ⊢ φ → M -1 ⁡ L ⁡ s ∈ LSAtoms ⁡ U
19 3 4 14 islsati ⊢ U ∈ LMod ∧ M -1 ⁡ L ⁡ s ∈ LSAtoms ⁡ U → ∃ v ∈ V M -1 ⁡ L ⁡ s = N ⁡ v
20 13 18 19 syl2anc ⊢ φ → ∃ v ∈ V M -1 ⁡ L ⁡ s = N ⁡ v
21 simpr ⊢ φ ∧ v ∈ V ∧ M -1 ⁡ L ⁡ s = N ⁡ v → M -1 ⁡ L ⁡ s = N ⁡ v
22 21 fveq2d ⊢ φ ∧ v ∈ V ∧ M -1 ⁡ L ⁡ s = N ⁡ v → M ⁡ M -1 ⁡ L ⁡ s = M ⁡ N ⁡ v
23 11 ad2antrr ⊢ φ ∧ v ∈ V ∧ M -1 ⁡ L ⁡ s = N ⁡ v → K ∈ HL ∧ W ∈ H
24 12 eldifad ⊢ φ → s ∈ D
25 eqid ⊢ LSubSp ⁡ C = LSubSp ⁡ C
26 6 25 8 lspsncl ⊢ C ∈ LMod ∧ s ∈ D → L ⁡ s ∈ LSubSp ⁡ C
27 16 24 26 syl2anc ⊢ φ → L ⁡ s ∈ LSubSp ⁡ C
28 1 9 5 25 11 mapdrn2 ⊢ φ → ran ⁡ M = LSubSp ⁡ C
29 27 28 eleqtrrd ⊢ φ → L ⁡ s ∈ ran ⁡ M
30 29 ad2antrr ⊢ φ ∧ v ∈ V ∧ M -1 ⁡ L ⁡ s = N ⁡ v → L ⁡ s ∈ ran ⁡ M
31 1 9 23 30 mapdcnvid2 ⊢ φ ∧ v ∈ V ∧ M -1 ⁡ L ⁡ s = N ⁡ v → M ⁡ M -1 ⁡ L ⁡ s = L ⁡ s
32 22 31 eqtr3d ⊢ φ ∧ v ∈ V ∧ M -1 ⁡ L ⁡ s = N ⁡ v → M ⁡ N ⁡ v = L ⁡ s
33 32 ex ⊢ φ ∧ v ∈ V → M -1 ⁡ L ⁡ s = N ⁡ v → M ⁡ N ⁡ v = L ⁡ s
34 33 reximdva ⊢ φ → ∃ v ∈ V M -1 ⁡ L ⁡ s = N ⁡ v → ∃ v ∈ V M ⁡ N ⁡ v = L ⁡ s
35 20 34 mpd ⊢ φ → ∃ v ∈ V M ⁡ N ⁡ v = L ⁡ s
36 11 3ad2ant1 ⊢ φ ∧ v ∈ V ∧ M ⁡ N ⁡ v = L ⁡ s → K ∈ HL ∧ W ∈ H
37 12 3ad2ant1 ⊢ φ ∧ v ∈ V ∧ M ⁡ N ⁡ v = L ⁡ s → s ∈ D ∖ 0 ˙
38 simp2 ⊢ φ ∧ v ∈ V ∧ M ⁡ N ⁡ v = L ⁡ s → v ∈ V
39 simp3 ⊢ φ ∧ v ∈ V ∧ M ⁡ N ⁡ v = L ⁡ s → M ⁡ N ⁡ v = L ⁡ s
40 1 2 3 4 5 6 7 8 9 10 36 37 38 39 hdmaprnlem15N ⊢ φ ∧ v ∈ V ∧ M ⁡ N ⁡ v = L ⁡ s → s ∈ ran ⁡ S
41 40 rexlimdv3a ⊢ φ → ∃ v ∈ V M ⁡ N ⁡ v = L ⁡ s → s ∈ ran ⁡ S
42 35 41 mpd ⊢ φ → s ∈ ran ⁡ S