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