Theorem lindslinindimp2lem3

Description: Lemma 3 for lindslinindsimp2 . (Contributed by AV, 25-Apr-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	lindslinind.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
	lindslinind.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	lindslinind.0	⊢ 0 = ( 0g ‘ 𝑅 )
	lindslinind.z	⊢ 𝑍 = ( 0g ‘ 𝑀 )
	lindslinind.y	⊢ 𝑌 = ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) )
	lindslinind.g	⊢ 𝐺 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) )
Assertion	lindslinindimp2lem3	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ) → 𝐺 finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		lindslinind.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
2		lindslinind.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		lindslinind.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		lindslinind.z	⊢ 𝑍 = ( 0g ‘ 𝑀 )
5		lindslinind.y	⊢ 𝑌 = ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) )
6		lindslinind.g	⊢ 𝐺 = ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) )
7		simp3r	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ) → 𝑓 finSupp 0 )
8	3	fvexi	⊢ 0 ∈ V
9	8	a1i	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ) → 0 ∈ V )
10	7 9	fsuppres	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ) → ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) finSupp 0 )
11	6 10	eqbrtrid	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∧ 𝑓 finSupp 0 ) ) → 𝐺 finSupp 0 )