This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsmgp

Description: The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015)

Ref Expression
Hypotheses prdsmgp.y 
|- Y = ( S Xs_ R )
prdsmgp.m 
|- M = ( mulGrp ` Y )
prdsmgp.z 
|- Z = ( S Xs_ ( mulGrp o. R ) )
prdsmgp.i 
|- ( ph -> I e. V )
prdsmgp.s 
|- ( ph -> S e. W )
prdsmgp.r 
|- ( ph -> R Fn I )
Assertion prdsmgp 
|- ( ph -> ( ( Base ` M ) = ( Base ` Z ) /\ ( +g ` M ) = ( +g ` Z ) ) )

Proof

Step Hyp Ref Expression
1 prdsmgp.y 
 |-  Y = ( S Xs_ R )
2 prdsmgp.m 
 |-  M = ( mulGrp ` Y )
3 prdsmgp.z 
 |-  Z = ( S Xs_ ( mulGrp o. R ) )
4 prdsmgp.i 
 |-  ( ph -> I e. V )
5 prdsmgp.s 
 |-  ( ph -> S e. W )
6 prdsmgp.r 
 |-  ( ph -> R Fn I )
7 eqid 
 |-  ( mulGrp ` ( R ` x ) ) = ( mulGrp ` ( R ` x ) )
8 eqid 
 |-  ( Base ` ( R ` x ) ) = ( Base ` ( R ` x ) )
9 7 8 mgpbas 
 |-  ( Base ` ( R ` x ) ) = ( Base ` ( mulGrp ` ( R ` x ) ) )
10 fvco2 
 |-  ( ( R Fn I /\ x e. I ) -> ( ( mulGrp o. R ) ` x ) = ( mulGrp ` ( R ` x ) ) )
