Step | Hyp | Ref
| Expression |
1 | | ablpropd.1 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
2 | | ablpropd.2 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
3 | | ablpropd.3 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) |
4 | 1, 2, 3 | mndpropd 17139 |
. . 3
⊢ (𝜑 → (𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd)) |
5 | 3 | oveqrspc2v 6572 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢(+g‘𝐾)𝑣) = (𝑢(+g‘𝐿)𝑣)) |
6 | 3 | oveqrspc2v 6572 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → (𝑣(+g‘𝐾)𝑢) = (𝑣(+g‘𝐿)𝑢)) |
7 | 6 | ancom2s 840 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑣(+g‘𝐾)𝑢) = (𝑣(+g‘𝐿)𝑢)) |
8 | 5, 7 | eqeq12d 2625 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ((𝑢(+g‘𝐾)𝑣) = (𝑣(+g‘𝐾)𝑢) ↔ (𝑢(+g‘𝐿)𝑣) = (𝑣(+g‘𝐿)𝑢))) |
9 | 8 | 2ralbidva 2971 |
. . . 4
⊢ (𝜑 → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢(+g‘𝐾)𝑣) = (𝑣(+g‘𝐾)𝑢) ↔ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢(+g‘𝐿)𝑣) = (𝑣(+g‘𝐿)𝑢))) |
10 | 1 | raleqdv 3121 |
. . . . 5
⊢ (𝜑 → (∀𝑣 ∈ 𝐵 (𝑢(+g‘𝐾)𝑣) = (𝑣(+g‘𝐾)𝑢) ↔ ∀𝑣 ∈ (Base‘𝐾)(𝑢(+g‘𝐾)𝑣) = (𝑣(+g‘𝐾)𝑢))) |
11 | 1, 10 | raleqbidv 3129 |
. . . 4
⊢ (𝜑 → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢(+g‘𝐾)𝑣) = (𝑣(+g‘𝐾)𝑢) ↔ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)(𝑢(+g‘𝐾)𝑣) = (𝑣(+g‘𝐾)𝑢))) |
12 | 2 | raleqdv 3121 |
. . . . 5
⊢ (𝜑 → (∀𝑣 ∈ 𝐵 (𝑢(+g‘𝐿)𝑣) = (𝑣(+g‘𝐿)𝑢) ↔ ∀𝑣 ∈ (Base‘𝐿)(𝑢(+g‘𝐿)𝑣) = (𝑣(+g‘𝐿)𝑢))) |
13 | 2, 12 | raleqbidv 3129 |
. . . 4
⊢ (𝜑 → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢(+g‘𝐿)𝑣) = (𝑣(+g‘𝐿)𝑢) ↔ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)(𝑢(+g‘𝐿)𝑣) = (𝑣(+g‘𝐿)𝑢))) |
14 | 9, 11, 13 | 3bitr3d 297 |
. . 3
⊢ (𝜑 → (∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)(𝑢(+g‘𝐾)𝑣) = (𝑣(+g‘𝐾)𝑢) ↔ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)(𝑢(+g‘𝐿)𝑣) = (𝑣(+g‘𝐿)𝑢))) |
15 | 4, 14 | anbi12d 743 |
. 2
⊢ (𝜑 → ((𝐾 ∈ Mnd ∧ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)(𝑢(+g‘𝐾)𝑣) = (𝑣(+g‘𝐾)𝑢)) ↔ (𝐿 ∈ Mnd ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)(𝑢(+g‘𝐿)𝑣) = (𝑣(+g‘𝐿)𝑢)))) |
16 | | eqid 2610 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
17 | | eqid 2610 |
. . 3
⊢
(+g‘𝐾) = (+g‘𝐾) |
18 | 16, 17 | iscmn 18023 |
. 2
⊢ (𝐾 ∈ CMnd ↔ (𝐾 ∈ Mnd ∧ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)(𝑢(+g‘𝐾)𝑣) = (𝑣(+g‘𝐾)𝑢))) |
19 | | eqid 2610 |
. . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) |
20 | | eqid 2610 |
. . 3
⊢
(+g‘𝐿) = (+g‘𝐿) |
21 | 19, 20 | iscmn 18023 |
. 2
⊢ (𝐿 ∈ CMnd ↔ (𝐿 ∈ Mnd ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)(𝑢(+g‘𝐿)𝑣) = (𝑣(+g‘𝐿)𝑢))) |
22 | 15, 18, 21 | 3bitr4g 302 |
1
⊢ (𝜑 → (𝐾 ∈ CMnd ↔ 𝐿 ∈ CMnd)) |