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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmaprnlem15.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem15.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmaprnlem15.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
hdmaprnlem15.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem15.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
hdmaprnlem15.q ⊢ 0 = ( 0g ‘ 𝐶 )
hdmaprnlem15.l ⊢ 𝐿 = ( LSpan ‘ 𝐶 )
hdmaprnlem15.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem15.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem15.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmaprnlem15.se ⊢ ( 𝜑 → 𝑠 ∈ ( 𝐷 ∖ { 0 } ) )
hdmaprnlem15.ve ⊢ ( 𝜑 → 𝑣 ∈ 𝑉 )
hdmaprnlem15.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
Assertion hdmaprnlem15N ( 𝜑 → 𝑠 ∈ ran 𝑆 )

Proof

Step Hyp Ref Expression
1 hdmaprnlem15.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmaprnlem15.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmaprnlem15.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmaprnlem15.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5 hdmaprnlem15.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 hdmaprnlem15.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
7 hdmaprnlem15.q ⊢ 0 = ( 0g ‘ 𝐶 )
8 hdmaprnlem15.l ⊢ 𝐿 = ( LSpan ‘ 𝐶 )
9 hdmaprnlem15.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
10 hdmaprnlem15.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11 hdmaprnlem15.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 hdmaprnlem15.se ⊢ ( 𝜑 → 𝑠 ∈ ( 𝐷 ∖ { 0 } ) )
13 hdmaprnlem15.ve ⊢ ( 𝜑 → 𝑣 ∈ 𝑉 )
14 hdmaprnlem15.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
15 1 2 3 4 11 13 dvh2dim ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑉 ¬ 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) )
16 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ∧ ¬ 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ∧ ¬ 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) ) → 𝑠 ∈ ( 𝐷 ∖ { 0 } ) )
18 13 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ∧ ¬ 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) ) → 𝑣 ∈ 𝑉 )
19 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ∧ ¬ 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
20 simp2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ∧ ¬ 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) ) → 𝑡 ∈ 𝑉 )
21 simp3 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ∧ ¬ 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) ) → ¬ 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) )
22 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
23 eqid ⊢ ( +g ‘ 𝐶 ) = ( +g ‘ 𝐶 )
24 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
25 1 2 3 4 5 8 9 10 16 17 18 19 20 21 6 7 22 23 24 hdmaprnlem11N ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ∧ ¬ 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) ) → 𝑠 ∈ ran 𝑆 )
26 25 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝑉 ¬ 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) → 𝑠 ∈ ran 𝑆 ) )
27 15 26 mpd ⊢ ( 𝜑 → 𝑠 ∈ ran 𝑆 )