Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
2 | | eqid 2177 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
3 | | opprbas.1 |
. . . . . . . . . . 11
⊢ 𝑂 =
(oppr‘𝑅) |
4 | | eqid 2177 |
. . . . . . . . . . 11
⊢
(.r‘𝑂) = (.r‘𝑂) |
5 | 1, 2, 3, 4 | opprmulg 13068 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑂)𝑦) = (𝑦(.r‘𝑅)𝑥)) |
6 | 5 | 3expa 1203 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑂)𝑦) = (𝑦(.r‘𝑅)𝑥)) |
7 | 6 | eqeq1d 2186 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑂)𝑦) = 𝑦 ↔ (𝑦(.r‘𝑅)𝑥) = 𝑦)) |
8 | | simpll 527 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑅 ∈ 𝑉) |
9 | | simpr 110 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑦 ∈ (Base‘𝑅)) |
10 | | simplr 528 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
11 | 1, 2, 3, 4 | opprmulg 13068 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑦(.r‘𝑂)𝑥) = (𝑥(.r‘𝑅)𝑦)) |
12 | 8, 9, 10, 11 | syl3anc 1238 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑦(.r‘𝑂)𝑥) = (𝑥(.r‘𝑅)𝑦)) |
13 | 12 | eqeq1d 2186 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑦(.r‘𝑂)𝑥) = 𝑦 ↔ (𝑥(.r‘𝑅)𝑦) = 𝑦)) |
14 | 7, 13 | anbi12d 473 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → (((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦) ↔ ((𝑦(.r‘𝑅)𝑥) = 𝑦 ∧ (𝑥(.r‘𝑅)𝑦) = 𝑦))) |
15 | 14 | biancomd 271 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → (((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦) ↔ ((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦))) |
16 | 15 | ralbidva 2473 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝑅)) → (∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦) ↔ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦))) |
17 | 16 | riotabidva 5841 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (℩𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦)) = (℩𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦))) |
18 | | df-riota 5825 |
. . . 4
⊢
(℩𝑥
∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦)) = (℩𝑥(𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦))) |
19 | | df-riota 5825 |
. . . 4
⊢
(℩𝑥
∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦)) = (℩𝑥(𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦))) |
20 | 17, 18, 19 | 3eqtr3g 2233 |
. . 3
⊢ (𝑅 ∈ 𝑉 → (℩𝑥(𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦))) = (℩𝑥(𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦)))) |
21 | 3 | opprex 13070 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → 𝑂 ∈ V) |
22 | | eqid 2177 |
. . . . . 6
⊢
(mulGrp‘𝑂) =
(mulGrp‘𝑂) |
23 | 22 | mgpex 12962 |
. . . . 5
⊢ (𝑂 ∈ V →
(mulGrp‘𝑂) ∈
V) |
24 | | eqid 2177 |
. . . . . 6
⊢
(Base‘(mulGrp‘𝑂)) = (Base‘(mulGrp‘𝑂)) |
25 | | eqid 2177 |
. . . . . 6
⊢
(+g‘(mulGrp‘𝑂)) =
(+g‘(mulGrp‘𝑂)) |
26 | | eqid 2177 |
. . . . . 6
⊢
(0g‘(mulGrp‘𝑂)) =
(0g‘(mulGrp‘𝑂)) |
27 | 24, 25, 26 | grpidvalg 12684 |
. . . . 5
⊢
((mulGrp‘𝑂)
∈ V → (0g‘(mulGrp‘𝑂)) = (℩𝑥(𝑥 ∈ (Base‘(mulGrp‘𝑂)) ∧ ∀𝑦 ∈
(Base‘(mulGrp‘𝑂))((𝑥(+g‘(mulGrp‘𝑂))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑂))𝑥) = 𝑦)))) |
28 | 21, 23, 27 | 3syl 17 |
. . . 4
⊢ (𝑅 ∈ 𝑉 →
(0g‘(mulGrp‘𝑂)) = (℩𝑥(𝑥 ∈ (Base‘(mulGrp‘𝑂)) ∧ ∀𝑦 ∈
(Base‘(mulGrp‘𝑂))((𝑥(+g‘(mulGrp‘𝑂))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑂))𝑥) = 𝑦)))) |
29 | 3, 1 | opprbasg 13072 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (Base‘𝑅) = (Base‘𝑂)) |
30 | | eqid 2177 |
. . . . . . . . . 10
⊢
(Base‘𝑂) =
(Base‘𝑂) |
31 | 22, 30 | mgpbasg 12963 |
. . . . . . . . 9
⊢ (𝑂 ∈ V →
(Base‘𝑂) =
(Base‘(mulGrp‘𝑂))) |
32 | 21, 31 | syl 14 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (Base‘𝑂) = (Base‘(mulGrp‘𝑂))) |
33 | 29, 32 | eqtrd 2210 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → (Base‘𝑅) = (Base‘(mulGrp‘𝑂))) |
34 | 33 | eleq2d 2247 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → (𝑥 ∈ (Base‘𝑅) ↔ 𝑥 ∈ (Base‘(mulGrp‘𝑂)))) |
35 | 22, 4 | mgpplusgg 12961 |
. . . . . . . . . . 11
⊢ (𝑂 ∈ V →
(.r‘𝑂) =
(+g‘(mulGrp‘𝑂))) |
36 | 21, 35 | syl 14 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → (.r‘𝑂) =
(+g‘(mulGrp‘𝑂))) |
37 | 36 | oveqd 5886 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝑉 → (𝑥(.r‘𝑂)𝑦) = (𝑥(+g‘(mulGrp‘𝑂))𝑦)) |
38 | 37 | eqeq1d 2186 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → ((𝑥(.r‘𝑂)𝑦) = 𝑦 ↔ (𝑥(+g‘(mulGrp‘𝑂))𝑦) = 𝑦)) |
39 | 36 | oveqd 5886 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝑉 → (𝑦(.r‘𝑂)𝑥) = (𝑦(+g‘(mulGrp‘𝑂))𝑥)) |
40 | 39 | eqeq1d 2186 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → ((𝑦(.r‘𝑂)𝑥) = 𝑦 ↔ (𝑦(+g‘(mulGrp‘𝑂))𝑥) = 𝑦)) |
41 | 38, 40 | anbi12d 473 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → (((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦) ↔ ((𝑥(+g‘(mulGrp‘𝑂))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑂))𝑥) = 𝑦))) |
42 | 33, 41 | raleqbidv 2684 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → (∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦) ↔ ∀𝑦 ∈ (Base‘(mulGrp‘𝑂))((𝑥(+g‘(mulGrp‘𝑂))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑂))𝑥) = 𝑦))) |
43 | 34, 42 | anbi12d 473 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → ((𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘(mulGrp‘𝑂)) ∧ ∀𝑦 ∈
(Base‘(mulGrp‘𝑂))((𝑥(+g‘(mulGrp‘𝑂))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑂))𝑥) = 𝑦)))) |
44 | 43 | iotabidv 5195 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (℩𝑥(𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦))) = (℩𝑥(𝑥 ∈ (Base‘(mulGrp‘𝑂)) ∧ ∀𝑦 ∈
(Base‘(mulGrp‘𝑂))((𝑥(+g‘(mulGrp‘𝑂))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑂))𝑥) = 𝑦)))) |
45 | 28, 44 | eqtr4d 2213 |
. . 3
⊢ (𝑅 ∈ 𝑉 →
(0g‘(mulGrp‘𝑂)) = (℩𝑥(𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑂)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑂)𝑥) = 𝑦)))) |
46 | | eqid 2177 |
. . . . . 6
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
47 | 46 | mgpex 12962 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → (mulGrp‘𝑅) ∈ V) |
48 | | eqid 2177 |
. . . . . 6
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅)) |
49 | | eqid 2177 |
. . . . . 6
⊢
(+g‘(mulGrp‘𝑅)) =
(+g‘(mulGrp‘𝑅)) |
50 | | eqid 2177 |
. . . . . 6
⊢
(0g‘(mulGrp‘𝑅)) =
(0g‘(mulGrp‘𝑅)) |
51 | 48, 49, 50 | grpidvalg 12684 |
. . . . 5
⊢
((mulGrp‘𝑅)
∈ V → (0g‘(mulGrp‘𝑅)) = (℩𝑥(𝑥 ∈ (Base‘(mulGrp‘𝑅)) ∧ ∀𝑦 ∈
(Base‘(mulGrp‘𝑅))((𝑥(+g‘(mulGrp‘𝑅))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑅))𝑥) = 𝑦)))) |
52 | 47, 51 | syl 14 |
. . . 4
⊢ (𝑅 ∈ 𝑉 →
(0g‘(mulGrp‘𝑅)) = (℩𝑥(𝑥 ∈ (Base‘(mulGrp‘𝑅)) ∧ ∀𝑦 ∈
(Base‘(mulGrp‘𝑅))((𝑥(+g‘(mulGrp‘𝑅))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑅))𝑥) = 𝑦)))) |
53 | 46, 1 | mgpbasg 12963 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → (Base‘𝑅) = (Base‘(mulGrp‘𝑅))) |
54 | 53 | eleq2d 2247 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → (𝑥 ∈ (Base‘𝑅) ↔ 𝑥 ∈ (Base‘(mulGrp‘𝑅)))) |
55 | 46, 2 | mgpplusgg 12961 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑉 → (.r‘𝑅) =
(+g‘(mulGrp‘𝑅))) |
56 | 55 | oveqd 5886 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝑉 → (𝑥(.r‘𝑅)𝑦) = (𝑥(+g‘(mulGrp‘𝑅))𝑦)) |
57 | 56 | eqeq1d 2186 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → ((𝑥(.r‘𝑅)𝑦) = 𝑦 ↔ (𝑥(+g‘(mulGrp‘𝑅))𝑦) = 𝑦)) |
58 | 55 | oveqd 5886 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝑉 → (𝑦(.r‘𝑅)𝑥) = (𝑦(+g‘(mulGrp‘𝑅))𝑥)) |
59 | 58 | eqeq1d 2186 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → ((𝑦(.r‘𝑅)𝑥) = 𝑦 ↔ (𝑦(+g‘(mulGrp‘𝑅))𝑥) = 𝑦)) |
60 | 57, 59 | anbi12d 473 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → (((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦) ↔ ((𝑥(+g‘(mulGrp‘𝑅))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑅))𝑥) = 𝑦))) |
61 | 53, 60 | raleqbidv 2684 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → (∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦) ↔ ∀𝑦 ∈ (Base‘(mulGrp‘𝑅))((𝑥(+g‘(mulGrp‘𝑅))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑅))𝑥) = 𝑦))) |
62 | 54, 61 | anbi12d 473 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → ((𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘(mulGrp‘𝑅)) ∧ ∀𝑦 ∈
(Base‘(mulGrp‘𝑅))((𝑥(+g‘(mulGrp‘𝑅))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑅))𝑥) = 𝑦)))) |
63 | 62 | iotabidv 5195 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (℩𝑥(𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦))) = (℩𝑥(𝑥 ∈ (Base‘(mulGrp‘𝑅)) ∧ ∀𝑦 ∈
(Base‘(mulGrp‘𝑅))((𝑥(+g‘(mulGrp‘𝑅))𝑦) = 𝑦 ∧ (𝑦(+g‘(mulGrp‘𝑅))𝑥) = 𝑦)))) |
64 | 52, 63 | eqtr4d 2213 |
. . 3
⊢ (𝑅 ∈ 𝑉 →
(0g‘(mulGrp‘𝑅)) = (℩𝑥(𝑥 ∈ (Base‘𝑅) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)𝑦) = 𝑦 ∧ (𝑦(.r‘𝑅)𝑥) = 𝑦)))) |
65 | 20, 45, 64 | 3eqtr4d 2220 |
. 2
⊢ (𝑅 ∈ 𝑉 →
(0g‘(mulGrp‘𝑂)) =
(0g‘(mulGrp‘𝑅))) |
66 | | eqid 2177 |
. . . 4
⊢
(1r‘𝑂) = (1r‘𝑂) |
67 | 22, 66 | ringidvalg 12970 |
. . 3
⊢ (𝑂 ∈ V →
(1r‘𝑂) =
(0g‘(mulGrp‘𝑂))) |
68 | 21, 67 | syl 14 |
. 2
⊢ (𝑅 ∈ 𝑉 → (1r‘𝑂) =
(0g‘(mulGrp‘𝑂))) |
69 | | oppr1.2 |
. . 3
⊢ 1 =
(1r‘𝑅) |
70 | 46, 69 | ringidvalg 12970 |
. 2
⊢ (𝑅 ∈ 𝑉 → 1 =
(0g‘(mulGrp‘𝑅))) |
71 | 65, 68, 70 | 3eqtr4rd 2221 |
1
⊢ (𝑅 ∈ 𝑉 → 1 =
(1r‘𝑂)) |