Theorem lindslinindimp2lem1

Description: Lemma 1 for lindslinindsimp2 . (Contributed by AV, 25-Apr-2019)

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

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	1	lmodfgrp	⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Grp )
8	7	adantl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → 𝑅 ∈ Grp )
9		elmapi	⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) → 𝑓 : 𝑆 ⟶ 𝐵 )
10		ffvelrn	⊢ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
11	10	a1d	⊢ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
12	11	ex	⊢ ( 𝑓 : 𝑆 ⟶ 𝐵 → ( 𝑥 ∈ 𝑆 → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) )
13	9 12	syl	⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) → ( 𝑥 ∈ 𝑆 → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) )
14	13	com13	⊢ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → ( 𝑥 ∈ 𝑆 → ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) ) )
15	14	3imp	⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
16		eqid	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
17	2 16	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ 𝐵 )
18	8 15 17	syl2an	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ 𝐵 )
19	5 18	eqeltrid	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → 𝑌 ∈ 𝐵 )