Step |
Hyp |
Ref |
Expression |
1 |
|
dvrass.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
dvrass.o |
⊢ 𝑈 = ( Unit ‘ 𝑅 ) |
3 |
|
dvrass.d |
⊢ / = ( /r ‘ 𝑅 ) |
4 |
|
dvrass.t |
⊢ · = ( .r ‘ 𝑅 ) |
5 |
|
eqid |
⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 ) |
6 |
1 4 2 5 3
|
dvrval |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) |
7 |
6
|
3adant1 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) |
8 |
7
|
oveq1d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) · 𝑌 ) = ( ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑌 ) ) |
9 |
|
simp1 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑅 ∈ Ring ) |
10 |
|
simp2 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 ) |
11 |
2 5 1
|
ringinvcl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ) |
12 |
11
|
3adant2 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ) |
13 |
1 2
|
unitcl |
⊢ ( 𝑌 ∈ 𝑈 → 𝑌 ∈ 𝐵 ) |
14 |
13
|
3ad2ant3 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ 𝐵 ) |
15 |
1 4
|
ringass |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑌 ) = ( 𝑋 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) ) ) |
16 |
9 10 12 14 15
|
syl13anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑌 ) = ( 𝑋 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) ) ) |
17 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
18 |
2 5 4 17
|
unitlinv |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) = ( 1r ‘ 𝑅 ) ) |
19 |
18
|
3adant2 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) = ( 1r ‘ 𝑅 ) ) |
20 |
19
|
oveq2d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) ) = ( 𝑋 · ( 1r ‘ 𝑅 ) ) ) |
21 |
1 4 17
|
ringridm |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 ) |
22 |
21
|
3adant3 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 ) |
23 |
20 22
|
eqtrd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) ) = 𝑋 ) |
24 |
16 23
|
eqtrd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑌 ) = 𝑋 ) |
25 |
8 24
|
eqtrd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) · 𝑌 ) = 𝑋 ) |