Theorem 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	⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
	lidldomn1.t	⊢ · = ( .r ‘ 𝑅 )
	lidldomn1.1	⊢ 1 = ( 1r ‘ 𝑅 )
	lidldomn1.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	lidldomn1	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝑈 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) → 𝐼 = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		lidldomn1.l	⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2		lidldomn1.t	⊢ · = ( .r ‘ 𝑅 )
3		lidldomn1.1	⊢ 1 = ( 1r ‘ 𝑅 )
4		lidldomn1.0	⊢ 0 = ( 0g ‘ 𝑅 )
5		domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
6	5	3ad2ant1	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝑅 ∈ Ring )
7		simp2l	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝑈 ∈ 𝐿 )
8		simp2r	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝑈 ≠ { 0 } )
9	1 4	lidlnz	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) → ∃ 𝑦 ∈ 𝑈 𝑦 ≠ 0 )
10	6 7 8 9	syl3anc	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → ∃ 𝑦 ∈ 𝑈 𝑦 ≠ 0 )
11		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐼 · 𝑥 ) = ( 𝐼 · 𝑦 ) )
12		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
13	11 12	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐼 · 𝑥 ) = 𝑥 ↔ ( 𝐼 · 𝑦 ) = 𝑦 ) )
14		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 · 𝐼 ) = ( 𝑦 · 𝐼 ) )
15	14 12	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 · 𝐼 ) = 𝑥 ↔ ( 𝑦 · 𝐼 ) = 𝑦 ) )
16	13 15	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) ↔ ( ( 𝐼 · 𝑦 ) = 𝑦 ∧ ( 𝑦 · 𝐼 ) = 𝑦 ) ) )
17	16	rspcva	⊢ ( ( 𝑦 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) ) → ( ( 𝐼 · 𝑦 ) = 𝑦 ∧ ( 𝑦 · 𝐼 ) = 𝑦 ) )
18	6	adantr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → 𝑅 ∈ Ring )
19		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20	19 1	lidlss	⊢ ( 𝑈 ∈ 𝐿 → 𝑈 ⊆ ( Base ‘ 𝑅 ) )
21	20	adantr	⊢ ( ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) → 𝑈 ⊆ ( Base ‘ 𝑅 ) )
22	21	3ad2ant2	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝑈 ⊆ ( Base ‘ 𝑅 ) )
23	22	sseld	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → ( 𝑦 ∈ 𝑈 → 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
24	23	com12	⊢ ( 𝑦 ∈ 𝑈 → ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
25	24	adantr	⊢ ( ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) → ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
26	25	impcom	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
27	19 2 3	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 1 · 𝑦 ) = 𝑦 )
28	18 26 27	syl2anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( 1 · 𝑦 ) = 𝑦 )
29		eqeq2	⊢ ( 𝑦 = ( 1 · 𝑦 ) → ( ( 𝐼 · 𝑦 ) = 𝑦 ↔ ( 𝐼 · 𝑦 ) = ( 1 · 𝑦 ) ) )
30	29	eqcoms	⊢ ( ( 1 · 𝑦 ) = 𝑦 → ( ( 𝐼 · 𝑦 ) = 𝑦 ↔ ( 𝐼 · 𝑦 ) = ( 1 · 𝑦 ) ) )
31	30	adantl	⊢ ( ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) ∧ ( 1 · 𝑦 ) = 𝑦 ) → ( ( 𝐼 · 𝑦 ) = 𝑦 ↔ ( 𝐼 · 𝑦 ) = ( 1 · 𝑦 ) ) )
32		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
33	5 32	syl	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Grp )
34	33	3ad2ant1	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝑅 ∈ Grp )
35	34	adantr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → 𝑅 ∈ Grp )
36	21	sseld	⊢ ( ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) → ( 𝐼 ∈ 𝑈 → 𝐼 ∈ ( Base ‘ 𝑅 ) ) )
37	36	a1i	⊢ ( 𝑅 ∈ Domn → ( ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) → ( 𝐼 ∈ 𝑈 → 𝐼 ∈ ( Base ‘ 𝑅 ) ) ) )
38	37	3imp	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ ( Base ‘ 𝑅 ) )
39	38	adantr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → 𝐼 ∈ ( Base ‘ 𝑅 ) )
40	19 2	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
41	18 39 26 40	syl3anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( 𝐼 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
42	19 3	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
43	5 42	syl	⊢ ( 𝑅 ∈ Domn → 1 ∈ ( Base ‘ 𝑅 ) )
44	43	3ad2ant1	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 1 ∈ ( Base ‘ 𝑅 ) )
45	44	adantr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → 1 ∈ ( Base ‘ 𝑅 ) )
46	19 2	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 1 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
47	18 45 26 46	syl3anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( 1 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
48		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
49	19 4 48	grpsubeq0	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐼 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1 · 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝐼 · 𝑦 ) ( -g ‘ 𝑅 ) ( 1 · 𝑦 ) ) = 0 ↔ ( 𝐼 · 𝑦 ) = ( 1 · 𝑦 ) ) )
50	35 41 47 49	syl3anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( ( 𝐼 · 𝑦 ) ( -g ‘ 𝑅 ) ( 1 · 𝑦 ) ) = 0 ↔ ( 𝐼 · 𝑦 ) = ( 1 · 𝑦 ) ) )
51	19 2 48 18 39 45 26	ringsubdir	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) · 𝑦 ) = ( ( 𝐼 · 𝑦 ) ( -g ‘ 𝑅 ) ( 1 · 𝑦 ) ) )
52	51	eqeq1d	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) · 𝑦 ) = 0 ↔ ( ( 𝐼 · 𝑦 ) ( -g ‘ 𝑅 ) ( 1 · 𝑦 ) ) = 0 ) )
53		simpl1	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → 𝑅 ∈ Domn )
54	34 38 44	3jca	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( Base ‘ 𝑅 ) ∧ 1 ∈ ( Base ‘ 𝑅 ) ) )
55	54	adantr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( Base ‘ 𝑅 ) ∧ 1 ∈ ( Base ‘ 𝑅 ) ) )
56	19 48	grpsubcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( Base ‘ 𝑅 ) ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ( -g ‘ 𝑅 ) 1 ) ∈ ( Base ‘ 𝑅 ) )
57	55 56	syl	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( 𝐼 ( -g ‘ 𝑅 ) 1 ) ∈ ( Base ‘ 𝑅 ) )
58	19 2 4	domneq0	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝐼 ( -g ‘ 𝑅 ) 1 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) · 𝑦 ) = 0 ↔ ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) = 0 ∨ 𝑦 = 0 ) ) )
59	53 57 26 58	syl3anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) · 𝑦 ) = 0 ↔ ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) = 0 ∨ 𝑦 = 0 ) ) )
60	19 4 48	grpsubeq0	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( Base ‘ 𝑅 ) ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) = 0 ↔ 𝐼 = 1 ) )
61	55 60	syl	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) = 0 ↔ 𝐼 = 1 ) )
62	61	biimpd	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) = 0 → 𝐼 = 1 ) )
63		eqneqall	⊢ ( 𝑦 = 0 → ( 𝑦 ≠ 0 → 𝐼 = 1 ) )
64	63	com12	⊢ ( 𝑦 ≠ 0 → ( 𝑦 = 0 → 𝐼 = 1 ) )
65	64	adantl	⊢ ( ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) → ( 𝑦 = 0 → 𝐼 = 1 ) )
66	65	adantl	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( 𝑦 = 0 → 𝐼 = 1 ) )
67	62 66	jaod	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) = 0 ∨ 𝑦 = 0 ) → 𝐼 = 1 ) )
68	59 67	sylbid	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( ( 𝐼 ( -g ‘ 𝑅 ) 1 ) · 𝑦 ) = 0 → 𝐼 = 1 ) )
69	52 68	sylbird	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( ( 𝐼 · 𝑦 ) ( -g ‘ 𝑅 ) ( 1 · 𝑦 ) ) = 0 → 𝐼 = 1 ) )
70	50 69	sylbird	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( 𝐼 · 𝑦 ) = ( 1 · 𝑦 ) → 𝐼 = 1 ) )
71	70	adantr	⊢ ( ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) ∧ ( 1 · 𝑦 ) = 𝑦 ) → ( ( 𝐼 · 𝑦 ) = ( 1 · 𝑦 ) → 𝐼 = 1 ) )
72	31 71	sylbid	⊢ ( ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) ∧ ( 1 · 𝑦 ) = 𝑦 ) → ( ( 𝐼 · 𝑦 ) = 𝑦 → 𝐼 = 1 ) )
73	28 72	mpdan	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) ) → ( ( 𝐼 · 𝑦 ) = 𝑦 → 𝐼 = 1 ) )
74	73	ex	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → ( ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) → ( ( 𝐼 · 𝑦 ) = 𝑦 → 𝐼 = 1 ) ) )
75	74	com13	⊢ ( ( 𝐼 · 𝑦 ) = 𝑦 → ( ( 𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) → ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝐼 = 1 ) ) )
76	75	expd	⊢ ( ( 𝐼 · 𝑦 ) = 𝑦 → ( 𝑦 ∈ 𝑈 → ( 𝑦 ≠ 0 → ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝐼 = 1 ) ) ) )
77	76	adantr	⊢ ( ( ( 𝐼 · 𝑦 ) = 𝑦 ∧ ( 𝑦 · 𝐼 ) = 𝑦 ) → ( 𝑦 ∈ 𝑈 → ( 𝑦 ≠ 0 → ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝐼 = 1 ) ) ) )
78	17 77	syl	⊢ ( ( 𝑦 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) ) → ( 𝑦 ∈ 𝑈 → ( 𝑦 ≠ 0 → ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝐼 = 1 ) ) ) )
79	78	ex	⊢ ( 𝑦 ∈ 𝑈 → ( ∀ 𝑥 ∈ 𝑈 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) → ( 𝑦 ∈ 𝑈 → ( 𝑦 ≠ 0 → ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝐼 = 1 ) ) ) ) )
80	79	pm2.43b	⊢ ( ∀ 𝑥 ∈ 𝑈 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) → ( 𝑦 ∈ 𝑈 → ( 𝑦 ≠ 0 → ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → 𝐼 = 1 ) ) ) )
81	80	com14	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → ( 𝑦 ∈ 𝑈 → ( 𝑦 ≠ 0 → ( ∀ 𝑥 ∈ 𝑈 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) → 𝐼 = 1 ) ) ) )
82	81	imp	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝑈 ) → ( 𝑦 ≠ 0 → ( ∀ 𝑥 ∈ 𝑈 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) → 𝐼 = 1 ) ) )
83	82	rexlimdva	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → ( ∃ 𝑦 ∈ 𝑈 𝑦 ≠ 0 → ( ∀ 𝑥 ∈ 𝑈 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) → 𝐼 = 1 ) ) )
84	10 83	mpd	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 } ) ∧ 𝐼 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝑈 ( ( 𝐼 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝐼 ) = 𝑥 ) → 𝐼 = 1 ) )