Step |
Hyp |
Ref |
Expression |
1 |
|
frgpup.b |
|- B = ( Base ` H ) |
2 |
|
frgpup.n |
|- N = ( invg ` H ) |
3 |
|
frgpup.t |
|- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) ) |
4 |
|
frgpup.h |
|- ( ph -> H e. Grp ) |
5 |
|
frgpup.i |
|- ( ph -> I e. V ) |
6 |
|
frgpup.a |
|- ( ph -> F : I --> B ) |
7 |
6
|
ffvelrnda |
|- ( ( ph /\ y e. I ) -> ( F ` y ) e. B ) |
8 |
7
|
adantrr |
|- ( ( ph /\ ( y e. I /\ z e. 2o ) ) -> ( F ` y ) e. B ) |
9 |
1 2
|
grpinvcl |
|- ( ( H e. Grp /\ ( F ` y ) e. B ) -> ( N ` ( F ` y ) ) e. B ) |
10 |
4 8 9
|
syl2an2r |
|- ( ( ph /\ ( y e. I /\ z e. 2o ) ) -> ( N ` ( F ` y ) ) e. B ) |
11 |
8 10
|
ifcld |
|- ( ( ph /\ ( y e. I /\ z e. 2o ) ) -> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) e. B ) |
12 |
11
|
ralrimivva |
|- ( ph -> A. y e. I A. z e. 2o if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) e. B ) |
13 |
3
|
fmpo |
|- ( A. y e. I A. z e. 2o if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) e. B <-> T : ( I X. 2o ) --> B ) |
14 |
12 13
|
sylib |
|- ( ph -> T : ( I X. 2o ) --> B ) |