isdrngo1

Description: The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010)

	Ref	Expression
Hypotheses	isdivrng1.1	$⊢ G = 1^{st} (R)$
	isdivrng1.2	$⊢ H = 2^{nd} (R)$
	isdivrng1.3	$⊢ Z = GId (G)$
	isdivrng1.4	$⊢ X = ran G$
Assertion	isdrngo1	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$

Proof

Step	Hyp	Ref	Expression
1		isdivrng1.1	$⊢ G = 1^{st} (R)$
2		isdivrng1.2	$⊢ H = 2^{nd} (R)$
3		isdivrng1.3	$⊢ Z = GId (G)$
4		isdivrng1.4	$⊢ X = ran G$
5		df-drngo	$⊢ DivRingOps = \{⟨g, h⟩ \| (⟨g, h⟩ \in RingOps \land {h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} \in GrpOp)\}$
6	5	relopabiv	$⊢ Rel DivRingOps$
7		1st2nd	$⊢ (Rel DivRingOps \land R \in DivRingOps) \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
8	6 7	mpan	$⊢ R \in DivRingOps \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
9		relrngo	$⊢ Rel RingOps$
10		1st2nd	$⊢ (Rel RingOps \land R \in RingOps) \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
11	9 10	mpan	$⊢ R \in RingOps \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
12	11	adantr	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
13	1 2	opeq12i	$⊢ ⟨G, H⟩ = ⟨1^{st} (R), 2^{nd} (R)⟩$
14	13	eqeq2i	$⊢ R = ⟨G, H⟩ \leftrightarrow R = ⟨1^{st} (R), 2^{nd} (R)⟩$
15	2	fvexi	$⊢ H \in V$
16		isdivrngo	$⊢ H \in V \to (⟨G, H⟩ \in DivRingOps \leftrightarrow (⟨G, H⟩ \in RingOps \land {H ↾}_{((ran G ∖ \{GId (G)\}) \times (ran G ∖ \{GId (G)\}))} \in GrpOp))$
17	15 16	ax-mp	$⊢ ⟨G, H⟩ \in DivRingOps \leftrightarrow (⟨G, H⟩ \in RingOps \land {H ↾}_{((ran G ∖ \{GId (G)\}) \times (ran G ∖ \{GId (G)\}))} \in GrpOp)$
18	3	sneqi	$⊢ \{Z\} = \{GId (G)\}$
19	4 18	difeq12i	$⊢ X ∖ \{Z\} = ran G ∖ \{GId (G)\}$
20	19 19	xpeq12i	$⊢ (X ∖ \{Z\}) \times (X ∖ \{Z\}) = (ran G ∖ \{GId (G)\}) \times (ran G ∖ \{GId (G)\})$
21	20	reseq2i	$⊢ {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} = {H ↾}_{((ran G ∖ \{GId (G)\}) \times (ran G ∖ \{GId (G)\}))}$
22	21	eleq1i	$⊢ {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \leftrightarrow {H ↾}_{((ran G ∖ \{GId (G)\}) \times (ran G ∖ \{GId (G)\}))} \in GrpOp$
23	22	anbi2i	$⊢ (⟨G, H⟩ \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \leftrightarrow (⟨G, H⟩ \in RingOps \land {H ↾}_{((ran G ∖ \{GId (G)\}) \times (ran G ∖ \{GId (G)\}))} \in GrpOp)$
24	17 23	bitr4i	$⊢ ⟨G, H⟩ \in DivRingOps \leftrightarrow (⟨G, H⟩ \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$
25		eleq1	$⊢ R = ⟨G, H⟩ \to (R \in DivRingOps \leftrightarrow ⟨G, H⟩ \in DivRingOps)$
26		eleq1	$⊢ R = ⟨G, H⟩ \to (R \in RingOps \leftrightarrow ⟨G, H⟩ \in RingOps)$
27	26	anbi1d	$⊢ R = ⟨G, H⟩ \to ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \leftrightarrow (⟨G, H⟩ \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp))$
28	25 27	bibi12d	$⊢ R = ⟨G, H⟩ \to ((R \in DivRingOps \leftrightarrow (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)) \leftrightarrow (⟨G, H⟩ \in DivRingOps \leftrightarrow (⟨G, H⟩ \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)))$
29	24 28	mpbiri	$⊢ R = ⟨G, H⟩ \to (R \in DivRingOps \leftrightarrow (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp))$
30	14 29	sylbir	$⊢ R = ⟨1^{st} (R), 2^{nd} (R)⟩ \to (R \in DivRingOps \leftrightarrow (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp))$
31	8 12 30	pm5.21nii	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$

Metamath Proof Explorer

Theorem isdrngo1

Proof