Metamath Proof Explorer


Theorem snlindsntorlem

Description: Lemma for snlindsntor . (Contributed by AV, 15-Apr-2019)

Ref Expression
Hypotheses snlindsntor.b 𝐵 = ( Base ‘ 𝑀 )
snlindsntor.r 𝑅 = ( Scalar ‘ 𝑀 )
snlindsntor.s 𝑆 = ( Base ‘ 𝑅 )
snlindsntor.0 0 = ( 0g𝑅 )
snlindsntor.z 𝑍 = ( 0g𝑀 )
snlindsntor.t · = ( ·𝑠𝑀 )
Assertion snlindsntorlem ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) → ( ∀ 𝑓 ∈ ( 𝑆m { 𝑋 } ) ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓𝑋 ) = 0 ) → ∀ 𝑠𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍𝑠 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 snlindsntor.b 𝐵 = ( Base ‘ 𝑀 )
2 snlindsntor.r 𝑅 = ( Scalar ‘ 𝑀 )
3 snlindsntor.s 𝑆 = ( Base ‘ 𝑅 )
4 snlindsntor.0 0 = ( 0g𝑅 )
5 snlindsntor.z 𝑍 = ( 0g𝑀 )
6 snlindsntor.t · = ( ·𝑠𝑀 )
7 eqidd ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → { ⟨ 𝑋 , 𝑠 ⟩ } = { ⟨ 𝑋 , 𝑠 ⟩ } )
8 fsng ( ( 𝑋𝐵𝑠𝑆 ) → ( { ⟨ 𝑋 , 𝑠 ⟩ } : { 𝑋 } ⟶ { 𝑠 } ↔ { ⟨ 𝑋 , 𝑠 ⟩ } = { ⟨ 𝑋 , 𝑠 ⟩ } ) )
9 8 adantll ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → ( { ⟨ 𝑋 , 𝑠 ⟩ } : { 𝑋 } ⟶ { 𝑠 } ↔ { ⟨ 𝑋 , 𝑠 ⟩ } = { ⟨ 𝑋 , 𝑠 ⟩ } ) )
10 7 9 mpbird ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → { ⟨ 𝑋 , 𝑠 ⟩ } : { 𝑋 } ⟶ { 𝑠 } )
11 snssi ( 𝑠𝑆 → { 𝑠 } ⊆ 𝑆 )
12 11 adantl ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → { 𝑠 } ⊆ 𝑆 )
13 10 12 fssd ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → { ⟨ 𝑋 , 𝑠 ⟩ } : { 𝑋 } ⟶ 𝑆 )
14 3 fvexi 𝑆 ∈ V
15 snex { 𝑋 } ∈ V
16 14 15 pm3.2i ( 𝑆 ∈ V ∧ { 𝑋 } ∈ V )
17 elmapg ( ( 𝑆 ∈ V ∧ { 𝑋 } ∈ V ) → ( { ⟨ 𝑋 , 𝑠 ⟩ } ∈ ( 𝑆m { 𝑋 } ) ↔ { ⟨ 𝑋 , 𝑠 ⟩ } : { 𝑋 } ⟶ 𝑆 ) )
18 16 17 mp1i ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → ( { ⟨ 𝑋 , 𝑠 ⟩ } ∈ ( 𝑆m { 𝑋 } ) ↔ { ⟨ 𝑋 , 𝑠 ⟩ } : { 𝑋 } ⟶ 𝑆 ) )
19 13 18 mpbird ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → { ⟨ 𝑋 , 𝑠 ⟩ } ∈ ( 𝑆m { 𝑋 } ) )
20 oveq1 ( 𝑓 = { ⟨ 𝑋 , 𝑠 ⟩ } → ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = ( { ⟨ 𝑋 , 𝑠 ⟩ } ( linC ‘ 𝑀 ) { 𝑋 } ) )
21 20 eqeq1d ( 𝑓 = { ⟨ 𝑋 , 𝑠 ⟩ } → ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ↔ ( { ⟨ 𝑋 , 𝑠 ⟩ } ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) )
22 fveq1 ( 𝑓 = { ⟨ 𝑋 , 𝑠 ⟩ } → ( 𝑓𝑋 ) = ( { ⟨ 𝑋 , 𝑠 ⟩ } ‘ 𝑋 ) )
23 22 eqeq1d ( 𝑓 = { ⟨ 𝑋 , 𝑠 ⟩ } → ( ( 𝑓𝑋 ) = 0 ↔ ( { ⟨ 𝑋 , 𝑠 ⟩ } ‘ 𝑋 ) = 0 ) )
24 21 23 imbi12d ( 𝑓 = { ⟨ 𝑋 , 𝑠 ⟩ } → ( ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓𝑋 ) = 0 ) ↔ ( ( { ⟨ 𝑋 , 𝑠 ⟩ } ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( { ⟨ 𝑋 , 𝑠 ⟩ } ‘ 𝑋 ) = 0 ) ) )
25 1 2 3 6 lincvalsng ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵𝑠𝑆 ) → ( { ⟨ 𝑋 , 𝑠 ⟩ } ( linC ‘ 𝑀 ) { 𝑋 } ) = ( 𝑠 · 𝑋 ) )
26 25 3expa ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → ( { ⟨ 𝑋 , 𝑠 ⟩ } ( linC ‘ 𝑀 ) { 𝑋 } ) = ( 𝑠 · 𝑋 ) )
27 26 eqeq1d ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → ( ( { ⟨ 𝑋 , 𝑠 ⟩ } ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ↔ ( 𝑠 · 𝑋 ) = 𝑍 ) )
28 fvsng ( ( 𝑋𝐵𝑠𝑆 ) → ( { ⟨ 𝑋 , 𝑠 ⟩ } ‘ 𝑋 ) = 𝑠 )
29 28 adantll ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → ( { ⟨ 𝑋 , 𝑠 ⟩ } ‘ 𝑋 ) = 𝑠 )
30 29 eqeq1d ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → ( ( { ⟨ 𝑋 , 𝑠 ⟩ } ‘ 𝑋 ) = 0𝑠 = 0 ) )
31 27 30 imbi12d ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → ( ( ( { ⟨ 𝑋 , 𝑠 ⟩ } ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( { ⟨ 𝑋 , 𝑠 ⟩ } ‘ 𝑋 ) = 0 ) ↔ ( ( 𝑠 · 𝑋 ) = 𝑍𝑠 = 0 ) ) )
32 24 31 sylan9bbr ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) ∧ 𝑓 = { ⟨ 𝑋 , 𝑠 ⟩ } ) → ( ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓𝑋 ) = 0 ) ↔ ( ( 𝑠 · 𝑋 ) = 𝑍𝑠 = 0 ) ) )
33 19 32 rspcdv ( ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) ∧ 𝑠𝑆 ) → ( ∀ 𝑓 ∈ ( 𝑆m { 𝑋 } ) ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓𝑋 ) = 0 ) → ( ( 𝑠 · 𝑋 ) = 𝑍𝑠 = 0 ) ) )
34 33 ralrimdva ( ( 𝑀 ∈ LMod ∧ 𝑋𝐵 ) → ( ∀ 𝑓 ∈ ( 𝑆m { 𝑋 } ) ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓𝑋 ) = 0 ) → ∀ 𝑠𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍𝑠 = 0 ) ) )