Metamath Proof Explorer

Theorem lmod1lem3

Description: Lemma 3 for lmod1 . (Contributed by AV, 29-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 lmod1lem3 
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .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 eqidd 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) = ( x e. ( Base ` R ) , y e. { I } |-> y ) )
3 simprr 
 |-  ( ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) /\ ( x = ( q ( +g ` ( Scalar ` M ) ) r ) /\ y = I ) ) -> y = I )
4 simplr 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> R e. Ring )
5 1 lmodsca 
 |-  ( R e. Ring -> R = ( Scalar ` M ) )
6 5 fveq2d 
 |-  ( R e. Ring -> ( +g ` R ) = ( +g ` ( Scalar ` M ) ) )
7 4 6 syl 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( +g ` R ) = ( +g ` ( Scalar ` M ) ) )
8 7 eqcomd 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( +g ` ( Scalar ` M ) ) = ( +g ` R ) )
9 8 oveqd 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( q ( +g ` ( Scalar ` M ) ) r ) = ( q ( +g ` R ) r ) )
10 simprl 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> q e. ( Base ` R ) )
11 simprr 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> r e. ( Base ` R ) )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 eqid 
 |-  ( +g ` R ) = ( +g ` R )
14 12 13 ringacl 
 |-  ( ( R e. Ring /\ q e. ( Base ` R ) /\ r e. ( Base ` R ) ) -> ( q ( +g ` R ) r ) e. ( Base ` R ) )
15 4 10 11 14 syl3anc 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( q ( +g ` R ) r ) e. ( Base ` R ) )
16 9 15 eqeltrd 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( q ( +g ` ( Scalar ` M ) ) r ) e. ( Base ` R ) )
17 snidg 
 |-  ( I e. V -> I e. { I } )
18 17 adantr 
 |-  ( ( I e. V /\ R e. Ring ) -> I e. { I } )
19 18 adantr 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> I e. { I } )
20 simpl 
 |-  ( ( I e. V /\ R e. Ring ) -> I e. V )
21 20 adantr 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> I e. V )
22 2 3 16 19 21 ovmpod 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( +g ` ( Scalar ` M ) ) r ) ( x e. ( Base ` R ) , y e. { I } |-> y ) I ) = I )
23 fvex 
 |-  ( Base ` R ) e. _V
24 snex 
 |-  { I } e. _V
25 23 24 pm3.2i 
 |-  ( ( Base ` R ) e. _V /\ { I } e. _V )
26 mpoexga 
 |-  ( ( ( Base ` R ) e. _V /\ { I } e. _V ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) e. _V )
27 25 26 mp1i 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) e. _V )
28 1 lmodvsca 
 |-  ( ( x e. ( Base ` R ) , y e. { I } |-> y ) e. _V -> ( x e. ( Base ` R ) , y e. { I } |-> y ) = ( .s ` M ) )
29 27 28 syl 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) = ( .s ` M ) )
30 29 eqcomd 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( .s ` M ) = ( x e. ( Base ` R ) , y e. { I } |-> y ) )
31 30 oveqd 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( +g ` ( Scalar ` M ) ) r ) ( x e. ( Base ` R ) , y e. { I } |-> y ) I ) )
32 simprr 
 |-  ( ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) /\ ( x = q /\ y = I ) ) -> y = I )
33 30 32 10 19 19 ovmpod 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( q ( .s ` M ) I ) = I )
34 simprr 
 |-  ( ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) /\ ( x = r /\ y = I ) ) -> y = I )
35 30 34 11 19 19 ovmpod 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( r ( .s ` M ) I ) = I )
36 33 35 oveq12d 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) = ( I ( +g ` M ) I ) )
37 snex 
 |-  { <. <. I , I >. , I >. } e. _V
38 1 lmodplusg 
 |-  ( { <. <. I , I >. , I >. } e. _V -> { <. <. I , I >. , I >. } = ( +g ` M ) )
39 37 38 mp1i 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> { <. <. I , I >. , I >. } = ( +g ` M ) )
40 39 eqcomd 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( +g ` M ) = { <. <. I , I >. , I >. } )
41 40 oveqd 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( I ( +g ` M ) I ) = ( I { <. <. I , I >. , I >. } I ) )
42 df-ov 
 |-  ( I { <. <. I , I >. , I >. } I ) = ( { <. <. I , I >. , I >. } ` <. I , I >. )
43 opex 
 |-  <. I , I >. e. _V
44 20 43 jctil 
 |-  ( ( I e. V /\ R e. Ring ) -> ( <. I , I >. e. _V /\ I e. V ) )
45 44 adantr 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( <. I , I >. e. _V /\ I e. V ) )
46 fvsng 
 |-  ( ( <. I , I >. e. _V /\ I e. V ) -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
47 45 46 syl 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
48 42 47 syl5eq 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( I { <. <. I , I >. , I >. } I ) = I )
49 36 41 48 3eqtrd 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) = I )
50 22 31 49 3eqtr4d 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) )