11 6 10 sylan 
 |-  ( ( ph /\ x e. I ) -> ( ( mulGrp o. R ) ` x ) = ( mulGrp ` ( R ` x ) ) )
12 11 eqcomd 
 |-  ( ( ph /\ x e. I ) -> ( mulGrp ` ( R ` x ) ) = ( ( mulGrp o. R ) ` x ) )
13 12 fveq2d 
 |-  ( ( ph /\ x e. I ) -> ( Base ` ( mulGrp ` ( R ` x ) ) ) = ( Base ` ( ( mulGrp o. R ) ` x ) ) )
14 9 13 eqtrid 
 |-  ( ( ph /\ x e. I ) -> ( Base ` ( R ` x ) ) = ( Base ` ( ( mulGrp o. R ) ` x ) ) )
15 14 ixpeq2dva 
 |-  ( ph -> X_ x e. I ( Base ` ( R ` x ) ) = X_ x e. I ( Base ` ( ( mulGrp o. R ) ` x ) ) )
16 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
17 2 16 mgpbas 
 |-  ( Base ` Y ) = ( Base ` M )
18 17 eqcomi 
 |-  ( Base ` M ) = ( Base ` Y )
19 1 18 5 4 6 prdsbas2 
 |-  ( ph -> ( Base ` M ) = X_ x e. I ( Base ` ( R ` x ) ) )
20 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
21 fnmgp 
 |-  mulGrp Fn _V
22 ssv 
 |-  ran R C_ _V
23 22 a1i 
 |-  ( ph -> ran R C_ _V )
24 fnco 
 |-  ( ( mulGrp Fn _V /\ R Fn I /\ ran R C_ _V ) -> ( mulGrp o. R ) Fn I )
25 21 6 23 24 mp3an2i 
 |-  ( ph -> ( mulGrp o. R ) Fn I )
26 3 20 5 4 25 prdsbas2 
 |-  ( ph -> ( Base ` Z ) = X_ x e. I ( Base ` ( ( mulGrp o. R ) ` x ) ) )
27 15 19 26 3eqtr4d 
 |-  ( ph -> ( Base ` M ) = ( Base ` Z ) )
28 eqid 
 |-  ( .r ` Y ) = ( .r ` Y )
29 2 28 mgpplusg 
 |-  ( .r ` Y ) = ( +g ` M )
30 eqid 
 |-  ( mulGrp ` ( R ` z ) ) = ( mulGrp ` ( R ` z ) )
31 eqid 
 |-  ( .r ` ( R ` z ) ) = ( .r ` ( R ` z ) )
32 30 31 mgpplusg 
 |-  ( .r ` ( R ` z ) ) = ( +g ` ( mulGrp ` ( R ` z ) ) )
33 fvco2 
 |-  ( ( R Fn I /\ z e. I ) -> ( ( mulGrp o. R ) ` z ) = ( mulGrp ` ( R ` z ) ) )
34 6 33 sylan 
 |-  ( ( ph /\ z e. I ) -> ( ( mulGrp o. R ) ` z ) = ( mulGrp ` ( R ` z ) ) )
35 34 eqcomd 
 |-  ( ( ph /\ z e. I ) -> ( mulGrp ` ( R ` z ) ) = ( ( mulGrp o. R ) ` z ) )
36 35 fveq2d 
 |-  ( ( ph /\ z e. I ) -> ( +g ` ( mulGrp ` ( R ` z ) ) ) = ( +g ` ( ( mulGrp o. R ) ` z ) ) )
37 32 36 eqtrid 
 |-  ( ( ph /\ z e. I ) -> ( .r ` ( R ` z ) ) = ( +g ` ( ( mulGrp o. R ) ` z ) ) )
38 37 oveqd 
 |-  ( ( ph /\ z e. I ) -> ( ( x ` z ) ( .r ` ( R ` z ) ) ( y ` z ) ) = ( ( x ` z ) ( +g ` ( ( mulGrp o. R ) ` z ) ) ( y ` z ) ) )
39 38 mpteq2dva 
 |-  ( ph -> ( z e. I |-> ( ( x ` z ) ( .r ` ( R ` z ) ) ( y ` z ) ) ) = ( z e. I |-> ( ( x ` z ) ( +g ` ( ( mulGrp o. R ) ` z ) ) ( y ` z ) ) ) )
40 27 27 39 mpoeq123dv 
 |-  ( ph -> ( x e. ( Base ` M ) , y e. ( Base ` M ) |-> ( z e. I |-> ( ( x ` z ) ( .r ` ( R ` z ) ) ( y ` z ) ) ) ) = ( x e. ( Base ` Z ) , y e. ( Base ` Z ) |-> ( z e. I |-> ( ( x ` z ) ( +g ` ( ( mulGrp o. R ) ` z ) ) ( y ` z ) ) ) ) )
41 fnex 
 |-  ( ( R Fn I /\ I e. V ) -> R e. _V )
42 6 4 41 syl2anc 
 |-  ( ph -> R e. _V )
43 6 fndmd 
 |-  ( ph -> dom R = I )
44 1 5 42 18 43 28 prdsmulr 
 |-  ( ph -> ( .r ` Y ) = ( x e. ( Base ` M ) , y e. ( Base ` M ) |-> ( z e. I |-> ( ( x ` z ) ( .r ` ( R ` z ) ) ( y ` z ) ) ) ) )
45 fnex 
 |-  ( ( ( mulGrp o. R ) Fn I /\ I e. V ) -> ( mulGrp o. R ) e. _V )
46 25 4 45 syl2anc 
 |-  ( ph -> ( mulGrp o. R ) e. _V )
47 25 fndmd 
 |-  ( ph -> dom ( mulGrp o. R ) = I )
48 eqid 
 |-  ( +g ` Z ) = ( +g ` Z )
49 3 5 46 20 47 48 prdsplusg 
 |-  ( ph -> ( +g ` Z ) = ( x e. ( Base ` Z ) , y e. ( Base ` Z ) |-> ( z e. I |-> ( ( x ` z ) ( +g ` ( ( mulGrp o. R ) ` z ) ) ( y ` z ) ) ) ) )
50 40 44 49 3eqtr4d 
 |-  ( ph -> ( .r ` Y ) = ( +g ` Z ) )
51 29 50 eqtr3id 
 |-  ( ph -> ( +g ` M ) = ( +g ` Z ) )
52 27 51 jca 
 |-  ( ph -> ( ( Base ` M ) = ( Base ` Z ) /\ ( +g ` M ) = ( +g ` Z ) ) )