divrngidl

Description: The only ideals in a division ring are the zero ideal and the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	divrngidl.1	$⊢ G = 1^{st} (R)$
	divrngidl.2	$⊢ H = 2^{nd} (R)$
	divrngidl.3	$⊢ X = ran G$
	divrngidl.4	$⊢ Z = GId (G)$
Assertion	divrngidl	$⊢ R \in DivRingOps \to Idl (R) = \{\{Z\}, X\}$

Proof

Step	Hyp	Ref	Expression
1		divrngidl.1	$⊢ G = 1^{st} (R)$
2		divrngidl.2	$⊢ H = 2^{nd} (R)$
3		divrngidl.3	$⊢ X = ran G$
4		divrngidl.4	$⊢ Z = GId (G)$
5		eqid	$⊢ GId (H) = GId (H)$
6	1 2 4 3 5	isdrngo2	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land (GId (H) \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)))$
7	1 4	idl0cl	$⊢ (R \in RingOps \land i \in Idl (R)) \to Z \in i$
8	7	adantr	$⊢ ((R \in RingOps \land i \in Idl (R)) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to Z \in i$
9	4	fvexi	$⊢ Z \in V$
10	9	snss	$⊢ Z \in i \leftrightarrow \{Z\} \subseteq i$
11		necom	$⊢ i \neq \{Z\} \leftrightarrow \{Z\} \neq i$
12		pssdifn0	$⊢ (\{Z\} \subseteq i \land \{Z\} \neq i) \to i ∖ \{Z\} \neq \emptyset$
13		n0	$⊢ i ∖ \{Z\} \neq \emptyset \leftrightarrow \exists z z \in (i ∖ \{Z\})$
14	12 13	sylib	$⊢ (\{Z\} \subseteq i \land \{Z\} \neq i) \to \exists z z \in (i ∖ \{Z\})$
15	10 11 14	syl2anb	$⊢ (Z \in i \land i \neq \{Z\}) \to \exists z z \in (i ∖ \{Z\})$
16	1 3	idlss	$⊢ (R \in RingOps \land i \in Idl (R)) \to i \subseteq X$
17		ssdif	$⊢ i \subseteq X \to i ∖ \{Z\} \subseteq X ∖ \{Z\}$
18	17	sselda	$⊢ (i \subseteq X \land z \in (i ∖ \{Z\})) \to z \in (X ∖ \{Z\})$
19	16 18	sylan	$⊢ ((R \in RingOps \land i \in Idl (R)) \land z \in (i ∖ \{Z\})) \to z \in (X ∖ \{Z\})$
20		oveq2	$⊢ x = z \to y H x = y H z$
21	20	eqeq1d	$⊢ x = z \to (y H x = GId (H) \leftrightarrow y H z = GId (H))$
22	21	rexbidv	$⊢ x = z \to (\exists y \in (X ∖ \{Z\}) y H x = GId (H) \leftrightarrow \exists y \in (X ∖ \{Z\}) y H z = GId (H))$
23	22	rspcva	$⊢ (z \in (X ∖ \{Z\}) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to \exists y \in (X ∖ \{Z\}) y H z = GId (H)$
24	19 23	sylan	$⊢ (((R \in RingOps \land i \in Idl (R)) \land z \in (i ∖ \{Z\})) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to \exists y \in (X ∖ \{Z\}) y H z = GId (H)$
25		eldifi	$⊢ z \in (i ∖ \{Z\}) \to z \in i$
26		eldifi	$⊢ y \in (X ∖ \{Z\}) \to y \in X$
27	25 26	anim12i	$⊢ (z \in (i ∖ \{Z\}) \land y \in (X ∖ \{Z\})) \to (z \in i \land y \in X)$
28	1 2 3	idllmulcl	$⊢ ((R \in RingOps \land i \in Idl (R)) \land (z \in i \land y \in X)) \to y H z \in i$
29	1 2 3 5	1idl	$⊢ (R \in RingOps \land i \in Idl (R)) \to (GId (H) \in i \leftrightarrow i = X)$
30	29	biimpd	$⊢ (R \in RingOps \land i \in Idl (R)) \to (GId (H) \in i \to i = X)$
31	30	adantr	$⊢ ((R \in RingOps \land i \in Idl (R)) \land (z \in i \land y \in X)) \to (GId (H) \in i \to i = X)$
32		eleq1	$⊢ y H z = GId (H) \to (y H z \in i \leftrightarrow GId (H) \in i)$
33	32	imbi1d	$⊢ y H z = GId (H) \to ((y H z \in i \to i = X) \leftrightarrow (GId (H) \in i \to i = X))$
34	31 33	syl5ibrcom	$⊢ ((R \in RingOps \land i \in Idl (R)) \land (z \in i \land y \in X)) \to (y H z = GId (H) \to (y H z \in i \to i = X))$
35	28 34	mpid	$⊢ ((R \in RingOps \land i \in Idl (R)) \land (z \in i \land y \in X)) \to (y H z = GId (H) \to i = X)$
36	27 35	sylan2	$⊢ ((R \in RingOps \land i \in Idl (R)) \land (z \in (i ∖ \{Z\}) \land y \in (X ∖ \{Z\}))) \to (y H z = GId (H) \to i = X)$
37	36	anassrs	$⊢ (((R \in RingOps \land i \in Idl (R)) \land z \in (i ∖ \{Z\})) \land y \in (X ∖ \{Z\})) \to (y H z = GId (H) \to i = X)$
38	37	rexlimdva	$⊢ ((R \in RingOps \land i \in Idl (R)) \land z \in (i ∖ \{Z\})) \to (\exists y \in (X ∖ \{Z\}) y H z = GId (H) \to i = X)$
39	38	imp	$⊢ (((R \in RingOps \land i \in Idl (R)) \land z \in (i ∖ \{Z\})) \land \exists y \in (X ∖ \{Z\}) y H z = GId (H)) \to i = X$
40	24 39	syldan	$⊢ (((R \in RingOps \land i \in Idl (R)) \land z \in (i ∖ \{Z\})) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to i = X$
41	40	an32s	$⊢ (((R \in RingOps \land i \in Idl (R)) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \land z \in (i ∖ \{Z\})) \to i = X$
42	41	ex	$⊢ ((R \in RingOps \land i \in Idl (R)) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to (z \in (i ∖ \{Z\}) \to i = X)$
43	42	exlimdv	$⊢ ((R \in RingOps \land i \in Idl (R)) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to (\exists z z \in (i ∖ \{Z\}) \to i = X)$
44	15 43	syl5	$⊢ ((R \in RingOps \land i \in Idl (R)) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to ((Z \in i \land i \neq \{Z\}) \to i = X)$
45	8 44	mpand	$⊢ ((R \in RingOps \land i \in Idl (R)) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to (i \neq \{Z\} \to i = X)$
46	45	an32s	$⊢ ((R \in RingOps \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \land i \in Idl (R)) \to (i \neq \{Z\} \to i = X)$
47		neor	$⊢ (i = \{Z\} \lor i = X) \leftrightarrow (i \neq \{Z\} \to i = X)$
48	46 47	sylibr	$⊢ ((R \in RingOps \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \land i \in Idl (R)) \to (i = \{Z\} \lor i = X)$
49	48	ex	$⊢ (R \in RingOps \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to (i \in Idl (R) \to (i = \{Z\} \lor i = X))$
50	1 4	0idl	$⊢ R \in RingOps \to \{Z\} \in Idl (R)$
51		eleq1	$⊢ i = \{Z\} \to (i \in Idl (R) \leftrightarrow \{Z\} \in Idl (R))$
52	50 51	syl5ibrcom	$⊢ R \in RingOps \to (i = \{Z\} \to i \in Idl (R))$
53	1 3	rngoidl	$⊢ R \in RingOps \to X \in Idl (R)$
54		eleq1	$⊢ i = X \to (i \in Idl (R) \leftrightarrow X \in Idl (R))$
55	53 54	syl5ibrcom	$⊢ R \in RingOps \to (i = X \to i \in Idl (R))$
56	52 55	jaod	$⊢ R \in RingOps \to ((i = \{Z\} \lor i = X) \to i \in Idl (R))$
57	56	adantr	$⊢ (R \in RingOps \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to ((i = \{Z\} \lor i = X) \to i \in Idl (R))$
58	49 57	impbid	$⊢ (R \in RingOps \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to (i \in Idl (R) \leftrightarrow (i = \{Z\} \lor i = X))$
59		vex	$⊢ i \in V$
60	59	elpr	$⊢ i \in \{\{Z\}, X\} \leftrightarrow (i = \{Z\} \lor i = X)$
61	58 60	bitr4di	$⊢ (R \in RingOps \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to (i \in Idl (R) \leftrightarrow i \in \{\{Z\}, X\})$
62	61	eqrdv	$⊢ (R \in RingOps \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H)) \to Idl (R) = \{\{Z\}, X\}$
63	62	adantrl	$⊢ (R \in RingOps \land (GId (H) \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = GId (H))) \to Idl (R) = \{\{Z\}, X\}$
64	6 63	sylbi	$⊢ R \in DivRingOps \to Idl (R) = \{\{Z\}, X\}$

Metamath Proof Explorer

Theorem divrngidl

Proof