zlidlring

Description: The zero (left) ideal of a non-unital ring is a unital ring (the zero ring). (Contributed by AV, 16-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	zlidlring	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to I \in Ring$

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	1 4	lidl0	$⊢ R \in Ring \to \{\underset{˙}{0}\} \in L$
6	5	adantr	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to \{\underset{˙}{0}\} \in L$
7		eleq1	$⊢ U = \{\underset{˙}{0}\} \to (U \in L \leftrightarrow \{\underset{˙}{0}\} \in L)$
8	7	adantl	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to (U \in L \leftrightarrow \{\underset{˙}{0}\} \in L)$
9	6 8	mpbird	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to U \in L$
10	1 2	lidlrng	$⊢ (R \in Ring \land U \in L) \to I \in Rng$
11	9 10	syldan	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to I \in Rng$
12		eleq1	$⊢ \{\underset{˙}{0}\} = U \to (\{\underset{˙}{0}\} \in L \leftrightarrow U \in L)$
13	12	eqcoms	$⊢ U = \{\underset{˙}{0}\} \to (\{\underset{˙}{0}\} \in L \leftrightarrow U \in L)$
14	13	adantl	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to (\{\underset{˙}{0}\} \in L \leftrightarrow U \in L)$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16	15 4	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in {Base}_{R}$
17		eqid	$⊢ \cdot_{R} = \cdot_{R}$
18	15 17 4	ringlz	$⊢ (R \in Ring \land \underset{˙}{0} \in {Base}_{R}) \to \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
19	18 18	jca	$⊢ (R \in Ring \land \underset{˙}{0} \in {Base}_{R}) \to (\underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0} \land \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0})$
20	16 19	mpdan	$⊢ R \in Ring \to (\underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0} \land \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0})$
21	4	fvexi	$⊢ \underset{˙}{0} \in V$
22		oveq2	$⊢ y = \underset{˙}{0} \to \underset{˙}{0} \cdot_{R} y = \underset{˙}{0} \cdot_{R} \underset{˙}{0}$
23		id	$⊢ y = \underset{˙}{0} \to y = \underset{˙}{0}$
24	22 23	eqeq12d	$⊢ y = \underset{˙}{0} \to (\underset{˙}{0} \cdot_{R} y = y \leftrightarrow \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0})$
25		oveq1	$⊢ y = \underset{˙}{0} \to y \cdot_{R} \underset{˙}{0} = \underset{˙}{0} \cdot_{R} \underset{˙}{0}$
26	25 23	eqeq12d	$⊢ y = \underset{˙}{0} \to (y \cdot_{R} \underset{˙}{0} = y \leftrightarrow \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0})$
27	24 26	anbi12d	$⊢ y = \underset{˙}{0} \to ((\underset{˙}{0} \cdot_{R} y = y \land y \cdot_{R} \underset{˙}{0} = y) \leftrightarrow (\underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0} \land \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0}))$
28	27	ralsng	$⊢ \underset{˙}{0} \in V \to (\forall y \in \{\underset{˙}{0}\} (\underset{˙}{0} \cdot_{R} y = y \land y \cdot_{R} \underset{˙}{0} = y) \leftrightarrow (\underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0} \land \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0}))$
29	21 28	mp1i	$⊢ R \in Ring \to (\forall y \in \{\underset{˙}{0}\} (\underset{˙}{0} \cdot_{R} y = y \land y \cdot_{R} \underset{˙}{0} = y) \leftrightarrow (\underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0} \land \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0}))$
30	20 29	mpbird	$⊢ R \in Ring \to \forall y \in \{\underset{˙}{0}\} (\underset{˙}{0} \cdot_{R} y = y \land y \cdot_{R} \underset{˙}{0} = y)$
31		oveq1	$⊢ x = \underset{˙}{0} \to x \cdot_{R} y = \underset{˙}{0} \cdot_{R} y$
32	31	eqeq1d	$⊢ x = \underset{˙}{0} \to (x \cdot_{R} y = y \leftrightarrow \underset{˙}{0} \cdot_{R} y = y)$
33	32	ovanraleqv	$⊢ x = \underset{˙}{0} \to (\forall y \in \{\underset{˙}{0}\} (x \cdot_{R} y = y \land y \cdot_{R} x = y) \leftrightarrow \forall y \in \{\underset{˙}{0}\} (\underset{˙}{0} \cdot_{R} y = y \land y \cdot_{R} \underset{˙}{0} = y))$
34	33	rexsng	$⊢ \underset{˙}{0} \in V \to (\exists x \in \{\underset{˙}{0}\} \forall y \in \{\underset{˙}{0}\} (x \cdot_{R} y = y \land y \cdot_{R} x = y) \leftrightarrow \forall y \in \{\underset{˙}{0}\} (\underset{˙}{0} \cdot_{R} y = y \land y \cdot_{R} \underset{˙}{0} = y))$
35	21 34	mp1i	$⊢ R \in Ring \to (\exists x \in \{\underset{˙}{0}\} \forall y \in \{\underset{˙}{0}\} (x \cdot_{R} y = y \land y \cdot_{R} x = y) \leftrightarrow \forall y \in \{\underset{˙}{0}\} (\underset{˙}{0} \cdot_{R} y = y \land y \cdot_{R} \underset{˙}{0} = y))$
36	30 35	mpbird	$⊢ R \in Ring \to \exists x \in \{\underset{˙}{0}\} \forall y \in \{\underset{˙}{0}\} (x \cdot_{R} y = y \land y \cdot_{R} x = y)$
37	36	adantr	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to \exists x \in \{\underset{˙}{0}\} \forall y \in \{\underset{˙}{0}\} (x \cdot_{R} y = y \land y \cdot_{R} x = y)$
38	37	adantr	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land U \in L) \to \exists x \in \{\underset{˙}{0}\} \forall y \in \{\underset{˙}{0}\} (x \cdot_{R} y = y \land y \cdot_{R} x = y)$
39	1 2	lidlbas	$⊢ U \in L \to {Base}_{I} = U$
40		simpr	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to U = \{\underset{˙}{0}\}$
41	39 40	sylan9eqr	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land U \in L) \to {Base}_{I} = \{\underset{˙}{0}\}$
42	2 17	ressmulr	$⊢ U \in L \to \cdot_{R} = \cdot_{I}$
43	42	eqcomd	$⊢ U \in L \to \cdot_{I} = \cdot_{R}$
44	43	adantl	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land U \in L) \to \cdot_{I} = \cdot_{R}$
45	44	oveqd	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land U \in L) \to x \cdot_{I} y = x \cdot_{R} y$
46	45	eqeq1d	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land U \in L) \to (x \cdot_{I} y = y \leftrightarrow x \cdot_{R} y = y)$
47	44	oveqd	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land U \in L) \to y \cdot_{I} x = y \cdot_{R} x$
48	47	eqeq1d	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land U \in L) \to (y \cdot_{I} x = y \leftrightarrow y \cdot_{R} x = y)$
49	46 48	anbi12d	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land 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))$
50	41 49	raleqbidv	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land U \in L) \to (\forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y) \leftrightarrow \forall y \in \{\underset{˙}{0}\} (x \cdot_{R} y = y \land y \cdot_{R} x = y))$
51	41 50	rexeqbidv	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land U \in L) \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 \{\underset{˙}{0}\} \forall y \in \{\underset{˙}{0}\} (x \cdot_{R} y = y \land y \cdot_{R} x = y))$
52	38 51	mpbird	$⊢ ((R \in Ring \land U = \{\underset{˙}{0}\}) \land U \in L) \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y)$
53	52	ex	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to (U \in L \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
54	14 53	sylbid	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to (\{\underset{˙}{0}\} \in L \to \exists x \in {Base}_{I} \forall y \in {Base}_{I} (x \cdot_{I} y = y \land y \cdot_{I} x = y))$
55	6 54	mpd	$⊢ (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)$
56		eqid	$⊢ {Base}_{I} = {Base}_{I}$
57		eqid	$⊢ \cdot_{I} = \cdot_{I}$
58	56 57	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))$
59	11 55 58	sylanbrc	$⊢ (R \in Ring \land U = \{\underset{˙}{0}\}) \to I \in Ring$

Metamath Proof Explorer

Theorem zlidlring

Proof