Metamath Proof Explorer

Theorem lmod1lem4

Description: Lemma 4 for lmod1 . (Contributed by AV, 29-Apr-2019)

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

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 2 3 pm3.2i ⊢BaseR∈V∧I∈V
5 4 a1i ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→BaseR∈V∧I∈V
6 mpoexga ⊢BaseR∈V∧I∈V→x∈BaseR,y∈I⟼y∈V
7 1 lmodvsca ⊢x∈BaseR,y∈I⟼y∈V→x∈BaseR,y∈I⟼y=⋅M
8 5 6 7 3syl ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→x∈BaseR,y∈I⟼y=⋅M
9 8 eqcomd ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→⋅M=x∈BaseR,y∈I⟼y
10 simprr ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR∧x=q∧y=I→y=I
11 simprl ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→q∈BaseR
12 snidg ⊢I∈V→I∈I
13 12 ad2antrr ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→I∈I
14 9 10 11 13 13 ovmpod ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→q⋅MI=I
15 simprr ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR∧x=r∧y=I→y=I
16 simprr ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→r∈BaseR
17 9 15 16 13 13 ovmpod ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→r⋅MI=I
18 17 oveq2d ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→q⋅Mr⋅MI=q⋅MI
19 simprr ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR∧x=q⋅Scalar⁡Mr∧y=I→y=I
20 simplr ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→R∈Ring
21 1 lmodsca ⊢R∈Ring→R=Scalar⁡M
22 21 fveq2d ⊢R∈Ring→⋅R=⋅Scalar⁡M
23 20 22 syl ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→⋅R=⋅Scalar⁡M
24 23 eqcomd ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→⋅Scalar⁡M=⋅R
25 24 oveqd ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→q⋅Scalar⁡Mr=q⋅Rr
26 eqid ⊢BaseR=BaseR
27 eqid ⊢⋅R=⋅R
28 26 27 ringcl ⊢R∈Ring∧q∈BaseR∧r∈BaseR→q⋅Rr∈BaseR
29 20 11 16 28 syl3anc ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→q⋅Rr∈BaseR
30 25 29 eqeltrd ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→q⋅Scalar⁡Mr∈BaseR
31 9 19 30 13 13 ovmpod ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→q⋅Scalar⁡Mr⋅MI=I
32 14 18 31 3eqtr4rd ⊢I∈V∧R∈Ring∧q∈BaseR∧r∈BaseR→q⋅Scalar⁡Mr⋅MI=q⋅Mr⋅MI