Step |
Hyp |
Ref |
Expression |
1 |
|
gexval.1 |
|- X = ( Base ` G ) |
2 |
|
gexval.2 |
|- .x. = ( .g ` G ) |
3 |
|
gexval.3 |
|- .0. = ( 0g ` G ) |
4 |
|
gexval.4 |
|- E = ( gEx ` G ) |
5 |
|
gexval.i |
|- I = { y e. NN | A. x e. X ( y .x. x ) = .0. } |
6 |
|
df-gex |
|- gEx = ( g e. _V |-> [_ { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) |
7 |
|
nnex |
|- NN e. _V |
8 |
7
|
rabex |
|- { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } e. _V |
9 |
8
|
a1i |
|- ( ( G e. V /\ g = G ) -> { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } e. _V ) |
10 |
|
simpr |
|- ( ( G e. V /\ g = G ) -> g = G ) |
11 |
10
|
fveq2d |
|- ( ( G e. V /\ g = G ) -> ( Base ` g ) = ( Base ` G ) ) |
12 |
11 1
|
eqtr4di |
|- ( ( G e. V /\ g = G ) -> ( Base ` g ) = X ) |
13 |
10
|
fveq2d |
|- ( ( G e. V /\ g = G ) -> ( .g ` g ) = ( .g ` G ) ) |
14 |
13 2
|
eqtr4di |
|- ( ( G e. V /\ g = G ) -> ( .g ` g ) = .x. ) |
15 |
14
|
oveqd |
|- ( ( G e. V /\ g = G ) -> ( y ( .g ` g ) x ) = ( y .x. x ) ) |
16 |
10
|
fveq2d |
|- ( ( G e. V /\ g = G ) -> ( 0g ` g ) = ( 0g ` G ) ) |
17 |
16 3
|
eqtr4di |
|- ( ( G e. V /\ g = G ) -> ( 0g ` g ) = .0. ) |
18 |
15 17
|
eqeq12d |
|- ( ( G e. V /\ g = G ) -> ( ( y ( .g ` g ) x ) = ( 0g ` g ) <-> ( y .x. x ) = .0. ) ) |
19 |
12 18
|
raleqbidv |
|- ( ( G e. V /\ g = G ) -> ( A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) <-> A. x e. X ( y .x. x ) = .0. ) ) |
20 |
19
|
rabbidv |
|- ( ( G e. V /\ g = G ) -> { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } = { y e. NN | A. x e. X ( y .x. x ) = .0. } ) |
21 |
20 5
|
eqtr4di |
|- ( ( G e. V /\ g = G ) -> { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } = I ) |
22 |
21
|
eqeq2d |
|- ( ( G e. V /\ g = G ) -> ( i = { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } <-> i = I ) ) |
23 |
22
|
biimpa |
|- ( ( ( G e. V /\ g = G ) /\ i = { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } ) -> i = I ) |
24 |
23
|
eqeq1d |
|- ( ( ( G e. V /\ g = G ) /\ i = { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } ) -> ( i = (/) <-> I = (/) ) ) |
25 |
23
|
infeq1d |
|- ( ( ( G e. V /\ g = G ) /\ i = { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } ) -> inf ( i , RR , < ) = inf ( I , RR , < ) ) |
26 |
24 25
|
ifbieq2d |
|- ( ( ( G e. V /\ g = G ) /\ i = { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } ) -> if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) ) |
27 |
9 26
|
csbied |
|- ( ( G e. V /\ g = G ) -> [_ { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) ) |
28 |
|
elex |
|- ( G e. V -> G e. _V ) |
29 |
|
c0ex |
|- 0 e. _V |
30 |
|
ltso |
|- < Or RR |
31 |
30
|
infex |
|- inf ( I , RR , < ) e. _V |
32 |
29 31
|
ifex |
|- if ( I = (/) , 0 , inf ( I , RR , < ) ) e. _V |
33 |
32
|
a1i |
|- ( G e. V -> if ( I = (/) , 0 , inf ( I , RR , < ) ) e. _V ) |
34 |
6 27 28 33
|
fvmptd2 |
|- ( G e. V -> ( gEx ` G ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) ) |
35 |
4 34
|
eqtrid |
|- ( G e. V -> E = if ( I = (/) , 0 , inf ( I , RR , < ) ) ) |