Metamath Proof Explorer

Theorem drngoi

Description: The properties of a division ring. (Contributed by NM, 4-Apr-2009) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 drngi.1 
 |-  G = ( 1st ` R )
2 drngi.2 
 |-  H = ( 2nd ` R )
3 drngi.3 
 |-  X = ran G
4 drngi.4 
 |-  Z = ( GId ` G )
5 opeq1 
 |-  ( g = ( 1st ` R ) -> <. g , h >. = <. ( 1st ` R ) , h >. )
6 5 eleq1d 
 |-  ( g = ( 1st ` R ) -> ( <. g , h >. e. RingOps <-> <. ( 1st ` R ) , h >. e. RingOps ) )
7 id 
 |-  ( g = ( 1st ` R ) -> g = ( 1st ` R ) )
8 7 1 eqtr4di 
 |-  ( g = ( 1st ` R ) -> g = G )
9 8 rneqd 
 |-  ( g = ( 1st ` R ) -> ran g = ran G )
10 9 3 eqtr4di 
 |-  ( g = ( 1st ` R ) -> ran g = X )
11 8 fveq2d 
 |-  ( g = ( 1st ` R ) -> ( GId ` g ) = ( GId ` G ) )
12 11 4 eqtr4di 
 |-  ( g = ( 1st ` R ) -> ( GId ` g ) = Z )
13 12 sneqd 
 |-  ( g = ( 1st ` R ) -> { ( GId ` g ) } = { Z } )
14 10 13 difeq12d 
 |-  ( g = ( 1st ` R ) -> ( ran g \ { ( GId ` g ) } ) = ( X \ { Z } ) )
15 14 sqxpeqd 
 |-  ( g = ( 1st ` R ) -> ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) = ( ( X \ { Z } ) X. ( X \ { Z } ) ) )
16 15 reseq2d 
 |-  ( g = ( 1st ` R ) -> ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) = ( h |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) )
17 16 eleq1d 
 |-  ( g = ( 1st ` R ) -> ( ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp <-> ( h |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )
18 6 17 anbi12d 
 |-  ( g = ( 1st ` R ) -> ( ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) <-> ( <. ( 1st ` R ) , h >. e. RingOps /\ ( h |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) )
19 opeq2 
 |-  ( h = ( 2nd ` R ) -> <. ( 1st ` R ) , h >. = <. ( 1st ` R ) , ( 2nd ` R ) >. )
20 19 eleq1d 
 |-  ( h = ( 2nd ` R ) -> ( <. ( 1st ` R ) , h >. e. RingOps <-> <. ( 1st ` R ) , ( 2nd ` R ) >. e. RingOps ) )
21 20 anbi1d 
 |-  ( h = ( 2nd ` R ) -> ( ( <. ( 1st ` R ) , h >. e. RingOps /\ ( h |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) <-> ( <. ( 1st ` R ) , ( 2nd ` R ) >. e. RingOps /\ ( h |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) )
22 id 
 |-  ( h = ( 2nd ` R ) -> h = ( 2nd ` R ) )
23 2 22 eqtr4id 
 |-  ( h = ( 2nd ` R ) -> H = h )
24 23 reseq1d 
 |-  ( h = ( 2nd ` R ) -> ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = ( h |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) )
25 24 eleq1d 
 |-  ( h = ( 2nd ` R ) -> ( ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp <-> ( h |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )
26 25 anbi2d 
 |-  ( h = ( 2nd ` R ) -> ( ( <. ( 1st ` R ) , ( 2nd ` R ) >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) <-> ( <. ( 1st ` R ) , ( 2nd ` R ) >. e. RingOps /\ ( h |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) )
27 21 26 bitr4d 
 |-  ( h = ( 2nd ` R ) -> ( ( <. ( 1st ` R ) , h >. e. RingOps /\ ( h |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) <-> ( <. ( 1st ` R ) , ( 2nd ` R ) >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) )
28 18 27 elopabi 
 |-  ( R e. { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) } -> ( <. ( 1st ` R ) , ( 2nd ` R ) >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )
29 df-drngo 
 |-  DivRingOps = { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) }
30 28 29 eleq2s 
 |-  ( R e. DivRingOps -> ( <. ( 1st ` R ) , ( 2nd ` R ) >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )
31 29 relopabiv 
 |-  Rel DivRingOps
32 1st2nd 
 |-  ( ( Rel DivRingOps /\ R e. DivRingOps ) -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
33 31 32 mpan 
 |-  ( R e. DivRingOps -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
34 33 eleq1d 
 |-  ( R e. DivRingOps -> ( R e. RingOps <-> <. ( 1st ` R ) , ( 2nd ` R ) >. e. RingOps ) )
35 34 anbi1d 
 |-  ( R e. DivRingOps -> ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) <-> ( <. ( 1st ` R ) , ( 2nd ` R ) >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) )
36 30 35 mpbird 
 |-  ( R e. DivRingOps -> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )