Metamath Proof Explorer

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 rngsubdir ⊢ ( ( ( 𝑅 ∈ 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 ) )