lidldomn1

Description: If a (left) ideal (which is not the zero ideal) of a domain has a multiplicative identity element, the identity element is the identity of the domain. (Contributed by AV, 17-Feb-2020)

	Ref	Expression
Hypotheses	lidldomn1.l	$⊢ L = LIdeal (R)$
	lidldomn1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	lidldomn1.1	$⊢ \underset{˙}{1} = 1_{R}$
	lidldomn1.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	lidldomn1	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to (\forall x \in U (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x) \to I = \underset{˙}{1})$

Proof

Step	Hyp	Ref	Expression
1		lidldomn1.l	$⊢ L = LIdeal (R)$
2		lidldomn1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		lidldomn1.1	$⊢ \underset{˙}{1} = 1_{R}$
4		lidldomn1.0	$⊢ \underset{˙}{0} = 0_{R}$
5		domnring	$⊢ R \in Domn \to R \in Ring$
6	5	3ad2ant1	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to R \in Ring$
7		simp2l	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to U \in L$
8		simp2r	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to U \neq \{\underset{˙}{0}\}$
9	1 4	lidlnz	$⊢ (R \in Ring \land U \in L \land U \neq \{\underset{˙}{0}\}) \to \exists y \in U y \neq \underset{˙}{0}$
10	6 7 8 9	syl3anc	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to \exists y \in U y \neq \underset{˙}{0}$
11		oveq2	$⊢ x = y \to I \underset{˙}{\cdot} x = I \underset{˙}{\cdot} y$
12		id	$⊢ x = y \to x = y$
13	11 12	eqeq12d	$⊢ x = y \to (I \underset{˙}{\cdot} x = x \leftrightarrow I \underset{˙}{\cdot} y = y)$
14		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} I = y \underset{˙}{\cdot} I$
15	14 12	eqeq12d	$⊢ x = y \to (x \underset{˙}{\cdot} I = x \leftrightarrow y \underset{˙}{\cdot} I = y)$
16	13 15	anbi12d	$⊢ x = y \to ((I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x) \leftrightarrow (I \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} I = y))$
17	16	rspcva	$⊢ (y \in U \land \forall x \in U (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x)) \to (I \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} I = y)$
18	6	adantr	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to R \in Ring$
19		eqid	$⊢ {Base}_{R} = {Base}_{R}$
20	19 1	lidlss	$⊢ U \in L \to U \subseteq {Base}_{R}$
21	20	adantr	$⊢ (U \in L \land U \neq \{\underset{˙}{0}\}) \to U \subseteq {Base}_{R}$
22	21	3ad2ant2	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to U \subseteq {Base}_{R}$
23	22	sseld	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to (y \in U \to y \in {Base}_{R})$
24	23	com12	$⊢ y \in U \to ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to y \in {Base}_{R})$
25	24	adantr	$⊢ (y \in U \land y \neq \underset{˙}{0}) \to ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to y \in {Base}_{R})$
26	25	impcom	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to y \in {Base}_{R}$
27	19 2 3	ringlidm	$⊢ (R \in Ring \land y \in {Base}_{R}) \to \underset{˙}{1} \underset{˙}{\cdot} y = y$
28	18 26 27	syl2anc	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to \underset{˙}{1} \underset{˙}{\cdot} y = y$
29		eqeq2	$⊢ y = \underset{˙}{1} \underset{˙}{\cdot} y \to (I \underset{˙}{\cdot} y = y \leftrightarrow I \underset{˙}{\cdot} y = \underset{˙}{1} \underset{˙}{\cdot} y)$
30	29	eqcoms	$⊢ \underset{˙}{1} \underset{˙}{\cdot} y = y \to (I \underset{˙}{\cdot} y = y \leftrightarrow I \underset{˙}{\cdot} y = \underset{˙}{1} \underset{˙}{\cdot} y)$
31	30	adantl	$⊢ (((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \land \underset{˙}{1} \underset{˙}{\cdot} y = y) \to (I \underset{˙}{\cdot} y = y \leftrightarrow I \underset{˙}{\cdot} y = \underset{˙}{1} \underset{˙}{\cdot} y)$
32		ringgrp	$⊢ R \in Ring \to R \in Grp$
33	5 32	syl	$⊢ R \in Domn \to R \in Grp$
34	33	3ad2ant1	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to R \in Grp$
35	34	adantr	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to R \in Grp$
36	21	sseld	$⊢ (U \in L \land U \neq \{\underset{˙}{0}\}) \to (I \in U \to I \in {Base}_{R})$
37	36	a1i	$⊢ R \in Domn \to ((U \in L \land U \neq \{\underset{˙}{0}\}) \to (I \in U \to I \in {Base}_{R}))$
38	37	3imp	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to I \in {Base}_{R}$
39	38	adantr	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to I \in {Base}_{R}$
40	19 2	ringcl	$⊢ (R \in Ring \land I \in {Base}_{R} \land y \in {Base}_{R}) \to I \underset{˙}{\cdot} y \in {Base}_{R}$
41	18 39 26 40	syl3anc	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to I \underset{˙}{\cdot} y \in {Base}_{R}$
42	19 3	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
43	5 42	syl	$⊢ R \in Domn \to \underset{˙}{1} \in {Base}_{R}$
44	43	3ad2ant1	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to \underset{˙}{1} \in {Base}_{R}$
45	44	adantr	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to \underset{˙}{1} \in {Base}_{R}$
46	19 2	ringcl	$⊢ (R \in Ring \land \underset{˙}{1} \in {Base}_{R} \land y \in {Base}_{R}) \to \underset{˙}{1} \underset{˙}{\cdot} y \in {Base}_{R}$
47	18 45 26 46	syl3anc	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to \underset{˙}{1} \underset{˙}{\cdot} y \in {Base}_{R}$
48		eqid	$⊢ -_{R} = -_{R}$
49	19 4 48	grpsubeq0	$⊢ (R \in Grp \land I \underset{˙}{\cdot} y \in {Base}_{R} \land \underset{˙}{1} \underset{˙}{\cdot} y \in {Base}_{R}) \to ((I \underset{˙}{\cdot} y) -_{R} (\underset{˙}{1} \underset{˙}{\cdot} y) = \underset{˙}{0} \leftrightarrow I \underset{˙}{\cdot} y = \underset{˙}{1} \underset{˙}{\cdot} y)$
50	35 41 47 49	syl3anc	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to ((I \underset{˙}{\cdot} y) -_{R} (\underset{˙}{1} \underset{˙}{\cdot} y) = \underset{˙}{0} \leftrightarrow I \underset{˙}{\cdot} y = \underset{˙}{1} \underset{˙}{\cdot} y)$
51	19 2 48 18 39 45 26	ringsubdir	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to (I -_{R} \underset{˙}{1}) \underset{˙}{\cdot} y = (I \underset{˙}{\cdot} y) -_{R} (\underset{˙}{1} \underset{˙}{\cdot} y)$
52	51	eqeq1d	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to ((I -_{R} \underset{˙}{1}) \underset{˙}{\cdot} y = \underset{˙}{0} \leftrightarrow (I \underset{˙}{\cdot} y) -_{R} (\underset{˙}{1} \underset{˙}{\cdot} y) = \underset{˙}{0})$
53		simpl1	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to R \in Domn$
54	34 38 44	3jca	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to (R \in Grp \land I \in {Base}_{R} \land \underset{˙}{1} \in {Base}_{R})$
55	54	adantr	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to (R \in Grp \land I \in {Base}_{R} \land \underset{˙}{1} \in {Base}_{R})$
56	19 48	grpsubcl	$⊢ (R \in Grp \land I \in {Base}_{R} \land \underset{˙}{1} \in {Base}_{R}) \to I -_{R} \underset{˙}{1} \in {Base}_{R}$
57	55 56	syl	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to I -_{R} \underset{˙}{1} \in {Base}_{R}$
58	19 2 4	domneq0	$⊢ (R \in Domn \land I -_{R} \underset{˙}{1} \in {Base}_{R} \land y \in {Base}_{R}) \to ((I -_{R} \underset{˙}{1}) \underset{˙}{\cdot} y = \underset{˙}{0} \leftrightarrow (I -_{R} \underset{˙}{1} = \underset{˙}{0} \lor y = \underset{˙}{0}))$
59	53 57 26 58	syl3anc	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to ((I -_{R} \underset{˙}{1}) \underset{˙}{\cdot} y = \underset{˙}{0} \leftrightarrow (I -_{R} \underset{˙}{1} = \underset{˙}{0} \lor y = \underset{˙}{0}))$
60	19 4 48	grpsubeq0	$⊢ (R \in Grp \land I \in {Base}_{R} \land \underset{˙}{1} \in {Base}_{R}) \to (I -_{R} \underset{˙}{1} = \underset{˙}{0} \leftrightarrow I = \underset{˙}{1})$
61	55 60	syl	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to (I -_{R} \underset{˙}{1} = \underset{˙}{0} \leftrightarrow I = \underset{˙}{1})$
62	61	biimpd	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to (I -_{R} \underset{˙}{1} = \underset{˙}{0} \to I = \underset{˙}{1})$
63		eqneqall	$⊢ y = \underset{˙}{0} \to (y \neq \underset{˙}{0} \to I = \underset{˙}{1})$
64	63	com12	$⊢ y \neq \underset{˙}{0} \to (y = \underset{˙}{0} \to I = \underset{˙}{1})$
65	64	adantl	$⊢ (y \in U \land y \neq \underset{˙}{0}) \to (y = \underset{˙}{0} \to I = \underset{˙}{1})$
66	65	adantl	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to (y = \underset{˙}{0} \to I = \underset{˙}{1})$
67	62 66	jaod	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to ((I -_{R} \underset{˙}{1} = \underset{˙}{0} \lor y = \underset{˙}{0}) \to I = \underset{˙}{1})$
68	59 67	sylbid	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to ((I -_{R} \underset{˙}{1}) \underset{˙}{\cdot} y = \underset{˙}{0} \to I = \underset{˙}{1})$
69	52 68	sylbird	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to ((I \underset{˙}{\cdot} y) -_{R} (\underset{˙}{1} \underset{˙}{\cdot} y) = \underset{˙}{0} \to I = \underset{˙}{1})$
70	50 69	sylbird	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to (I \underset{˙}{\cdot} y = \underset{˙}{1} \underset{˙}{\cdot} y \to I = \underset{˙}{1})$
71	70	adantr	$⊢ (((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \land \underset{˙}{1} \underset{˙}{\cdot} y = y) \to (I \underset{˙}{\cdot} y = \underset{˙}{1} \underset{˙}{\cdot} y \to I = \underset{˙}{1})$
72	31 71	sylbid	$⊢ (((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \land \underset{˙}{1} \underset{˙}{\cdot} y = y) \to (I \underset{˙}{\cdot} y = y \to I = \underset{˙}{1})$
73	28 72	mpdan	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land (y \in U \land y \neq \underset{˙}{0})) \to (I \underset{˙}{\cdot} y = y \to I = \underset{˙}{1})$
74	73	ex	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to ((y \in U \land y \neq \underset{˙}{0}) \to (I \underset{˙}{\cdot} y = y \to I = \underset{˙}{1}))$
75	74	com13	$⊢ I \underset{˙}{\cdot} y = y \to ((y \in U \land y \neq \underset{˙}{0}) \to ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to I = \underset{˙}{1}))$
76	75	expd	$⊢ I \underset{˙}{\cdot} y = y \to (y \in U \to (y \neq \underset{˙}{0} \to ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to I = \underset{˙}{1})))$
77	76	adantr	$⊢ (I \underset{˙}{\cdot} y = y \land y \underset{˙}{\cdot} I = y) \to (y \in U \to (y \neq \underset{˙}{0} \to ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to I = \underset{˙}{1})))$
78	17 77	syl	$⊢ (y \in U \land \forall x \in U (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x)) \to (y \in U \to (y \neq \underset{˙}{0} \to ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to I = \underset{˙}{1})))$
79	78	ex	$⊢ y \in U \to (\forall x \in U (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x) \to (y \in U \to (y \neq \underset{˙}{0} \to ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to I = \underset{˙}{1}))))$
80	79	pm2.43b	$⊢ \forall x \in U (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x) \to (y \in U \to (y \neq \underset{˙}{0} \to ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to I = \underset{˙}{1})))$
81	80	com14	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to (y \in U \to (y \neq \underset{˙}{0} \to (\forall x \in U (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x) \to I = \underset{˙}{1})))$
82	81	imp	$⊢ ((R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \land y \in U) \to (y \neq \underset{˙}{0} \to (\forall x \in U (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x) \to I = \underset{˙}{1}))$
83	82	rexlimdva	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to (\exists y \in U y \neq \underset{˙}{0} \to (\forall x \in U (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x) \to I = \underset{˙}{1}))$
84	10 83	mpd	$⊢ (R \in Domn \land (U \in L \land U \neq \{\underset{˙}{0}\}) \land I \in U) \to (\forall x \in U (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x) \to I = \underset{˙}{1})$

Metamath Proof Explorer

Theorem lidldomn1

Proof