Metamath Proof Explorer

Theorem hdmaprnlem15N

Description: Lemma for hdmaprnN . Eliminate u . (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
hdmaprnlem15.se ⊢ φ → s ∈ D ∖ 0 ˙
hdmaprnlem15.ve ⊢ φ → v ∈ V
hdmaprnlem15.e ⊢ φ → M ⁡ N ⁡ v = L ⁡ s
Assertion hdmaprnlem15N ⊢ φ → 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 hdmaprnlem15.se ⊢ φ → s ∈ D ∖ 0 ˙
13 hdmaprnlem15.ve ⊢ φ → v ∈ V
14 hdmaprnlem15.e ⊢ φ → M ⁡ N ⁡ v = L ⁡ s
15 1 2 3 4 11 13 dvh2dim ⊢ φ → ∃ t ∈ V ¬ t ∈ N ⁡ v
16 11 3ad2ant1 ⊢ φ ∧ t ∈ V ∧ ¬ t ∈ N ⁡ v → K ∈ HL ∧ W ∈ H
17 12 3ad2ant1 ⊢ φ ∧ t ∈ V ∧ ¬ t ∈ N ⁡ v → s ∈ D ∖ 0 ˙
18 13 3ad2ant1 ⊢ φ ∧ t ∈ V ∧ ¬ t ∈ N ⁡ v → v ∈ V
19 14 3ad2ant1 ⊢ φ ∧ t ∈ V ∧ ¬ t ∈ N ⁡ v → M ⁡ N ⁡ v = L ⁡ s
20 simp2 ⊢ φ ∧ t ∈ V ∧ ¬ t ∈ N ⁡ v → t ∈ V
21 simp3 ⊢ φ ∧ t ∈ V ∧ ¬ t ∈ N ⁡ v → ¬ t ∈ N ⁡ v
22 eqid ⊢ 0 U = 0 U
23 eqid ⊢ + C = + C
24 eqid ⊢ + U = + U
25 1 2 3 4 5 8 9 10 16 17 18 19 20 21 6 7 22 23 24 hdmaprnlem11N ⊢ φ ∧ t ∈ V ∧ ¬ t ∈ N ⁡ v → s ∈ ran ⁡ S
26 25 rexlimdv3a ⊢ φ → ∃ t ∈ V ¬ t ∈ N ⁡ v → s ∈ ran ⁡ S
27 15 26 mpd ⊢ φ → s ∈ ran ⁡ S