Metamath Proof Explorer


Theorem lmod1lem2

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

Ref Expression
Hypothesis lmod1.m M=BasendxI+ndxIIIScalarndxRndxxBaseR,yIy
Assertion lmod1lem2 IVRRingrBaseRrMI+MI=rMI+MrMI

Proof

Step Hyp Ref Expression
1 lmod1.m M=BasendxI+ndxIIIScalarndxRndxxBaseR,yIy
2 fvex BaseRV
3 snex IV
4 2 3 pm3.2i BaseRVIV
5 mpoexga BaseRVIVxBaseR,yIyV
6 4 5 mp1i IVRRingrBaseRxBaseR,yIyV
7 1 lmodvsca xBaseR,yIyVxBaseR,yIy=M
8 6 7 syl IVRRingrBaseRxBaseR,yIy=M
9 8 eqcomd IVRRingrBaseRM=xBaseR,yIy
10 simprr IVRRingrBaseRx=ry=Iy=I
11 simp3 IVRRingrBaseRrBaseR
12 snidg IVII
13 12 3ad2ant1 IVRRingrBaseRII
14 9 10 11 13 13 ovmpod IVRRingrBaseRrMI=I
15 snex IIIV
16 1 lmodplusg IIIVIII=+M
17 15 16 mp1i IVRRingrBaseRIII=+M
18 17 eqcomd IVRRingrBaseR+M=III
19 18 oveqd IVRRingrBaseRI+MI=IIIII
20 df-ov IIIII=IIIII
21 opex IIV
22 simp1 IVRRingrBaseRIV
23 fvsng IIVIVIIIII=I
24 21 22 23 sylancr IVRRingrBaseRIIIII=I
25 20 24 eqtrid IVRRingrBaseRIIIII=I
26 19 25 eqtrd IVRRingrBaseRI+MI=I
27 26 oveq2d IVRRingrBaseRrMI+MI=rMI
28 3 a1i IVRRingrBaseRIV
29 2 28 5 sylancr IVRRingrBaseRxBaseR,yIyV
30 29 7 syl IVRRingrBaseRxBaseR,yIy=M
31 30 eqcomd IVRRingrBaseRM=xBaseR,yIy
32 31 10 11 13 13 ovmpod IVRRingrBaseRrMI=I
33 32 32 oveq12d IVRRingrBaseRrMI+MrMI=I+MI
34 33 26 eqtrd IVRRingrBaseRrMI+MrMI=I
35 14 27 34 3eqtr4d IVRRingrBaseRrMI+MI=rMI+MrMI