Proof of Theorem grpinvpropd
Step | Hyp | Ref
| Expression |
1 | | grpinvpropd.3 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) |
2 | | grpinvpropd.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
3 | | grpinvpropd.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
4 | 2, 3, 1 | grpidpropd 18158 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝐾) = (0g‘𝐿)) |
5 | 4 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (0g‘𝐾) = (0g‘𝐿)) |
6 | 1, 5 | eqeq12d 2754 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥(+g‘𝐾)𝑦) = (0g‘𝐾) ↔ (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) |
7 | 6 | anass1rs 655 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) → ((𝑥(+g‘𝐾)𝑦) = (0g‘𝐾) ↔ (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) |
8 | 7 | riotabidva 7208 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐾)𝑦) = (0g‘𝐾)) = (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) |
9 | 8 | mpteq2dva 5164 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐾)𝑦) = (0g‘𝐾))) = (𝑦 ∈ 𝐵 ↦ (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿)))) |
10 | 2 | riotaeqdv 7189 |
. . . 4
⊢ (𝜑 → (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐾)𝑦) = (0g‘𝐾)) = (℩𝑥 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) = (0g‘𝐾))) |
11 | 2, 10 | mpteq12dv 5154 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐾)𝑦) = (0g‘𝐾))) = (𝑦 ∈ (Base‘𝐾) ↦ (℩𝑥 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) = (0g‘𝐾)))) |
12 | 3 | riotaeqdv 7189 |
. . . 4
⊢ (𝜑 → (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿)) = (℩𝑥 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) |
13 | 3, 12 | mpteq12dv 5154 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) = (𝑦 ∈ (Base‘𝐿) ↦ (℩𝑥 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) = (0g‘𝐿)))) |
14 | 9, 11, 13 | 3eqtr3d 2786 |
. 2
⊢ (𝜑 → (𝑦 ∈ (Base‘𝐾) ↦ (℩𝑥 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) = (0g‘𝐾))) = (𝑦 ∈ (Base‘𝐿) ↦ (℩𝑥 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) = (0g‘𝐿)))) |
15 | | eqid 2738 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
16 | | eqid 2738 |
. . 3
⊢
(+g‘𝐾) = (+g‘𝐾) |
17 | | eqid 2738 |
. . 3
⊢
(0g‘𝐾) = (0g‘𝐾) |
18 | | eqid 2738 |
. . 3
⊢
(invg‘𝐾) = (invg‘𝐾) |
19 | 15, 16, 17, 18 | grpinvfval 18430 |
. 2
⊢
(invg‘𝐾) = (𝑦 ∈ (Base‘𝐾) ↦ (℩𝑥 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) = (0g‘𝐾))) |
20 | | eqid 2738 |
. . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) |
21 | | eqid 2738 |
. . 3
⊢
(+g‘𝐿) = (+g‘𝐿) |
22 | | eqid 2738 |
. . 3
⊢
(0g‘𝐿) = (0g‘𝐿) |
23 | | eqid 2738 |
. . 3
⊢
(invg‘𝐿) = (invg‘𝐿) |
24 | 20, 21, 22, 23 | grpinvfval 18430 |
. 2
⊢
(invg‘𝐿) = (𝑦 ∈ (Base‘𝐿) ↦ (℩𝑥 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) |
25 | 14, 19, 24 | 3eqtr4g 2804 |
1
⊢ (𝜑 →
(invg‘𝐾) =
(invg‘𝐿)) |