Theorem lmod1lem2

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

	Ref	Expression
Hypothesis	lmod1.m	|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )
Assertion	lmod1lem2	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmod1.m	|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )
2		fvex	|- ( Base ` R ) e. _V
3		snex	|- { I } e. _V
4	2 3	pm3.2i	|- ( ( Base ` R ) e. _V /\ { I } e. _V )
5		mpoexga	|- ( ( ( Base ` R ) e. _V /\ { I } e. _V ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) e. _V )
6	4 5	mp1i	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) e. _V )
7	1	lmodvsca	|- ( ( x e. ( Base ` R ) , y e. { I } |-> y ) e. _V -> ( x e. ( Base ` R ) , y e. { I } |-> y ) = ( .s ` M ) )
8	6 7	syl	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) = ( .s ` M ) )
9	8	eqcomd	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( .s ` M ) = ( x e. ( Base ` R ) , y e. { I } |-> y ) )
10		simprr	|- ( ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) /\ ( x = r /\ y = I ) ) -> y = I )
11		simp3	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> r e. ( Base ` R ) )
12		snidg	|- ( I e. V -> I e. { I } )
13	12	3ad2ant1	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> I e. { I } )
14	9 10 11 13 13	ovmpod	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( r ( .s ` M ) I ) = I )
15		snex	|- { <. <. I , I >. , I >. } e. _V
16	1	lmodplusg	|- ( { <. <. I , I >. , I >. } e. _V -> { <. <. I , I >. , I >. } = ( +g ` M ) )
17	15 16	mp1i	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> { <. <. I , I >. , I >. } = ( +g ` M ) )
18	17	eqcomd	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( +g ` M ) = { <. <. I , I >. , I >. } )
19	18	oveqd	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( I ( +g ` M ) I ) = ( I { <. <. I , I >. , I >. } I ) )
20		df-ov	|- ( I { <. <. I , I >. , I >. } I ) = ( { <. <. I , I >. , I >. } ` <. I , I >. )
21		opex	|- <. I , I >. e. _V
22		simp1	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> I e. V )
23		fvsng	|- ( ( <. I , I >. e. _V /\ I e. V ) -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
24	21 22 23	sylancr	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
25	20 24	syl5eq	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( I { <. <. I , I >. , I >. } I ) = I )
26	19 25	eqtrd	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( I ( +g ` M ) I ) = I )
27	26	oveq2d	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( r ( .s ` M ) I ) )
28	3	a1i	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> { I } e. _V )
29	2 28 5	sylancr	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) e. _V )
30	29 7	syl	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) = ( .s ` M ) )
31	30	eqcomd	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( .s ` M ) = ( x e. ( Base ` R ) , y e. { I } |-> y ) )
32	31 10 11 13 13	ovmpod	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( r ( .s ` M ) I ) = I )
33	32 32	oveq12d	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) = ( I ( +g ` M ) I ) )
34	33 26	eqtrd	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) = I )
35	14 27 34	3eqtr4d	|- ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) )