Proof of Theorem ringinvnzdiv
Step | Hyp | Ref
| Expression |
1 | | ringinvnzdiv.a |
. . 3
⊢ (𝜑 → ∃𝑎 ∈ 𝐵 (𝑎 · 𝑋) = 1 ) |
2 | | ringinvnzdiv.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) |
3 | | ringinvnzdiv.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
4 | | ringinvnzdiv.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) |
5 | | ringinvnzdiv.t |
. . . . . . . . . 10
⊢ · =
(.r‘𝑅) |
6 | | ringinvnzdiv.u |
. . . . . . . . . 10
⊢ 1 =
(1r‘𝑅) |
7 | 4, 5, 6 | ringlidm 19810 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵) → ( 1 · 𝑌) = 𝑌) |
8 | 2, 3, 7 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ( 1 · 𝑌) = 𝑌) |
9 | 8 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 → 𝑌 = ( 1 · 𝑌)) |
10 | 9 | ad3antrrr 727 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑎 · 𝑋) = 1 ) ∧ (𝑋 · 𝑌) = 0 ) → 𝑌 = ( 1 · 𝑌)) |
11 | | oveq1 7282 |
. . . . . . . . . 10
⊢ ( 1 = (𝑎 · 𝑋) → ( 1 · 𝑌) = ((𝑎 · 𝑋) · 𝑌)) |
12 | 11 | eqcoms 2746 |
. . . . . . . . 9
⊢ ((𝑎 · 𝑋) = 1 → ( 1 · 𝑌) = ((𝑎 · 𝑋) · 𝑌)) |
13 | 12 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑎 · 𝑋) = 1 ) → ( 1 · 𝑌) = ((𝑎 · 𝑋) · 𝑌)) |
14 | 2 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑅 ∈ Ring) |
15 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
16 | | ringinvnzdiv.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
17 | 16 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
18 | 3 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
19 | 15, 17, 18 | 3jca 1127 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑎 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) |
20 | 14, 19 | jca 512 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑅 ∈ Ring ∧ (𝑎 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))) |
21 | 20 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑎 · 𝑋) = 1 ) → (𝑅 ∈ Ring ∧ (𝑎 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))) |
22 | 4, 5 | ringass 19803 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑎 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑎 · 𝑋) · 𝑌) = (𝑎 · (𝑋 · 𝑌))) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑎 · 𝑋) = 1 ) → ((𝑎 · 𝑋) · 𝑌) = (𝑎 · (𝑋 · 𝑌))) |
24 | 13, 23 | eqtrd 2778 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑎 · 𝑋) = 1 ) → ( 1 · 𝑌) = (𝑎 · (𝑋 · 𝑌))) |
25 | 24 | adantr 481 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑎 · 𝑋) = 1 ) ∧ (𝑋 · 𝑌) = 0 ) → ( 1 · 𝑌) = (𝑎 · (𝑋 · 𝑌))) |
26 | | oveq2 7283 |
. . . . . . 7
⊢ ((𝑋 · 𝑌) = 0 → (𝑎 · (𝑋 · 𝑌)) = (𝑎 · 0 )) |
27 | | ringinvnzdiv.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑅) |
28 | 4, 5, 27 | ringrz 19827 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → (𝑎 · 0 ) = 0 ) |
29 | 2, 28 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑎 · 0 ) = 0 ) |
30 | 29 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑎 · 𝑋) = 1 ) → (𝑎 · 0 ) = 0 ) |
31 | 26, 30 | sylan9eqr 2800 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑎 · 𝑋) = 1 ) ∧ (𝑋 · 𝑌) = 0 ) → (𝑎 · (𝑋 · 𝑌)) = 0 ) |
32 | 10, 25, 31 | 3eqtrd 2782 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑎 · 𝑋) = 1 ) ∧ (𝑋 · 𝑌) = 0 ) → 𝑌 = 0 ) |
33 | 32 | exp31 420 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑎 · 𝑋) = 1 → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 ))) |
34 | 33 | rexlimdva 3213 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ 𝐵 (𝑎 · 𝑋) = 1 → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 ))) |
35 | 1, 34 | mpd 15 |
. 2
⊢ (𝜑 → ((𝑋 · 𝑌) = 0 → 𝑌 = 0 )) |
36 | | oveq2 7283 |
. . . 4
⊢ (𝑌 = 0 → (𝑋 · 𝑌) = (𝑋 · 0 )) |
37 | 4, 5, 27 | ringrz 19827 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 · 0 ) = 0 ) |
38 | 2, 16, 37 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑋 · 0 ) = 0 ) |
39 | 36, 38 | sylan9eqr 2800 |
. . 3
⊢ ((𝜑 ∧ 𝑌 = 0 ) → (𝑋 · 𝑌) = 0 ) |
40 | 39 | ex 413 |
. 2
⊢ (𝜑 → (𝑌 = 0 → (𝑋 · 𝑌) = 0 )) |
41 | 35, 40 | impbid 211 |
1
⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ 𝑌 = 0 )) |