Metamath Proof Explorer

Theorem isdrngo1

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

Ref Expression
Hypotheses isdivrng1.1 
|- G = ( 1st ` R )
isdivrng1.2 
|- H = ( 2nd ` R )
isdivrng1.3 
|- Z = ( GId ` G )
isdivrng1.4 
|- X = ran G
Assertion isdrngo1 
|- ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )

Proof

Step Hyp Ref Expression
1 isdivrng1.1 
 |-  G = ( 1st ` R )
2 isdivrng1.2 
 |-  H = ( 2nd ` R )
3 isdivrng1.3 
 |-  Z = ( GId ` G )
4 isdivrng1.4 
 |-  X = ran G
5 df-drngo 
 |-  DivRingOps = { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) }
6 5 relopabi 
 |-  Rel DivRingOps
7 1st2nd 
 |-  ( ( Rel DivRingOps /\ R e. DivRingOps ) -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
8 6 7 mpan 
 |-  ( R e. DivRingOps -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
9 relrngo 
 |-  Rel RingOps
10 1st2nd 
 |-  ( ( Rel RingOps /\ R e. RingOps ) -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
11 9 10 mpan 
 |-  ( R e. RingOps -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
12 11 adantr 
 |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
13 1 2 opeq12i 
 |-  <. G , H >. = <. ( 1st ` R ) , ( 2nd ` R ) >.
14 13 eqeq2i 
 |-  ( R = <. G , H >. <-> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
15 2 fvexi 
 |-  H e. _V
16 isdivrngo 
 |-  ( H e. _V -> ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) )
17 15 16 ax-mp 
 |-  ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) )
18 3 sneqi 
 |-  { Z } = { ( GId ` G ) }
19 4 18 difeq12i 
 |-  ( X \ { Z } ) = ( ran G \ { ( GId ` G ) } )
20 19 19 xpeq12i 
 |-  ( ( X \ { Z } ) X. ( X \ { Z } ) ) = ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) )
21 20 reseq2i 
 |-  ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) )
22 21 eleq1i 
 |-  ( ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp <-> ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp )
23 22 anbi2i 
 |-  ( ( <. G , H >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) )
24 17 23 bitr4i 
 |-  ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )
25 eleq1 
 |-  ( R = <. G , H >. -> ( R e. DivRingOps <-> <. G , H >. e. DivRingOps ) )
26 eleq1 
 |-  ( R = <. G , H >. -> ( R e. RingOps <-> <. G , H >. e. RingOps ) )
27 26 anbi1d 
 |-  ( R = <. G , H >. -> ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) )
28 25 27 bibi12d 
 |-  ( R = <. G , H >. -> ( ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) <-> ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) ) )
29 24 28 mpbiri 
 |-  ( R = <. G , H >. -> ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) )
30 14 29 sylbir 
 |-  ( R = <. ( 1st ` R ) , ( 2nd ` R ) >. -> ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) )
31 8 12 30 pm5.21nii 
 |-  ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )