Metamath Proof Explorer

Theorem isrngo

Description: The predicate "is a (unital) ring." Definition of "ring with unit" in Schechter p. 187. (Contributed by Jeff Hankins, 21-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis isring.1 
|- X = ran G
Assertion isrngo 
|- ( H e. A -> ( <. G , H >. e. RingOps <-> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( 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 ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isring.1 
 |-  X = ran G
2 df-br 
 |-  ( G RingOps H <-> <. G , H >. e. RingOps )
3 relrngo 
 |-  Rel RingOps
4 3 brrelex1i 
 |-  ( G RingOps H -> G e. _V )
5 2 4 sylbir 
 |-  ( <. G , H >. e. RingOps -> G e. _V )
6 5 a1i 
 |-  ( H e. A -> ( <. G , H >. e. RingOps -> G e. _V ) )
7 elex 
 |-  ( G e. AbelOp -> G e. _V )
8 7 ad2antrr 
 |-  ( ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( 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 ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) -> G e. _V )
9 8 a1i 
 |-  ( H e. A -> ( ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( 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 ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) -> G e. _V ) )
10 df-rngo 
 |-  RingOps = { <. g , h >. | ( ( 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 ) ) ) }
11 10 eleq2i 
 |-  ( <. G , H >. e. RingOps <-> <. G , H >. e. { <. g , h >. | ( ( 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 ) ) ) } )
12 simpl 
 |-  ( ( g = G /\ h = H ) -> g = G )
13 12 eleq1d 
 |-  ( ( g = G /\ h = H ) -> ( g e. AbelOp <-> G e. AbelOp ) )
14 simpr 
 |-  ( ( g = G /\ h = H ) -> h = H )
15 12 rneqd 
 |-  ( ( g = G /\ h = H ) -> ran g = ran G )
16 15 1 eqtr4di 
 |-  ( ( g = G /\ h = H ) -> ran g = X )
17 16 sqxpeqd 
 |-  ( ( g = G /\ h = H ) -> ( ran g X. ran g ) = ( X X. X ) )
18 14 17 16 feq123d 
 |-  ( ( g = G /\ h = H ) -> ( h : ( ran g X. ran g ) --> ran g <-> H : ( X X. X ) --> X ) )
19 13 18 anbi12d 
 |-  ( ( g = G /\ h = H ) -> ( ( g e. AbelOp /\ h : ( ran g X. ran g ) --> ran g ) <-> ( G e. AbelOp /\ H : ( X X. X ) --> X ) ) )
20 14 oveqd 
 |-  ( ( g = G /\ h = H ) -> ( x h y ) = ( x H y ) )
21 eqidd 
 |-  ( ( g = G /\ h = H ) -> z = z )
22 14 20 21 oveq123d 
 |-  ( ( g = G /\ h = H ) -> ( ( x h y ) h z ) = ( ( x H y ) H z ) )
23 eqidd 
 |-  ( ( g = G /\ h = H ) -> x = x )
24 14 oveqd 
 |-  ( ( g = G /\ h = H ) -> ( y h z ) = ( y H z ) )
25 14 23 24 oveq123d 
 |-  ( ( g = G /\ h = H ) -> ( x h ( y h z ) ) = ( x H ( y H z ) ) )
26 22 25 eqeq12d 
 |-  ( ( g = G /\ h = H ) -> ( ( ( x h y ) h z ) = ( x h ( y h z ) ) <-> ( ( x H y ) H z ) = ( x H ( y H z ) ) ) )
27 12 oveqd 
 |-  ( ( g = G /\ h = H ) -> ( y g z ) = ( y G z ) )
28 14 23 27 oveq123d 
 |-  ( ( g = G /\ h = H ) -> ( x h ( y g z ) ) = ( x H ( y G z ) ) )
29 14 oveqd 
 |-  ( ( g = G /\ h = H ) -> ( x h z ) = ( x H z ) )
30 12 20 29 oveq123d 
 |-  ( ( g = G /\ h = H ) -> ( ( x h y ) g ( x h z ) ) = ( ( x H y ) G ( x H z ) ) )
31 28 30 eqeq12d 
 |-  ( ( g = G /\ h = H ) -> ( ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) <-> ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) ) )
32 12 oveqd 
 |-  ( ( g = G /\ h = H ) -> ( x g y ) = ( x G y ) )
33 14 32 21 oveq123d 
 |-  ( ( g = G /\ h = H ) -> ( ( x g y ) h z ) = ( ( x G y ) H z ) )
34 12 29 24 oveq123d 
 |-  ( ( g = G /\ h = H ) -> ( ( x h z ) g ( y h z ) ) = ( ( x H z ) G ( y H z ) ) )
35 33 34 eqeq12d 
 |-  ( ( g = G /\ h = H ) -> ( ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) <-> ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) )
36 26 31 35 3anbi123d 
 |-  ( ( g = G /\ h = H ) -> ( ( ( ( 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 ) ) ) <-> ( ( ( 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 ) ) ) ) )
37 16 36 raleqbidv 
 |-  ( ( g = G /\ h = H ) -> ( 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 ) ) ) <-> 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 ) ) ) ) )
38 16 37 raleqbidv 
 |-  ( ( g = G /\ h = H ) -> ( 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 ) ) ) <-> 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 ) ) ) ) )
39 16 38 raleqbidv 
 |-  ( ( g = G /\ h = H ) -> ( 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 ) ) ) <-> 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 ) ) ) ) )
40 20 eqeq1d 
 |-  ( ( g = G /\ h = H ) -> ( ( x h y ) = y <-> ( x H y ) = y ) )
41 14 oveqd 
 |-  ( ( g = G /\ h = H ) -> ( y h x ) = ( y H x ) )
42 41 eqeq1d 
 |-  ( ( g = G /\ h = H ) -> ( ( y h x ) = y <-> ( y H x ) = y ) )
43 40 42 anbi12d 
 |-  ( ( g = G /\ h = H ) -> ( ( ( x h y ) = y /\ ( y h x ) = y ) <-> ( ( x H y ) = y /\ ( y H x ) = y ) ) )
44 16 43 raleqbidv 
 |-  ( ( g = G /\ h = H ) -> ( A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y ) <-> A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) )
45 16 44 rexeqbidv 
 |-  ( ( g = G /\ h = H ) -> ( E. x e. ran g A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y ) <-> E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) )
46 39 45 anbi12d 
 |-  ( ( g = G /\ h = H ) -> ( ( 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 ) ) <-> ( 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 ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) )
47 19 46 anbi12d 
 |-  ( ( g = G /\ h = H ) -> ( ( ( 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 ) ) ) <-> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( 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 ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) )
48 47 opelopabga 
 |-  ( ( G e. _V /\ H e. A ) -> ( <. G , H >. e. { <. g , h >. | ( ( 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 ) ) ) } <-> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( 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 ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) )
49 11 48 bitrid 
 |-  ( ( G e. _V /\ H e. A ) -> ( <. G , H >. e. RingOps <-> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( 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 ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) )
50 49 expcom 
 |-  ( H e. A -> ( G e. _V -> ( <. G , H >. e. RingOps <-> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( 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 ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) ) )
51 6 9 50 pm5.21ndd 
 |-  ( H e. A -> ( <. G , H >. e. RingOps <-> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( 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 ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) )