Proof of Theorem unitlinv
Step | Hyp | Ref
| Expression |
1 | | unitinvcl.1 |
. . . . . . 7
⊢ 𝑈 = (Unit‘𝑅) |
2 | 1 | a1i 9 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑈 = (Unit‘𝑅)) |
3 | | eqidd 2178 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
((mulGrp‘𝑅)
↾s 𝑈) =
((mulGrp‘𝑅)
↾s 𝑈)) |
4 | | ringsrg 13177 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing) |
5 | 2, 3, 4 | unitgrpbasd 13237 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑈 =
(Base‘((mulGrp‘𝑅) ↾s 𝑈))) |
6 | 5 | eleq2d 2247 |
. . . 4
⊢ (𝑅 ∈ Ring → (𝑋 ∈ 𝑈 ↔ 𝑋 ∈ (Base‘((mulGrp‘𝑅) ↾s 𝑈)))) |
7 | 6 | pm5.32i 454 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) ↔ (𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘((mulGrp‘𝑅) ↾s 𝑈)))) |
8 | | eqid 2177 |
. . . . 5
⊢
((mulGrp‘𝑅)
↾s 𝑈) =
((mulGrp‘𝑅)
↾s 𝑈) |
9 | 1, 8 | unitgrp 13238 |
. . . 4
⊢ (𝑅 ∈ Ring →
((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp) |
10 | | eqid 2177 |
. . . . 5
⊢
(Base‘((mulGrp‘𝑅) ↾s 𝑈)) = (Base‘((mulGrp‘𝑅) ↾s 𝑈)) |
11 | | eqid 2177 |
. . . . 5
⊢
(+g‘((mulGrp‘𝑅) ↾s 𝑈)) =
(+g‘((mulGrp‘𝑅) ↾s 𝑈)) |
12 | | eqid 2177 |
. . . . 5
⊢
(0g‘((mulGrp‘𝑅) ↾s 𝑈)) =
(0g‘((mulGrp‘𝑅) ↾s 𝑈)) |
13 | | eqid 2177 |
. . . . 5
⊢
(invg‘((mulGrp‘𝑅) ↾s 𝑈)) =
(invg‘((mulGrp‘𝑅) ↾s 𝑈)) |
14 | 10, 11, 12, 13 | grplinv 12876 |
. . . 4
⊢
((((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp ∧ 𝑋 ∈
(Base‘((mulGrp‘𝑅) ↾s 𝑈))) →
(((invg‘((mulGrp‘𝑅) ↾s 𝑈))‘𝑋)(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑋) =
(0g‘((mulGrp‘𝑅) ↾s 𝑈))) |
15 | 9, 14 | sylan 283 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈
(Base‘((mulGrp‘𝑅) ↾s 𝑈))) →
(((invg‘((mulGrp‘𝑅) ↾s 𝑈))‘𝑋)(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑋) =
(0g‘((mulGrp‘𝑅) ↾s 𝑈))) |
16 | 7, 15 | sylbi 121 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) →
(((invg‘((mulGrp‘𝑅) ↾s 𝑈))‘𝑋)(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑋) =
(0g‘((mulGrp‘𝑅) ↾s 𝑈))) |
17 | | eqid 2177 |
. . . . . 6
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
18 | | unitinvcl.3 |
. . . . . 6
⊢ · =
(.r‘𝑅) |
19 | 17, 18 | mgpplusgg 13087 |
. . . . 5
⊢ (𝑅 ∈ Ring → · =
(+g‘(mulGrp‘𝑅))) |
20 | | basfn 12514 |
. . . . . . 7
⊢ Base Fn
V |
21 | | elex 2748 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ V) |
22 | | funfvex 5532 |
. . . . . . . 8
⊢ ((Fun
Base ∧ 𝑅 ∈ dom
Base) → (Base‘𝑅)
∈ V) |
23 | 22 | funfni 5316 |
. . . . . . 7
⊢ ((Base Fn
V ∧ 𝑅 ∈ V) →
(Base‘𝑅) ∈
V) |
24 | 20, 21, 23 | sylancr 414 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) ∈
V) |
25 | | eqidd 2178 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) =
(Base‘𝑅)) |
26 | 25, 2, 4 | unitssd 13231 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑈 ⊆ (Base‘𝑅)) |
27 | 24, 26 | ssexd 4143 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑈 ∈ V) |
28 | 17 | mgpex 13088 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
V) |
29 | 3, 19, 27, 28 | ressplusgd 12581 |
. . . 4
⊢ (𝑅 ∈ Ring → · =
(+g‘((mulGrp‘𝑅) ↾s 𝑈))) |
30 | | unitinvcl.2 |
. . . . . . 7
⊢ 𝐼 = (invr‘𝑅) |
31 | 30 | a1i 9 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝐼 = (invr‘𝑅)) |
32 | | id 19 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Ring) |
33 | 2, 3, 31, 32 | invrfvald 13244 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝐼 =
(invg‘((mulGrp‘𝑅) ↾s 𝑈))) |
34 | 33 | fveq1d 5517 |
. . . 4
⊢ (𝑅 ∈ Ring → (𝐼‘𝑋) =
((invg‘((mulGrp‘𝑅) ↾s 𝑈))‘𝑋)) |
35 | | eqidd 2178 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑋 = 𝑋) |
36 | 29, 34, 35 | oveq123d 5895 |
. . 3
⊢ (𝑅 ∈ Ring → ((𝐼‘𝑋) · 𝑋) =
(((invg‘((mulGrp‘𝑅) ↾s 𝑈))‘𝑋)(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑋)) |
37 | 36 | adantr 276 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝐼‘𝑋) · 𝑋) =
(((invg‘((mulGrp‘𝑅) ↾s 𝑈))‘𝑋)(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑋)) |
38 | | unitinvcl.4 |
. . . 4
⊢ 1 =
(1r‘𝑅) |
39 | 1, 8, 38 | unitgrpid 13240 |
. . 3
⊢ (𝑅 ∈ Ring → 1 =
(0g‘((mulGrp‘𝑅) ↾s 𝑈))) |
40 | 39 | adantr 276 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → 1 =
(0g‘((mulGrp‘𝑅) ↾s 𝑈))) |
41 | 16, 37, 40 | 3eqtr4d 2220 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝐼‘𝑋) · 𝑋) = 1 ) |