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 18675 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝐾) = (0g‘𝐿)) |
| 5 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (0g‘𝐾) = (0g‘𝐿)) |
| 6 | 1, 5 | eqeq12d 2753 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥(+g‘𝐾)𝑦) = (0g‘𝐾) ↔ (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) |
| 7 | 6 | anass1rs 655 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) → ((𝑥(+g‘𝐾)𝑦) = (0g‘𝐾) ↔ (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) |
| 8 | 7 | riotabidva 7407 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐾)𝑦) = (0g‘𝐾)) = (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) |
| 9 | 8 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐾)𝑦) = (0g‘𝐾))) = (𝑦 ∈ 𝐵 ↦ (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿)))) |
| 10 | 2 | riotaeqdv 7389 |
. . . 4
⊢ (𝜑 → (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐾)𝑦) = (0g‘𝐾)) = (℩𝑥 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) = (0g‘𝐾))) |
| 11 | 2, 10 | mpteq12dv 5233 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐾)𝑦) = (0g‘𝐾))) = (𝑦 ∈ (Base‘𝐾) ↦ (℩𝑥 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) = (0g‘𝐾)))) |
| 12 | 3 | riotaeqdv 7389 |
. . . 4
⊢ (𝜑 → (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿)) = (℩𝑥 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) |
| 13 | 3, 12 | mpteq12dv 5233 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (℩𝑥 ∈ 𝐵 (𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) = (𝑦 ∈ (Base‘𝐿) ↦ (℩𝑥 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) = (0g‘𝐿)))) |
| 14 | 9, 11, 13 | 3eqtr3d 2785 |
. 2
⊢ (𝜑 → (𝑦 ∈ (Base‘𝐾) ↦ (℩𝑥 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) = (0g‘𝐾))) = (𝑦 ∈ (Base‘𝐿) ↦ (℩𝑥 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) = (0g‘𝐿)))) |
| 15 | | eqid 2737 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 16 | | eqid 2737 |
. . 3
⊢
(+g‘𝐾) = (+g‘𝐾) |
| 17 | | eqid 2737 |
. . 3
⊢
(0g‘𝐾) = (0g‘𝐾) |
| 18 | | eqid 2737 |
. . 3
⊢
(invg‘𝐾) = (invg‘𝐾) |
| 19 | 15, 16, 17, 18 | grpinvfval 18996 |
. 2
⊢
(invg‘𝐾) = (𝑦 ∈ (Base‘𝐾) ↦ (℩𝑥 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) = (0g‘𝐾))) |
| 20 | | eqid 2737 |
. . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) |
| 21 | | eqid 2737 |
. . 3
⊢
(+g‘𝐿) = (+g‘𝐿) |
| 22 | | eqid 2737 |
. . 3
⊢
(0g‘𝐿) = (0g‘𝐿) |
| 23 | | eqid 2737 |
. . 3
⊢
(invg‘𝐿) = (invg‘𝐿) |
| 24 | 20, 21, 22, 23 | grpinvfval 18996 |
. 2
⊢
(invg‘𝐿) = (𝑦 ∈ (Base‘𝐿) ↦ (℩𝑥 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) = (0g‘𝐿))) |
| 25 | 14, 19, 24 | 3eqtr4g 2802 |
1
⊢ (𝜑 →
(invg‘𝐾) =
(invg‘𝐿)) |