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 \in DivRingOps \to (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in 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) \to ⟨g, h⟩ = ⟨1^{st} (R), h⟩$
6	5	eleq1d	$⊢ g = 1^{st} (R) \to (⟨g, h⟩ \in RingOps \leftrightarrow ⟨1^{st} (R), h⟩ \in RingOps)$
7		id	$⊢ g = 1^{st} (R) \to g = 1^{st} (R)$
8	7 1	eqtr4di	$⊢ g = 1^{st} (R) \to g = G$
9	8	rneqd	$⊢ g = 1^{st} (R) \to ran g = ran G$
10	9 3	eqtr4di	$⊢ g = 1^{st} (R) \to ran g = X$
11	8	fveq2d	$⊢ g = 1^{st} (R) \to GId (g) = GId (G)$
12	11 4	eqtr4di	$⊢ g = 1^{st} (R) \to GId (g) = Z$
13	12	sneqd	$⊢ g = 1^{st} (R) \to \{GId (g)\} = \{Z\}$
14	10 13	difeq12d	$⊢ g = 1^{st} (R) \to ran g ∖ \{GId (g)\} = X ∖ \{Z\}$
15	14	sqxpeqd	$⊢ g = 1^{st} (R) \to (ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}) = (X ∖ \{Z\}) \times (X ∖ \{Z\})$
16	15	reseq2d	$⊢ g = 1^{st} (R) \to {h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} = {h ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}$
17	16	eleq1d	$⊢ g = 1^{st} (R) \to ({h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} \in GrpOp \leftrightarrow {h ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$
18	6 17	anbi12d	$⊢ g = 1^{st} (R) \to ((⟨g, h⟩ \in RingOps \land {h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} \in GrpOp) \leftrightarrow (⟨1^{st} (R), h⟩ \in RingOps \land {h ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp))$
19		opeq2	$⊢ h = 2^{nd} (R) \to ⟨1^{st} (R), h⟩ = ⟨1^{st} (R), 2^{nd} (R)⟩$
20	19	eleq1d	$⊢ h = 2^{nd} (R) \to (⟨1^{st} (R), h⟩ \in RingOps \leftrightarrow ⟨1^{st} (R), 2^{nd} (R)⟩ \in RingOps)$
21	20	anbi1d	$⊢ h = 2^{nd} (R) \to ((⟨1^{st} (R), h⟩ \in RingOps \land {h ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \leftrightarrow (⟨1^{st} (R), 2^{nd} (R)⟩ \in RingOps \land {h ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp))$
22		id	$⊢ h = 2^{nd} (R) \to h = 2^{nd} (R)$
23	2 22	eqtr4id	$⊢ h = 2^{nd} (R) \to H = h$
24	23	reseq1d	$⊢ h = 2^{nd} (R) \to {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} = {h ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}$
25	24	eleq1d	$⊢ h = 2^{nd} (R) \to ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \leftrightarrow {h ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$
26	25	anbi2d	$⊢ h = 2^{nd} (R) \to ((⟨1^{st} (R), 2^{nd} (R)⟩ \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \leftrightarrow (⟨1^{st} (R), 2^{nd} (R)⟩ \in RingOps \land {h ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp))$
27	21 26	bitr4d	$⊢ h = 2^{nd} (R) \to ((⟨1^{st} (R), h⟩ \in RingOps \land {h ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \leftrightarrow (⟨1^{st} (R), 2^{nd} (R)⟩ \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp))$
28	18 27	elopabi	$⊢ R \in \{⟨g, h⟩ \| (⟨g, h⟩ \in RingOps \land {h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} \in GrpOp)\} \to (⟨1^{st} (R), 2^{nd} (R)⟩ \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$
29		df-drngo	$⊢ DivRingOps = \{⟨g, h⟩ \| (⟨g, h⟩ \in RingOps \land {h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} \in GrpOp)\}$
30	28 29	eleq2s	$⊢ R \in DivRingOps \to (⟨1^{st} (R), 2^{nd} (R)⟩ \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$
31	29	relopabiv	$⊢ Rel DivRingOps$
32		1st2nd	$⊢ (Rel DivRingOps \land R \in DivRingOps) \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
33	31 32	mpan	$⊢ R \in DivRingOps \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
34	33	eleq1d	$⊢ R \in DivRingOps \to (R \in RingOps \leftrightarrow ⟨1^{st} (R), 2^{nd} (R)⟩ \in RingOps)$
35	34	anbi1d	$⊢ R \in DivRingOps \to ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \leftrightarrow (⟨1^{st} (R), 2^{nd} (R)⟩ \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp))$
36	30 35	mpbird	$⊢ R \in DivRingOps \to (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$

Metamath Proof Explorer

Theorem drngoi

Proof