Metamath Proof Explorer

Theorem isdivrngo

Description: The predicate "is a division ring". (Contributed by FL, 6-Sep-2009) (New usage is discouraged.)

Ref Expression
Assertion isdivrngo 
|- ( H e. A -> ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( G DivRingOps H <-> <. G , H >. e. DivRingOps )
2 df-drngo 
 |-  DivRingOps = { <. x , y >. | ( <. x , y >. e. RingOps /\ ( y |` ( ( ran x \ { ( GId ` x ) } ) X. ( ran x \ { ( GId ` x ) } ) ) ) e. GrpOp ) }
3 2 relopabiv 
 |-  Rel DivRingOps
4 3 brrelex1i 
 |-  ( G DivRingOps H -> G e. _V )
5 1 4 sylbir 
 |-  ( <. G , H >. e. DivRingOps -> G e. _V )
6 5 anim1i 
 |-  ( ( <. G , H >. e. DivRingOps /\ H e. A ) -> ( G e. _V /\ H e. A ) )
7 6 ancoms 
 |-  ( ( H e. A /\ <. G , H >. e. DivRingOps ) -> ( G e. _V /\ H e. A ) )
8 rngoablo2 
 |-  ( <. G , H >. e. RingOps -> G e. AbelOp )
9 elex 
 |-  ( G e. AbelOp -> G e. _V )
10 8 9 syl 
 |-  ( <. G , H >. e. RingOps -> G e. _V )
11 10 ad2antrl 
 |-  ( ( H e. A /\ ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) -> G e. _V )
12 simpl 
 |-  ( ( H e. A /\ ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) -> H e. A )
13 11 12 jca 
 |-  ( ( H e. A /\ ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) -> ( G e. _V /\ H e. A ) )
14 df-drngo 
 |-  DivRingOps = { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) }
15 14 eleq2i 
 |-  ( <. G , H >. e. DivRingOps <-> <. G , H >. e. { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) } )
16 opeq1 
 |-  ( g = G -> <. g , h >. = <. G , h >. )
17 16 eleq1d 
 |-  ( g = G -> ( <. g , h >. e. RingOps <-> <. G , h >. e. RingOps ) )
18 rneq 
 |-  ( g = G -> ran g = ran G )
19 fveq2 
 |-  ( g = G -> ( GId ` g ) = ( GId ` G ) )
20 19 sneqd 
 |-  ( g = G -> { ( GId ` g ) } = { ( GId ` G ) } )
21 18 20 difeq12d 
 |-  ( g = G -> ( ran g \ { ( GId ` g ) } ) = ( ran G \ { ( GId ` G ) } ) )
22 21 sqxpeqd 
 |-  ( g = G -> ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) = ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) )
23 22 reseq2d 
 |-  ( g = G -> ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) = ( h |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) )
24 23 eleq1d 
 |-  ( g = G -> ( ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp <-> ( h |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) )
25 17 24 anbi12d 
 |-  ( g = G -> ( ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) <-> ( <. G , h >. e. RingOps /\ ( h |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) )
26 opeq2 
 |-  ( h = H -> <. G , h >. = <. G , H >. )
27 26 eleq1d 
 |-  ( h = H -> ( <. G , h >. e. RingOps <-> <. G , H >. e. RingOps ) )
28 reseq1 
 |-  ( h = H -> ( h |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) = ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) )
29 28 eleq1d 
 |-  ( h = H -> ( ( h |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp <-> ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) )
30 27 29 anbi12d 
 |-  ( h = H -> ( ( <. G , h >. e. RingOps /\ ( h |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) )
31 25 30 opelopabg 
 |-  ( ( G e. _V /\ H e. A ) -> ( <. G , H >. e. { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) } <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) )
32 15 31 syl5bb 
 |-  ( ( G e. _V /\ H e. A ) -> ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) )
33 7 13 32 pm5.21nd 
 |-  ( H e. A -> ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) )