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
|
syl5eq |
|- ( ( 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
|
syl5eq |
|- ( ( 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
|
syl5eqr |
|- ( ph -> ( +g ` M ) = ( +g ` Z ) ) |
52 |
27 51
|
jca |
|- ( ph -> ( ( Base ` M ) = ( Base ` Z ) /\ ( +g ` M ) = ( +g ` Z ) ) ) |