Metamath Proof Explorer

Theorem isrngod

Description: Conditions that determine a ring. (Changed label from isringd to isrngod -NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses isringod.1 
|- ( ph -> G e. AbelOp )
isringod.2 
|- ( ph -> X = ran G )
isringod.3 
|- ( ph -> H : ( X X. X ) --> X )
isringod.4 
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x H y ) H z ) = ( x H ( y H z ) ) )
isringod.5 
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) )
isringod.6 
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) )
isringod.7 
|- ( ph -> U e. X )
isringod.8 
|- ( ( ph /\ y e. X ) -> ( U H y ) = y )
isringod.9 
|- ( ( ph /\ y e. X ) -> ( y H U ) = y )
Assertion isrngod 
|- ( ph -> <. G , H >. e. RingOps )

Proof

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 fex 
 |-  ( ( H : ( ran G X. ran G ) --> ran G /\ ( ran G X. ran G ) e. _V ) -> H e. _V )
35 12 33 34 syl2anc 
 |-  ( ph -> H e. _V )
36 eqid 
 |-  ran G = ran G
37 36 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 ) ) ) ) )
38 35 37 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 ) ) ) ) )
39 30 38 mpbird 
 |-  ( ph -> <. G , H >. e. RingOps )