Step |
Hyp |
Ref |
Expression |
1 |
|
ielefmnd.g |
Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |- |
2 |
1
|
efmndsgrp |
Could not format G e. Smgrp : No typesetting found for |- G e. Smgrp with typecode |- |
3 |
2
|
a1i |
Could not format ( A e. V -> G e. Smgrp ) : No typesetting found for |- ( A e. V -> G e. Smgrp ) with typecode |- |
4 |
1
|
ielefmnd |
|
5 |
|
oveq1 |
|
6 |
5
|
eqeq1d |
|
7 |
|
oveq2 |
|
8 |
7
|
eqeq1d |
|
9 |
6 8
|
anbi12d |
|
10 |
9
|
ralbidv |
|
11 |
10
|
adantl |
|
12 |
|
eqid |
|
13 |
1 12
|
efmndbasf |
|
14 |
13
|
adantl |
|
15 |
|
fcoi2 |
|
16 |
|
fcoi1 |
|
17 |
15 16
|
jca |
|
18 |
14 17
|
syl |
|
19 |
|
eqid |
|
20 |
1 12 19
|
efmndov |
|
21 |
4 20
|
sylan |
|
22 |
21
|
eqeq1d |
|
23 |
4
|
anim1ci |
|
24 |
1 12 19
|
efmndov |
|
25 |
23 24
|
syl |
|
26 |
25
|
eqeq1d |
|
27 |
22 26
|
anbi12d |
|
28 |
18 27
|
mpbird |
|
29 |
28
|
ralrimiva |
|
30 |
4 11 29
|
rspcedvd |
|
31 |
12 19
|
ismnddef |
Could not format ( G e. Mnd <-> ( G e. Smgrp /\ E. i e. ( Base ` G ) A. f e. ( Base ` G ) ( ( i ( +g ` G ) f ) = f /\ ( f ( +g ` G ) i ) = f ) ) ) : No typesetting found for |- ( G e. Mnd <-> ( G e. Smgrp /\ E. i e. ( Base ` G ) A. f e. ( Base ` G ) ( ( i ( +g ` G ) f ) = f /\ ( f ( +g ` G ) i ) = f ) ) ) with typecode |- |
32 |
3 30 31
|
sylanbrc |
|