Step |
Hyp |
Ref |
Expression |
1 |
|
ringinvdv.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
ringinvdv.u |
⊢ 𝑈 = ( Unit ‘ 𝑅 ) |
3 |
|
ringinvdv.d |
⊢ / = ( /r ‘ 𝑅 ) |
4 |
|
ringinvdv.o |
⊢ 1 = ( 1r ‘ 𝑅 ) |
5 |
|
ringinvdv.i |
⊢ 𝐼 = ( invr ‘ 𝑅 ) |
6 |
1 4
|
ringidcl |
⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 ) |
7 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
8 |
1 7 2 5 3
|
dvrval |
⊢ ( ( 1 ∈ 𝐵 ∧ 𝑋 ∈ 𝑈 ) → ( 1 / 𝑋 ) = ( 1 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) ) |
9 |
6 8
|
sylan |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 1 / 𝑋 ) = ( 1 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) ) |
10 |
2 5 1
|
ringinvcl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ) |
11 |
1 7 4
|
ringlidm |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ 𝑋 ) ) |
12 |
10 11
|
syldan |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 1 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ 𝑋 ) ) |
13 |
9 12
|
eqtr2d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) = ( 1 / 𝑋 ) ) |