| Step | Hyp | Ref
| Expression |
| 1 | | domnring 20707 |
. . . 4
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) |
| 2 | 1 | 3ad2ant1 1134 |
. . 3
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝑅 ∈ Ring) |
| 3 | | simp2l 1200 |
. . 3
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝑈 ∈ 𝐿) |
| 4 | | simp2r 1201 |
. . 3
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝑈 ≠ { 0 }) |
| 5 | | lidldomn1.l |
. . . 4
⊢ 𝐿 = (LIdeal‘𝑅) |
| 6 | | lidldomn1.0 |
. . . 4
⊢ 0 =
(0g‘𝑅) |
| 7 | 5, 6 | lidlnz 21252 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) → ∃𝑦 ∈ 𝑈 𝑦 ≠ 0 ) |
| 8 | 2, 3, 4, 7 | syl3anc 1373 |
. 2
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → ∃𝑦 ∈ 𝑈 𝑦 ≠ 0 ) |
| 9 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐼 · 𝑥) = (𝐼 · 𝑦)) |
| 10 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
| 11 | 9, 10 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝐼 · 𝑥) = 𝑥 ↔ (𝐼 · 𝑦) = 𝑦)) |
| 12 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 · 𝐼) = (𝑦 · 𝐼)) |
| 13 | 12, 10 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑥 · 𝐼) = 𝑥 ↔ (𝑦 · 𝐼) = 𝑦)) |
| 14 | 11, 13 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) ↔ ((𝐼 · 𝑦) = 𝑦 ∧ (𝑦 · 𝐼) = 𝑦))) |
| 15 | 14 | rspcva 3620 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥)) → ((𝐼 · 𝑦) = 𝑦 ∧ (𝑦 · 𝐼) = 𝑦)) |
| 16 | 2 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → 𝑅 ∈ Ring) |
| 17 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 18 | 17, 5 | lidlss 21222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 ∈ 𝐿 → 𝑈 ⊆ (Base‘𝑅)) |
| 19 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) → 𝑈 ⊆ (Base‘𝑅)) |
| 20 | 19 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝑈 ⊆ (Base‘𝑅)) |
| 21 | 20 | sseld 3982 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → (𝑦 ∈ 𝑈 → 𝑦 ∈ (Base‘𝑅))) |
| 22 | 21 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑈 → ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝑦 ∈ (Base‘𝑅))) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) → ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝑦 ∈ (Base‘𝑅))) |
| 24 | 23 | impcom 407 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → 𝑦 ∈ (Base‘𝑅)) |
| 25 | | lidldomn1.t |
. . . . . . . . . . . . . . 15
⊢ · =
(.r‘𝑅) |
| 26 | | lidldomn1.1 |
. . . . . . . . . . . . . . 15
⊢ 1 =
(1r‘𝑅) |
| 27 | 17, 25, 26 | ringlidm 20266 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ (Base‘𝑅)) → ( 1 · 𝑦) = 𝑦) |
| 28 | 16, 24, 27 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → ( 1 · 𝑦) = 𝑦) |
| 29 | | eqeq2 2749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ( 1 · 𝑦) → ((𝐼 · 𝑦) = 𝑦 ↔ (𝐼 · 𝑦) = ( 1 · 𝑦))) |
| 30 | 29 | eqcoms 2745 |
. . . . . . . . . . . . . . 15
⊢ (( 1 · 𝑦) = 𝑦 → ((𝐼 · 𝑦) = 𝑦 ↔ (𝐼 · 𝑦) = ( 1 · 𝑦))) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) ∧ ( 1 · 𝑦) = 𝑦) → ((𝐼 · 𝑦) = 𝑦 ↔ (𝐼 · 𝑦) = ( 1 · 𝑦))) |
| 32 | | ringgrp 20235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 33 | 1, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Grp) |
| 34 | 33 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝑅 ∈ Grp) |
| 35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → 𝑅 ∈ Grp) |
| 36 | 19 | sseld 3982 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) → (𝐼 ∈ 𝑈 → 𝐼 ∈ (Base‘𝑅))) |
| 37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ Domn → ((𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) → (𝐼 ∈ 𝑈 → 𝐼 ∈ (Base‘𝑅)))) |
| 38 | 37 | 3imp 1111 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝐼 ∈ (Base‘𝑅)) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → 𝐼 ∈ (Base‘𝑅)) |
| 40 | 17, 25 | ringcl 20247 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐼 · 𝑦) ∈ (Base‘𝑅)) |
| 41 | 16, 39, 24, 40 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → (𝐼 · 𝑦) ∈ (Base‘𝑅)) |
| 42 | 17, 26 | ringidcl 20262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Ring → 1 ∈
(Base‘𝑅)) |
| 43 | 1, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ Domn → 1 ∈
(Base‘𝑅)) |
| 44 | 43 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 1 ∈ (Base‘𝑅)) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → 1 ∈
(Base‘𝑅)) |
| 46 | 17, 25 | ringcl 20247 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ Ring ∧ 1 ∈
(Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → ( 1 · 𝑦) ∈ (Base‘𝑅)) |
| 47 | 16, 45, 24, 46 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → ( 1 · 𝑦) ∈ (Base‘𝑅)) |
| 48 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(-g‘𝑅) = (-g‘𝑅) |
| 49 | 17, 6, 48 | grpsubeq0 19044 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Grp ∧ (𝐼 · 𝑦) ∈ (Base‘𝑅) ∧ ( 1 · 𝑦) ∈ (Base‘𝑅)) → (((𝐼 · 𝑦)(-g‘𝑅)( 1 · 𝑦)) = 0 ↔ (𝐼 · 𝑦) = ( 1 · 𝑦))) |
| 50 | 35, 41, 47, 49 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → (((𝐼 · 𝑦)(-g‘𝑅)( 1 · 𝑦)) = 0 ↔ (𝐼 · 𝑦) = ( 1 · 𝑦))) |
| 51 | 17, 25, 48, 16, 39, 45, 24 | ringsubdir 20305 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → ((𝐼(-g‘𝑅) 1 ) · 𝑦) = ((𝐼 · 𝑦)(-g‘𝑅)( 1 · 𝑦))) |
| 52 | 51 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → (((𝐼(-g‘𝑅) 1 ) · 𝑦) = 0 ↔ ((𝐼 · 𝑦)(-g‘𝑅)( 1 · 𝑦)) = 0 )) |
| 53 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → 𝑅 ∈ Domn) |
| 54 | 34, 38, 44 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → (𝑅 ∈ Grp ∧ 𝐼 ∈ (Base‘𝑅) ∧ 1 ∈ (Base‘𝑅))) |
| 55 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → (𝑅 ∈ Grp ∧ 𝐼 ∈ (Base‘𝑅) ∧ 1 ∈ (Base‘𝑅))) |
| 56 | 17, 48 | grpsubcl 19038 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (Base‘𝑅) ∧ 1 ∈ (Base‘𝑅)) → (𝐼(-g‘𝑅) 1 ) ∈ (Base‘𝑅)) |
| 57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → (𝐼(-g‘𝑅) 1 ) ∈ (Base‘𝑅)) |
| 58 | 17, 25, 6 | domneq0 20708 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Domn ∧ (𝐼(-g‘𝑅) 1 ) ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (((𝐼(-g‘𝑅) 1 ) · 𝑦) = 0 ↔ ((𝐼(-g‘𝑅) 1 ) = 0 ∨ 𝑦 = 0 ))) |
| 59 | 53, 57, 24, 58 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → (((𝐼(-g‘𝑅) 1 ) · 𝑦) = 0 ↔ ((𝐼(-g‘𝑅) 1 ) = 0 ∨ 𝑦 = 0 ))) |
| 60 | 17, 6, 48 | grpsubeq0 19044 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ (Base‘𝑅) ∧ 1 ∈ (Base‘𝑅)) → ((𝐼(-g‘𝑅) 1 ) = 0 ↔ 𝐼 = 1 )) |
| 61 | 55, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → ((𝐼(-g‘𝑅) 1 ) = 0 ↔ 𝐼 = 1 )) |
| 62 | 61 | biimpd 229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → ((𝐼(-g‘𝑅) 1 ) = 0 → 𝐼 = 1 )) |
| 63 | | eqneqall 2951 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 0 → (𝑦 ≠ 0 → 𝐼 = 1 )) |
| 64 | 63 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ≠ 0 → (𝑦 = 0 → 𝐼 = 1 )) |
| 65 | 64 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) → (𝑦 = 0 → 𝐼 = 1 )) |
| 66 | 65 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → (𝑦 = 0 → 𝐼 = 1 )) |
| 67 | 62, 66 | jaod 860 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → (((𝐼(-g‘𝑅) 1 ) = 0 ∨ 𝑦 = 0 ) → 𝐼 = 1 )) |
| 68 | 59, 67 | sylbid 240 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → (((𝐼(-g‘𝑅) 1 ) · 𝑦) = 0 → 𝐼 = 1 )) |
| 69 | 52, 68 | sylbird 260 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → (((𝐼 · 𝑦)(-g‘𝑅)( 1 · 𝑦)) = 0 → 𝐼 = 1 )) |
| 70 | 50, 69 | sylbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → ((𝐼 · 𝑦) = ( 1 · 𝑦) → 𝐼 = 1 )) |
| 71 | 70 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) ∧ ( 1 · 𝑦) = 𝑦) → ((𝐼 · 𝑦) = ( 1 · 𝑦) → 𝐼 = 1 )) |
| 72 | 31, 71 | sylbid 240 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) ∧ ( 1 · 𝑦) = 𝑦) → ((𝐼 · 𝑦) = 𝑦 → 𝐼 = 1 )) |
| 73 | 28, 72 | mpdan 687 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ (𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 )) → ((𝐼 · 𝑦) = 𝑦 → 𝐼 = 1 )) |
| 74 | 73 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → ((𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) → ((𝐼 · 𝑦) = 𝑦 → 𝐼 = 1 ))) |
| 75 | 74 | com13 88 |
. . . . . . . . . 10
⊢ ((𝐼 · 𝑦) = 𝑦 → ((𝑦 ∈ 𝑈 ∧ 𝑦 ≠ 0 ) → ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝐼 = 1 ))) |
| 76 | 75 | expd 415 |
. . . . . . . . 9
⊢ ((𝐼 · 𝑦) = 𝑦 → (𝑦 ∈ 𝑈 → (𝑦 ≠ 0 → ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝐼 = 1 )))) |
| 77 | 76 | adantr 480 |
. . . . . . . 8
⊢ (((𝐼 · 𝑦) = 𝑦 ∧ (𝑦 · 𝐼) = 𝑦) → (𝑦 ∈ 𝑈 → (𝑦 ≠ 0 → ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝐼 = 1 )))) |
| 78 | 15, 77 | syl 17 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥)) → (𝑦 ∈ 𝑈 → (𝑦 ≠ 0 → ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝐼 = 1 )))) |
| 79 | 78 | ex 412 |
. . . . . 6
⊢ (𝑦 ∈ 𝑈 → (∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) → (𝑦 ∈ 𝑈 → (𝑦 ≠ 0 → ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝐼 = 1 ))))) |
| 80 | 79 | pm2.43b 55 |
. . . . 5
⊢
(∀𝑥 ∈
𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) → (𝑦 ∈ 𝑈 → (𝑦 ≠ 0 → ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → 𝐼 = 1 )))) |
| 81 | 80 | com14 96 |
. . . 4
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → (𝑦 ∈ 𝑈 → (𝑦 ≠ 0 → (∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) → 𝐼 = 1 )))) |
| 82 | 81 | imp 406 |
. . 3
⊢ (((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) ∧ 𝑦 ∈ 𝑈) → (𝑦 ≠ 0 → (∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) → 𝐼 = 1 ))) |
| 83 | 82 | rexlimdva 3155 |
. 2
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → (∃𝑦 ∈ 𝑈 𝑦 ≠ 0 → (∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) → 𝐼 = 1 ))) |
| 84 | 8, 83 | mpd 15 |
1
⊢ ((𝑅 ∈ Domn ∧ (𝑈 ∈ 𝐿 ∧ 𝑈 ≠ { 0 }) ∧ 𝐼 ∈ 𝑈) → (∀𝑥 ∈ 𝑈 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥) → 𝐼 = 1 )) |