Metamath Proof Explorer

Theorem iscrngo2

Description: The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010)

Ref Expression
Hypotheses iscring2.1 
|- G = ( 1st ` R )
iscring2.2 
|- H = ( 2nd ` R )
iscring2.3 
|- X = ran G
Assertion iscrngo2 
|- ( R e. CRingOps <-> ( R e. RingOps /\ A. x e. X A. y e. X ( x H y ) = ( y H x ) ) )

Proof

Step Hyp Ref Expression
1 iscring2.1 
 |-  G = ( 1st ` R )
2 iscring2.2 
 |-  H = ( 2nd ` R )
3 iscring2.3 
 |-  X = ran G
4 iscrngo 
 |-  ( R e. CRingOps <-> ( R e. RingOps /\ R e. Com2 ) )
5 relrngo 
 |-  Rel RingOps
6 1st2nd 
 |-  ( ( Rel RingOps /\ R e. RingOps ) -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
7 5 6 mpan 
 |-  ( R e. RingOps -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
8 eleq1 
 |-  ( R = <. ( 1st ` R ) , ( 2nd ` R ) >. -> ( R e. Com2 <-> <. ( 1st ` R ) , ( 2nd ` R ) >. e. Com2 ) )
9 1 rneqi 
 |-  ran G = ran ( 1st ` R )
10 3 9 eqtri 
 |-  X = ran ( 1st ` R )
11 10 raleqi 
 |-  ( A. x e. X A. y e. ran ( 1st ` R ) ( x ( 2nd ` R ) y ) = ( y ( 2nd ` R ) x ) <-> A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( x ( 2nd ` R ) y ) = ( y ( 2nd ` R ) x ) )
12 2 oveqi 
 |-  ( x H y ) = ( x ( 2nd ` R ) y )
13 2 oveqi 
 |-  ( y H x ) = ( y ( 2nd ` R ) x )
14 12 13 eqeq12i 
 |-  ( ( x H y ) = ( y H x ) <-> ( x ( 2nd ` R ) y ) = ( y ( 2nd ` R ) x ) )
15 10 14 raleqbii 
 |-  ( A. y e. X ( x H y ) = ( y H x ) <-> A. y e. ran ( 1st ` R ) ( x ( 2nd ` R ) y ) = ( y ( 2nd ` R ) x ) )
16 15 ralbii 
 |-  ( A. x e. X A. y e. X ( x H y ) = ( y H x ) <-> A. x e. X A. y e. ran ( 1st ` R ) ( x ( 2nd ` R ) y ) = ( y ( 2nd ` R ) x ) )
17 fvex 
 |-  ( 1st ` R ) e. _V
18 fvex 
 |-  ( 2nd ` R ) e. _V
19 iscom2 
 |-  ( ( ( 1st ` R ) e. _V /\ ( 2nd ` R ) e. _V ) -> ( <. ( 1st ` R ) , ( 2nd ` R ) >. e. Com2 <-> A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( x ( 2nd ` R ) y ) = ( y ( 2nd ` R ) x ) ) )
20 17 18 19 mp2an 
 |-  ( <. ( 1st ` R ) , ( 2nd ` R ) >. e. Com2 <-> A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( x ( 2nd ` R ) y ) = ( y ( 2nd ` R ) x ) )
21 11 16 20 3bitr4ri 
 |-  ( <. ( 1st ` R ) , ( 2nd ` R ) >. e. Com2 <-> A. x e. X A. y e. X ( x H y ) = ( y H x ) )
22 8 21 bitrdi 
 |-  ( R = <. ( 1st ` R ) , ( 2nd ` R ) >. -> ( R e. Com2 <-> A. x e. X A. y e. X ( x H y ) = ( y H x ) ) )
23 7 22 syl 
 |-  ( R e. RingOps -> ( R e. Com2 <-> A. x e. X A. y e. X ( x H y ) = ( y H x ) ) )
24 23 pm5.32i 
 |-  ( ( R e. RingOps /\ R e. Com2 ) <-> ( R e. RingOps /\ A. x e. X A. y e. X ( x H y ) = ( y H x ) ) )
25 4 24 bitri 
 |-  ( R e. CRingOps <-> ( R e. RingOps /\ A. x e. X A. y e. X ( x H y ) = ( y H x ) ) )