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∈A→GH∈DivRingOps↔GH∈RingOps∧H↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp

Proof

Step Hyp Ref Expression
1 df-br ⊢GDivRingOpsH↔GH∈DivRingOps
2 df-drngo ⊢DivRingOps=xy|xy∈RingOps∧y↾ran⁡x∖GId⁡x×ran⁡x∖GId⁡x∈GrpOp
3 2 relopabiv ⊢Rel⁡DivRingOps
4 3 brrelex1i ⊢GDivRingOpsH→G∈V
5 1 4 sylbir ⊢GH∈DivRingOps→G∈V
6 5 anim1i ⊢GH∈DivRingOps∧H∈A→G∈V∧H∈A
7 6 ancoms ⊢H∈A∧GH∈DivRingOps→G∈V∧H∈A
8 rngoablo2 ⊢GH∈RingOps→G∈AbelOp
9 elex ⊢G∈AbelOp→G∈V
10 8 9 syl ⊢GH∈RingOps→G∈V
11 10 ad2antrl ⊢H∈A∧GH∈RingOps∧H↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp→G∈V
12 simpl ⊢H∈A∧GH∈RingOps∧H↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp→H∈A
13 11 12 jca ⊢H∈A∧GH∈RingOps∧H↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp→G∈V∧H∈A
14 df-drngo ⊢DivRingOps=gh|gh∈RingOps∧h↾ran⁡g∖GId⁡g×ran⁡g∖GId⁡g∈GrpOp
15 14 eleq2i ⊢GH∈DivRingOps↔GH∈gh|gh∈RingOps∧h↾ran⁡g∖GId⁡g×ran⁡g∖GId⁡g∈GrpOp
16 opeq1 ⊢g=G→gh=Gh
17 16 eleq1d ⊢g=G→gh∈RingOps↔Gh∈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×ran⁡g∖GId⁡g=ran⁡G∖GId⁡G×ran⁡G∖GId⁡G
23 22 reseq2d ⊢g=G→h↾ran⁡g∖GId⁡g×ran⁡g∖GId⁡g=h↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G
24 23 eleq1d ⊢g=G→h↾ran⁡g∖GId⁡g×ran⁡g∖GId⁡g∈GrpOp↔h↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp
25 17 24 anbi12d ⊢g=G→gh∈RingOps∧h↾ran⁡g∖GId⁡g×ran⁡g∖GId⁡g∈GrpOp↔Gh∈RingOps∧h↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp
26 opeq2 ⊢h=H→Gh=GH
27 26 eleq1d ⊢h=H→Gh∈RingOps↔GH∈RingOps
28 reseq1 ⊢h=H→h↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G=H↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G
29 28 eleq1d ⊢h=H→h↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp↔H↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp
30 27 29 anbi12d ⊢h=H→Gh∈RingOps∧h↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp↔GH∈RingOps∧H↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp
31 25 30 opelopabg ⊢G∈V∧H∈A→GH∈gh|gh∈RingOps∧h↾ran⁡g∖GId⁡g×ran⁡g∖GId⁡g∈GrpOp↔GH∈RingOps∧H↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp
32 15 31 bitrid ⊢G∈V∧H∈A→GH∈DivRingOps↔GH∈RingOps∧H↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp
33 7 13 32 pm5.21nd ⊢H∈A→GH∈DivRingOps↔GH∈RingOps∧H↾ran⁡G∖GId⁡G×ran⁡G∖GId⁡G∈GrpOp