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