Metamath Proof Explorer

Theorem lindslinindimp2lem2

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

Ref Expression
Hypotheses lindslinind.r ⊢ R = Scalar ⁡ M
lindslinind.b ⊢ B = Base R
lindslinind.0 ⊢ 0 ˙ = 0 R
lindslinind.z ⊢ Z = 0 M
lindslinind.y ⊢ Y = inv g ⁡ R ⁡ f ⁡ x
lindslinind.g ⊢ G = f ↾ S ∖ x
Assertion lindslinindimp2lem2 ⊢ S ∈ V ∧ M ∈ LMod ∧ S ⊆ Base M ∧ x ∈ S ∧ f ∈ B S → G ∈ B S ∖ x

Proof

Step Hyp Ref Expression
1 lindslinind.r ⊢ R = Scalar ⁡ M
2 lindslinind.b ⊢ B = Base R
3 lindslinind.0 ⊢ 0 ˙ = 0 R
4 lindslinind.z ⊢ Z = 0 M
5 lindslinind.y ⊢ Y = inv g ⁡ R ⁡ f ⁡ x
6 lindslinind.g ⊢ G = f ↾ S ∖ x
7 elmapi ⊢ f ∈ B S → f : S ⟶ B
8 7 3ad2ant3 ⊢ S ⊆ Base M ∧ x ∈ S ∧ f ∈ B S → f : S ⟶ B
9 8 adantl ⊢ S ∈ V ∧ M ∈ LMod ∧ S ⊆ Base M ∧ x ∈ S ∧ f ∈ B S → f : S ⟶ B
10 difss ⊢ S ∖ x ⊆ S
11 fssres ⊢ f : S ⟶ B ∧ S ∖ x ⊆ S → f ↾ S ∖ x : S ∖ x ⟶ B
12 9 10 11 sylancl ⊢ S ∈ V ∧ M ∈ LMod ∧ S ⊆ Base M ∧ x ∈ S ∧ f ∈ B S → f ↾ S ∖ x : S ∖ x ⟶ B
13 6 feq1i ⊢ G : S ∖ x ⟶ B ↔ f ↾ S ∖ x : S ∖ x ⟶ B
14 12 13 sylibr ⊢ S ∈ V ∧ M ∈ LMod ∧ S ⊆ Base M ∧ x ∈ S ∧ f ∈ B S → G : S ∖ x ⟶ B
15 2 fvexi ⊢ B ∈ V
16 difexg ⊢ S ∈ V → S ∖ x ∈ V
17 16 ad2antrr ⊢ S ∈ V ∧ M ∈ LMod ∧ S ⊆ Base M ∧ x ∈ S ∧ f ∈ B S → S ∖ x ∈ V
18 elmapg ⊢ B ∈ V ∧ S ∖ x ∈ V → G ∈ B S ∖ x ↔ G : S ∖ x ⟶ B
19 15 17 18 sylancr ⊢ S ∈ V ∧ M ∈ LMod ∧ S ⊆ Base M ∧ x ∈ S ∧ f ∈ B S → G ∈ B S ∖ x ↔ G : S ∖ x ⟶ B
20 14 19 mpbird ⊢ S ∈ V ∧ M ∈ LMod ∧ S ⊆ Base M ∧ x ∈ S ∧ f ∈ B S → G ∈ B S ∖ x