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 = 1 st ⁡ R
drngi.2 ⊢ H = 2 nd ⁡ R
drngi.3 ⊢ X = ran ⁡ G
drngi.4 ⊢ Z = GId ⁡ G
Assertion drngoi ⊢ R ∈ DivRingOps → R ∈ RingOps ∧ H ↾ X ∖ Z × X ∖ Z ∈ GrpOp

Proof

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