Step |
Hyp |
Ref |
Expression |
1 |
|
prdsgrpd.y |
|- Y = ( S Xs_ R ) |
2 |
|
prdsgrpd.i |
|- ( ph -> I e. W ) |
3 |
|
prdsgrpd.s |
|- ( ph -> S e. V ) |
4 |
|
prdsgrpd.r |
|- ( ph -> R : I --> Grp ) |
5 |
|
prdsinvgd.b |
|- B = ( Base ` Y ) |
6 |
|
prdsinvgd.n |
|- N = ( invg ` Y ) |
7 |
|
prdsinvgd.x |
|- ( ph -> X e. B ) |
8 |
|
eqid |
|- ( +g ` Y ) = ( +g ` Y ) |
9 |
3
|
elexd |
|- ( ph -> S e. _V ) |
10 |
2
|
elexd |
|- ( ph -> I e. _V ) |
11 |
|
eqid |
|- ( 0g o. R ) = ( 0g o. R ) |
12 |
|
eqid |
|- ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) |
13 |
1 5 8 9 10 4 7 11 12
|
prdsinvlem |
|- ( ph -> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) e. B /\ ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ( +g ` Y ) X ) = ( 0g o. R ) ) ) |
14 |
13
|
simprd |
|- ( ph -> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ( +g ` Y ) X ) = ( 0g o. R ) ) |
15 |
|
grpmnd |
|- ( a e. Grp -> a e. Mnd ) |
16 |
15
|
ssriv |
|- Grp C_ Mnd |
17 |
|
fss |
|- ( ( R : I --> Grp /\ Grp C_ Mnd ) -> R : I --> Mnd ) |
18 |
4 16 17
|
sylancl |
|- ( ph -> R : I --> Mnd ) |
19 |
1 2 3 18
|
prds0g |
|- ( ph -> ( 0g o. R ) = ( 0g ` Y ) ) |
20 |
14 19
|
eqtrd |
|- ( ph -> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ( +g ` Y ) X ) = ( 0g ` Y ) ) |
21 |
1 2 3 4
|
prdsgrpd |
|- ( ph -> Y e. Grp ) |
22 |
13
|
simpld |
|- ( ph -> ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) e. B ) |
23 |
|
eqid |
|- ( 0g ` Y ) = ( 0g ` Y ) |
24 |
5 8 23 6
|
grpinvid2 |
|- ( ( Y e. Grp /\ X e. B /\ ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) e. B ) -> ( ( N ` X ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) <-> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ( +g ` Y ) X ) = ( 0g ` Y ) ) ) |
25 |
21 7 22 24
|
syl3anc |
|- ( ph -> ( ( N ` X ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) <-> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ( +g ` Y ) X ) = ( 0g ` Y ) ) ) |
26 |
20 25
|
mpbird |
|- ( ph -> ( N ` X ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ) |