Step |
Hyp |
Ref |
Expression |
1 |
|
isringod.1 |
|- ( ph -> G e. AbelOp ) |
2 |
|
isringod.2 |
|- ( ph -> X = ran G ) |
3 |
|
isringod.3 |
|- ( ph -> H : ( X X. X ) --> X ) |
4 |
|
isringod.4 |
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x H y ) H z ) = ( x H ( y H z ) ) ) |
5 |
|
isringod.5 |
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) ) |
6 |
|
isringod.6 |
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) |
7 |
|
isringod.7 |
|- ( ph -> U e. X ) |
8 |
|
isringod.8 |
|- ( ( ph /\ y e. X ) -> ( U H y ) = y ) |
9 |
|
isringod.9 |
|- ( ( ph /\ y e. X ) -> ( y H U ) = y ) |
10 |
2
|
sqxpeqd |
|- ( ph -> ( X X. X ) = ( ran G X. ran G ) ) |
11 |
10 2
|
feq23d |
|- ( ph -> ( H : ( X X. X ) --> X <-> H : ( ran G X. ran G ) --> ran G ) ) |
12 |
3 11
|
mpbid |
|- ( ph -> H : ( ran G X. ran G ) --> ran G ) |
13 |
4 5 6
|
3jca |
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) ) |
14 |
13
|
ralrimivvva |
|- ( ph -> A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) ) |
15 |
2
|
raleqdv |
|- ( ph -> ( A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) <-> A. z e. ran G ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) ) ) |
16 |
2 15
|
raleqbidv |
|- ( ph -> ( A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) <-> A. y e. ran G A. z e. ran G ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) ) ) |
17 |
2 16
|
raleqbidv |
|- ( ph -> ( A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) <-> A. x e. ran G A. y e. ran G A. z e. ran G ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) ) ) |
18 |
14 17
|
mpbid |
|- ( ph -> A. x e. ran G A. y e. ran G A. z e. ran G ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) ) |
19 |
8 9
|
jca |
|- ( ( ph /\ y e. X ) -> ( ( U H y ) = y /\ ( y H U ) = y ) ) |
20 |
19
|
ralrimiva |
|- ( ph -> A. y e. X ( ( U H y ) = y /\ ( y H U ) = y ) ) |
21 |
|
oveq1 |
|- ( x = U -> ( x H y ) = ( U H y ) ) |
22 |
21
|
eqeq1d |
|- ( x = U -> ( ( x H y ) = y <-> ( U H y ) = y ) ) |
23 |
22
|
ovanraleqv |
|- ( x = U -> ( A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) <-> A. y e. X ( ( U H y ) = y /\ ( y H U ) = y ) ) ) |
24 |
23
|
rspcev |
|- ( ( U e. X /\ A. y e. X ( ( U H y ) = y /\ ( y H U ) = y ) ) -> E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) |
25 |
7 20 24
|
syl2anc |
|- ( ph -> E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) |
26 |
2
|
raleqdv |
|- ( ph -> ( A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) <-> A. y e. ran G ( ( x H y ) = y /\ ( y H x ) = y ) ) ) |
27 |
2 26
|
rexeqbidv |
|- ( ph -> ( E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) <-> E. x e. ran G A. y e. ran G ( ( x H y ) = y /\ ( y H x ) = y ) ) ) |
28 |
25 27
|
mpbid |
|- ( ph -> E. x e. ran G A. y e. ran G ( ( x H y ) = y /\ ( y H x ) = y ) ) |
29 |
18 28
|
jca |
|- ( ph -> ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. ran G A. y e. ran G ( ( x H y ) = y /\ ( y H x ) = y ) ) ) |
30 |
1 12 29
|
jca31 |
|- ( ph -> ( ( G e. AbelOp /\ H : ( ran G X. ran G ) --> ran G ) /\ ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. ran G A. y e. ran G ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) |
31 |
|
rnexg |
|- ( G e. AbelOp -> ran G e. _V ) |
32 |
1 31
|
syl |
|- ( ph -> ran G e. _V ) |
33 |
32 32
|
xpexd |
|- ( ph -> ( ran G X. ran G ) e. _V ) |
34 |
12 33
|
fexd |
|- ( ph -> H e. _V ) |
35 |
|
eqid |
|- ran G = ran G |
36 |
35
|
isrngo |
|- ( H e. _V -> ( <. G , H >. e. RingOps <-> ( ( G e. AbelOp /\ H : ( ran G X. ran G ) --> ran G ) /\ ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. ran G A. y e. ran G ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) ) |
37 |
34 36
|
syl |
|- ( ph -> ( <. G , H >. e. RingOps <-> ( ( G e. AbelOp /\ H : ( ran G X. ran G ) --> ran G ) /\ ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. ran G A. y e. ran G ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) ) |
38 |
30 37
|
mpbird |
|- ( ph -> <. G , H >. e. RingOps ) |