uzlidlring

Description: Only the zero (left) ideal or the unit (left) ideal of a domain is a unital ring. (Contributed by AV, 18-Feb-2020)

	Ref	Expression
Hypotheses	lidlabl.l	$⊢ L = LIdeal (R)$
	lidlabl.i	$⊢ I = R ↾_{𝑠} U$
	zlidlring.b	$⊢ B = {Base}_{R}$
	zlidlring.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	uzlidlring	$⊢ (R \in Domn \land U \in L) \to (I \in Ring \leftrightarrow (U = \{\underset{˙}{0}\} \lor U = B))$

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	$⊢ L = LIdeal (R)$
2		lidlabl.i	$⊢ I = R ↾_{𝑠} U$
3		zlidlring.b	$⊢ B = {Base}_{R}$
4		zlidlring.0	$⊢ \underset{˙}{0} = 0_{R}$
5		eqid	$⊢ {Base}_{I} = {Base}_{I}$
6		eqid	$⊢ \cdot_{I} = \cdot_{I}$
7	5 6	isringrng	$⊢ I \in Ring \leftrightarrow (I \in Rng \land \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
8		domnring	$⊢ R \in Domn \to R \in Ring$
9	8	anim1i	$⊢ (R \in Domn \land U \in L) \to (R \in Ring \land U \in L)$
10	1 2	lidlrng	$⊢ (R \in Ring \land U \in L) \to I \in Rng$
11	9 10	syl	$⊢ (R \in Domn \land U \in L) \to I \in Rng$
12		ibar	$⊢ I \in Rng \to (\exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y) \leftrightarrow (I \in Rng \land \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)))$
13	12	bicomd	$⊢ I \in Rng \to ((I \in Rng \land \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \leftrightarrow \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
14	13	adantl	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to ((I \in Rng \land \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \leftrightarrow \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
15		eqid	$⊢ \cdot_{R} = \cdot_{R}$
16	2 15	ressmulr	$⊢ U \in L \to \cdot_{R} = \cdot_{I}$
17	16	eqcomd	$⊢ U \in L \to \cdot_{I} = \cdot_{R}$
18	17	oveqd	$⊢ U \in L \to x \cdot_{I} y = x \cdot_{R} y$
19	18	eqeq1d	$⊢ U \in L \to (x \cdot_{I} y = y \leftrightarrow x \cdot_{R} y = y)$
20	17	oveqd	$⊢ U \in L \to y \cdot_{I} x = y \cdot_{R} x$
21	20	eqeq1d	$⊢ U \in L \to (y \cdot_{I} x = y \leftrightarrow y \cdot_{R} x = y)$
22	19 21	anbi12d	$⊢ U \in L \to ((x \cdot_{I} y = y \land y \cdot_{I} x = y) \leftrightarrow (x \cdot_{R} y = y \land y \cdot_{R} x = y))$
23	22	ad2antlr	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to ((x \cdot_{I} y = y \land y \cdot_{I} x = y) \leftrightarrow (x \cdot_{R} y = y \land y \cdot_{R} x = y))$
24	23	ad2antrr	$⊢ ((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \to ((x \cdot_{I} y = y \land y \cdot_{I} x = y) \leftrightarrow (x \cdot_{R} y = y \land y \cdot_{R} x = y))$
25	24	ralbidv	$⊢ ((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \to (\forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y) \leftrightarrow \forall y \in {Base}_{I} (x \cdot_{R} y = y \land y \cdot_{R} x = y))$
26		simp-4l	$⊢ ((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \to R \in Domn$
27	1 2	lidlbas	$⊢ U \in L \to {Base}_{I} = U$
28	27	eleq1d	$⊢ U \in L \to ({Base}_{I} \in L \leftrightarrow U \in L)$
29	28	ibir	$⊢ U \in L \to {Base}_{I} \in L$
30	29	ad3antlr	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \to {Base}_{I} \in L$
31	27	ad2antlr	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to {Base}_{I} = U$
32	31	eqeq1d	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to ({Base}_{I} = \{\underset{˙}{0}\} \leftrightarrow U = \{\underset{˙}{0}\})$
33	32	biimpd	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to ({Base}_{I} = \{\underset{˙}{0}\} \to U = \{\underset{˙}{0}\})$
34	33	necon3bd	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to (\neg U = \{\underset{˙}{0}\} \to {Base}_{I} \neq \{\underset{˙}{0}\})$
35	34	imp	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \to {Base}_{I} \neq \{\underset{˙}{0}\}$
36	30 35	jca	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \to ({Base}_{I} \in L \land {Base}_{I} \neq \{\underset{˙}{0}\})$
37	36	adantr	$⊢ ((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \to ({Base}_{I} \in L \land {Base}_{I} \neq \{\underset{˙}{0}\})$
38		simpr	$⊢ ((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \to x \in {Base}_{I}$
39		eqid	$⊢ 1_{R} = 1_{R}$
40	1 15 39 4	lidldomn1	$⊢ (R \in Domn \land ({Base}_{I} \in L \land {Base}_{I} \neq \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \to (\forall y \in {Base}_{I} (x \cdot_{R} y = y \land y \cdot_{R} x = y) \to x = 1_{R})$
41	26 37 38 40	syl3anc	$⊢ ((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \to (\forall y \in {Base}_{I} (x \cdot_{R} y = y \land y \cdot_{R} x = y) \to x = 1_{R})$
42	25 41	sylbid	$⊢ ((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \to (\forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y) \to x = 1_{R})$
43	42	imp	$⊢ (((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \land \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \to x = 1_{R}$
44	27	ad3antlr	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \to {Base}_{I} = U$
45	44	eleq2d	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \to (x \in {Base}_{I} \leftrightarrow x \in U)$
46	45	biimpd	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \to (x \in {Base}_{I} \to x \in U)$
47	46	imp	$⊢ ((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \to x \in U$
48	47	adantr	$⊢ (((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \land \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \to x \in U$
49	43 48	eqeltrrd	$⊢ (((((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \land x \in {Base}_{I}) \land \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \to 1_{R} \in U$
50	49	rexlimdva2	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \neg U = \{\underset{˙}{0}\}) \to (\exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y) \to 1_{R} \in U)$
51	50	impancom	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \to (\neg U = \{\underset{˙}{0}\} \to 1_{R} \in U)$
52	9	adantr	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to (R \in Ring \land U \in L)$
53	1 3 39	lidl1el	$⊢ (R \in Ring \land U \in L) \to (1_{R} \in U \leftrightarrow U = B)$
54	52 53	syl	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to (1_{R} \in U \leftrightarrow U = B)$
55	54	adantr	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \to (1_{R} \in U \leftrightarrow U = B)$
56	51 55	sylibd	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \to (\neg U = \{\underset{˙}{0}\} \to U = B)$
57	56	orrd	$⊢ (((R \in Domn \land U \in L) \land I \in Rng) \land \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \to (U = \{\underset{˙}{0}\} \lor U = B)$
58	57	ex	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to (\exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y) \to (U = \{\underset{˙}{0}\} \lor U = B))$
59	1 2 3 4	zlidlring	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to I \in Ring$
60	7	simprbi	$⊢ I \in Ring \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)$
61	59 60	syl	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)$
62	61	ex	$⊢ R \in Ring \to (U = \{\underset{˙}{0}\} \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
63	8 62	syl	$⊢ R \in Domn \to (U = \{\underset{˙}{0}\} \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
64	63	ad2antrr	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to (U = \{\underset{˙}{0}\} \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
65	9	anim1i	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to ((R \in Ring \land U \in L) \land I \in Rng)$
66	3 15	ringideu	$⊢ R \in Ring \to \exists! x \in B \forall y \in B (x \cdot_{R} y = y \land y \cdot_{R} x = y)$
67		reurex	$⊢ \exists! x \in B \forall y \in B (x \cdot_{R} y = y \land y \cdot_{R} x = y) \to \exists x \in B \forall y \in B (x \cdot_{R} y = y \land y \cdot_{R} x = y)$
68	66 67	syl	$⊢ R \in Ring \to \exists x \in B \forall y \in B (x \cdot_{R} y = y \land y \cdot_{R} x = y)$
69	68	adantr	$⊢ (R \in Ring \land U \in L) \to \exists x \in B \forall y \in B (x \cdot_{R} y = y \land y \cdot_{R} x = y)$
70	69	ad2antrr	$⊢ (((R \in Ring \land U \in L) \land I \in Rng) \land U = B) \to \exists x \in B \forall y \in B (x \cdot_{R} y = y \land y \cdot_{R} x = y)$
71	2 3	ressbas	$⊢ U \in L \to U \cap B = {Base}_{I}$
72	71	ad3antlr	$⊢ (((R \in Ring \land U \in L) \land I \in Rng) \land U = B) \to U \cap B = {Base}_{I}$
73		ineq1	$⊢ U = B \to U \cap B = B \cap B$
74		inidm	$⊢ B \cap B = B$
75	73 74	eqtrdi	$⊢ U = B \to U \cap B = B$
76	75	adantl	$⊢ (((R \in Ring \land U \in L) \land I \in Rng) \land U = B) \to U \cap B = B$
77	72 76	eqtr3d	$⊢ (((R \in Ring \land U \in L) \land I \in Rng) \land U = B) \to {Base}_{I} = B$
78	22	ad3antlr	$⊢ (((R \in Ring \land U \in L) \land I \in Rng) \land U = B) \to ((x \cdot_{I} y = y \land y \cdot_{I} x = y) \leftrightarrow (x \cdot_{R} y = y \land y \cdot_{R} x = y))$
79	77 78	raleqbidv	$⊢ (((R \in Ring \land U \in L) \land I \in Rng) \land U = B) \to (\forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y) \leftrightarrow \forall y \in B (x \cdot_{R} y = y \land y \cdot_{R} x = y))$
80	77 79	rexeqbidv	$⊢ (((R \in Ring \land U \in L) \land I \in Rng) \land U = B) \to (\exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y) \leftrightarrow \exists x \in B \forall y \in B (x \cdot_{R} y = y \land y \cdot_{R} x = y))$
81	70 80	mpbird	$⊢ (((R \in Ring \land U \in L) \land I \in Rng) \land U = B) \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)$
82	81	ex	$⊢ ((R \in Ring \land U \in L) \land I \in Rng) \to (U = B \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
83	65 82	syl	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to (U = B \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
84	64 83	jaod	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to ((U = \{\underset{˙}{0}\} \lor U = B) \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
85	58 84	impbid	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to (\exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y) \leftrightarrow (U = \{\underset{˙}{0}\} \lor U = B))$
86	14 85	bitrd	$⊢ ((R \in Domn \land U \in L) \land I \in Rng) \to ((I \in Rng \land \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \leftrightarrow (U = \{\underset{˙}{0}\} \lor U = B))$
87	11 86	mpdan	$⊢ (R \in Domn \land U \in L) \to ((I \in Rng \land \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)) \leftrightarrow (U = \{\underset{˙}{0}\} \lor U = B))$
88	7 87	bitrid	$⊢ (R \in Domn \land U \in L) \to (I \in Ring \leftrightarrow (U = \{\underset{˙}{0}\} \lor U = B))$

Metamath Proof Explorer

Theorem uzlidlring

Proof