Metamath Proof Explorer

Theorem lmod1lem1

Description: Lemma 1 for lmod1 . (Contributed by AV, 28-Apr-2019)

Ref Expression
Hypothesis lmod1.m ⊢M=BasendxI+ndxIIIScalar⁡ndxR∪⋅ndxx∈BaseR,y∈I⟼y
Assertion lmod1lem1 ⊢I∈V∧R∈Ring∧r∈BaseR→r⋅MI∈I

Proof

Step Hyp Ref Expression
1 lmod1.m ⊢M=BasendxI+ndxIIIScalar⁡ndxR∪⋅ndxx∈BaseR,y∈I⟼y
2 fvex ⊢BaseR∈V
3 snex ⊢I∈V
4 3 a1i ⊢I∈V∧R∈Ring∧r∈BaseR→I∈V
5 mpoexga ⊢BaseR∈V∧I∈V→x∈BaseR,y∈I⟼y∈V
6 2 4 5 sylancr ⊢I∈V∧R∈Ring∧r∈BaseR→x∈BaseR,y∈I⟼y∈V
7 1 lmodvsca ⊢x∈BaseR,y∈I⟼y∈V→x∈BaseR,y∈I⟼y=⋅M
8 6 7 syl ⊢I∈V∧R∈Ring∧r∈BaseR→x∈BaseR,y∈I⟼y=⋅M
9 8 eqcomd ⊢I∈V∧R∈Ring∧r∈BaseR→⋅M=x∈BaseR,y∈I⟼y
10 simprr ⊢I∈V∧R∈Ring∧r∈BaseR∧x=r∧y=I→y=I
11 simp3 ⊢I∈V∧R∈Ring∧r∈BaseR→r∈BaseR
12 snidg ⊢I∈V→I∈I
13 12 3ad2ant1 ⊢I∈V∧R∈Ring∧r∈BaseR→I∈I
14 9 10 11 13 13 ovmpod ⊢I∈V∧R∈Ring∧r∈BaseR→r⋅MI=I
15 14 13 eqeltrd ⊢I∈V∧R∈Ring∧r∈BaseR→r⋅MI∈I