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 ) ) )