Step |
Hyp |
Ref |
Expression |
1 |
|
odcl.1 |
|- X = ( Base ` G ) |
2 |
|
odcl.2 |
|- O = ( od ` G ) |
3 |
|
odid.3 |
|- .x. = ( .g ` G ) |
4 |
|
odid.4 |
|- .0. = ( 0g ` G ) |
5 |
1 2
|
odcl |
|- ( A e. X -> ( O ` A ) e. NN0 ) |
6 |
5
|
adantl |
|- ( ( G e. Grp /\ A e. X ) -> ( O ` A ) e. NN0 ) |
7 |
1 2 3 4
|
odeq |
|- ( ( G e. Grp /\ A e. X /\ x e. NN0 ) -> ( x = ( O ` A ) <-> A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) ) ) |
8 |
7
|
3expa |
|- ( ( ( G e. Grp /\ A e. X ) /\ x e. NN0 ) -> ( x = ( O ` A ) <-> A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) ) ) |
9 |
8
|
bicomd |
|- ( ( ( G e. Grp /\ A e. X ) /\ x e. NN0 ) -> ( A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) <-> x = ( O ` A ) ) ) |
10 |
6 9
|
riota5 |
|- ( ( G e. Grp /\ A e. X ) -> ( iota_ x e. NN0 A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) ) = ( O ` A ) ) |
11 |
10
|
eqcomd |
|- ( ( G e. Grp /\ A e. X ) -> ( O ` A ) = ( iota_ x e. NN0 A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) ) ) |