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 ⊢ 𝐻 = ( 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 ∧ 𝑊 ∈ 𝐻 ) )
hdmaprnlem16.se ⊢ ( 𝜑 → 𝑠 ∈ ( 𝐷 ∖ { 0 } ) )
Assertion hdmaprnlem16N ( 𝜑 → 𝑠 ∈ 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 hdmaprnlem16.se ⊢ ( 𝜑 → 𝑠 ∈ ( 𝐷 ∖ { 0 } ) )
13 1 2 11 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
14 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
15 eqid ⊢ ( LSAtoms ‘ 𝐶 ) = ( LSAtoms ‘ 𝐶 )
16 1 5 11 lcdlmod ⊢ ( 𝜑 → 𝐶 ∈ LMod )
17 6 8 7 15 16 12 lsatlspsn ⊢ ( 𝜑 → ( 𝐿 ‘ { 𝑠 } ) ∈ ( LSAtoms ‘ 𝐶 ) )
18 1 9 2 14 5 15 11 17 mapdcnvatN ⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
19 3 4 14 islsati ⊢ ( ( 𝑈 ∈ LMod ∧ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) → ∃ 𝑣 ∈ 𝑉 ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) )
20 13 18 19 syl2anc ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑉 ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) )
21 simpr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) )
22 21 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) )
23 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
24 12 eldifad ⊢ ( 𝜑 → 𝑠 ∈ 𝐷 )
25 eqid ⊢ ( LSubSp ‘ 𝐶 ) = ( LSubSp ‘ 𝐶 )
26 6 25 8 lspsncl ⊢ ( ( 𝐶 ∈ LMod ∧ 𝑠 ∈ 𝐷 ) → ( 𝐿 ‘ { 𝑠 } ) ∈ ( LSubSp ‘ 𝐶 ) )
27 16 24 26 syl2anc ⊢ ( 𝜑 → ( 𝐿 ‘ { 𝑠 } ) ∈ ( LSubSp ‘ 𝐶 ) )
28 1 9 5 25 11 mapdrn2 ⊢ ( 𝜑 → ran 𝑀 = ( LSubSp ‘ 𝐶 ) )
29 27 28 eleqtrrd ⊢ ( 𝜑 → ( 𝐿 ‘ { 𝑠 } ) ∈ ran 𝑀 )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝐿 ‘ { 𝑠 } ) ∈ ran 𝑀 )
31 1 9 23 30 mapdcnvid2 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ) = ( 𝐿 ‘ { 𝑠 } ) )
32 22 31 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
33 32 ex ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) ) )
34 33 reximdva ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑉 ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( 𝑁 ‘ { 𝑣 } ) → ∃ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) ) )
35 20 34 mpd ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
36 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
37 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) ) → 𝑠 ∈ ( 𝐷 ∖ { 0 } ) )
38 simp2 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) ) → 𝑣 ∈ 𝑉 )
39 simp3 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
40 1 2 3 4 5 6 7 8 9 10 36 37 38 39 hdmaprnlem15N ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) ) → 𝑠 ∈ ran 𝑆 )
41 40 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑉 ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) → 𝑠 ∈ ran 𝑆 ) )
42 35 41 mpd ⊢ ( 𝜑 → 𝑠 ∈ ran 𝑆 )