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 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 )