Theorem lindslinindimp2lem2

Description: Lemma 2 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	lindslinindimp2lem2	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → 𝐺 ∈ ( 𝐵 ↑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		elmapi	⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) → 𝑓 : 𝑆 ⟶ 𝐵 )
8	7	3ad2ant3	⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) → 𝑓 : 𝑆 ⟶ 𝐵 )
9	8	adantl	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → 𝑓 : 𝑆 ⟶ 𝐵 )
10		difss	⊢ ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑆
11		fssres	⊢ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑆 ) → ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) : ( 𝑆 ∖ { 𝑥 } ) ⟶ 𝐵 )
12	9 10 11	sylancl	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) : ( 𝑆 ∖ { 𝑥 } ) ⟶ 𝐵 )
13	6	feq1i	⊢ ( 𝐺 : ( 𝑆 ∖ { 𝑥 } ) ⟶ 𝐵 ↔ ( 𝑓 ↾ ( 𝑆 ∖ { 𝑥 } ) ) : ( 𝑆 ∖ { 𝑥 } ) ⟶ 𝐵 )
14	12 13	sylibr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → 𝐺 : ( 𝑆 ∖ { 𝑥 } ) ⟶ 𝐵 )
15	2	fvexi	⊢ 𝐵 ∈ V
16		difexg	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∖ { 𝑥 } ) ∈ V )
17	16	ad2antrr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → ( 𝑆 ∖ { 𝑥 } ) ∈ V )
18		elmapg	⊢ ( ( 𝐵 ∈ V ∧ ( 𝑆 ∖ { 𝑥 } ) ∈ V ) → ( 𝐺 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ↔ 𝐺 : ( 𝑆 ∖ { 𝑥 } ) ⟶ 𝐵 ) )
19	15 17 18	sylancr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → ( 𝐺 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) ↔ 𝐺 : ( 𝑆 ∖ { 𝑥 } ) ⟶ 𝐵 ) )
20	14 19	mpbird	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ) ) → 𝐺 ∈ ( 𝐵 ↑m ( 𝑆 ∖ { 𝑥 } ) ) )