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