isdrngo3

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 10-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$
	isdivrng2.5	$⊢ U = GId (H)$
Assertion	isdrngo3	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in X y H x = U))$

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		isdivrng2.5	$⊢ U = GId (H)$
6	1 2 3 4 5	isdrngo2	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U))$
7		eldifi	$⊢ x \in (X ∖ \{Z\}) \to x \in X$
8		difss	$⊢ X ∖ \{Z\} \subseteq X$
9		ssrexv	$⊢ X ∖ \{Z\} \subseteq X \to (\exists y \in (X ∖ \{Z\}) y H x = U \to \exists y \in X y H x = U)$
10	8 9	ax-mp	$⊢ \exists y \in (X ∖ \{Z\}) y H x = U \to \exists y \in X y H x = U$
11		neeq1	$⊢ y H x = U \to (y H x \neq Z \leftrightarrow U \neq Z)$
12	11	biimparc	$⊢ (U \neq Z \land y H x = U) \to y H x \neq Z$
13	3 4 1 2	rngolz	$⊢ (R \in RingOps \land x \in X) \to Z H x = Z$
14		oveq1	$⊢ y = Z \to y H x = Z H x$
15	14	eqeq1d	$⊢ y = Z \to (y H x = Z \leftrightarrow Z H x = Z)$
16	13 15	syl5ibrcom	$⊢ (R \in RingOps \land x \in X) \to (y = Z \to y H x = Z)$
17	16	necon3d	$⊢ (R \in RingOps \land x \in X) \to (y H x \neq Z \to y \neq Z)$
18	17	imp	$⊢ ((R \in RingOps \land x \in X) \land y H x \neq Z) \to y \neq Z$
19	12 18	sylan2	$⊢ ((R \in RingOps \land x \in X) \land (U \neq Z \land y H x = U)) \to y \neq Z$
20	19	an4s	$⊢ ((R \in RingOps \land U \neq Z) \land (x \in X \land y H x = U)) \to y \neq Z$
21	20	anassrs	$⊢ (((R \in RingOps \land U \neq Z) \land x \in X) \land y H x = U) \to y \neq Z$
22		pm3.2	$⊢ y \in X \to (y \neq Z \to (y \in X \land y \neq Z))$
23	21 22	syl5com	$⊢ (((R \in RingOps \land U \neq Z) \land x \in X) \land y H x = U) \to (y \in X \to (y \in X \land y \neq Z))$
24		eldifsn	$⊢ y \in (X ∖ \{Z\}) \leftrightarrow (y \in X \land y \neq Z)$
25	23 24	syl6ibr	$⊢ (((R \in RingOps \land U \neq Z) \land x \in X) \land y H x = U) \to (y \in X \to y \in (X ∖ \{Z\}))$
26	25	imdistanda	$⊢ ((R \in RingOps \land U \neq Z) \land x \in X) \to ((y H x = U \land y \in X) \to (y H x = U \land y \in (X ∖ \{Z\})))$
27		ancom	$⊢ (y \in X \land y H x = U) \leftrightarrow (y H x = U \land y \in X)$
28		ancom	$⊢ (y \in (X ∖ \{Z\}) \land y H x = U) \leftrightarrow (y H x = U \land y \in (X ∖ \{Z\}))$
29	26 27 28	3imtr4g	$⊢ ((R \in RingOps \land U \neq Z) \land x \in X) \to ((y \in X \land y H x = U) \to (y \in (X ∖ \{Z\}) \land y H x = U))$
30	29	reximdv2	$⊢ ((R \in RingOps \land U \neq Z) \land x \in X) \to (\exists y \in X y H x = U \to \exists y \in (X ∖ \{Z\}) y H x = U)$
31	10 30	impbid2	$⊢ ((R \in RingOps \land U \neq Z) \land x \in X) \to (\exists y \in (X ∖ \{Z\}) y H x = U \leftrightarrow \exists y \in X y H x = U)$
32	7 31	sylan2	$⊢ ((R \in RingOps \land U \neq Z) \land x \in (X ∖ \{Z\})) \to (\exists y \in (X ∖ \{Z\}) y H x = U \leftrightarrow \exists y \in X y H x = U)$
33	32	ralbidva	$⊢ (R \in RingOps \land U \neq Z) \to (\forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U \leftrightarrow \forall x \in (X ∖ \{Z\}) \exists y \in X y H x = U)$
34	33	pm5.32da	$⊢ R \in RingOps \to ((U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U) \leftrightarrow (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in X y H x = U))$
35	34	pm5.32i	$⊢ (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \leftrightarrow (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in X y H x = U))$
36	6 35	bitri	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in X y H x = U))$

Metamath Proof Explorer

Theorem isdrngo3

Proof