Step | Hyp | Ref
| Expression |
1 | | mndpluscn.t |
. . . 4
⊢ ∗
:(𝐶 × 𝐶)⟶𝐶 |
2 | | ffn 5958 |
. . . 4
⊢ ( ∗
:(𝐶 × 𝐶)⟶𝐶 → ∗ Fn (𝐶 × 𝐶)) |
3 | | fnov 6666 |
. . . . 5
⊢ ( ∗ Fn
(𝐶 × 𝐶) ↔ ∗ = (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ (𝑎 ∗ 𝑏))) |
4 | 3 | biimpi 205 |
. . . 4
⊢ ( ∗ Fn
(𝐶 × 𝐶) → ∗ = (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ (𝑎 ∗ 𝑏))) |
5 | 1, 2, 4 | mp2b 10 |
. . 3
⊢ ∗ =
(𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ (𝑎 ∗ 𝑏)) |
6 | | mndpluscn.f |
. . . . . . . . 9
⊢ 𝐹 ∈ (𝐽Homeo𝐾) |
7 | | mndpluscn.j |
. . . . . . . . . . 11
⊢ 𝐽 ∈ (TopOn‘𝐵) |
8 | 7 | toponunii 20547 |
. . . . . . . . . 10
⊢ 𝐵 = ∪
𝐽 |
9 | | mndpluscn.k |
. . . . . . . . . . 11
⊢ 𝐾 ∈ (TopOn‘𝐶) |
10 | 9 | toponunii 20547 |
. . . . . . . . . 10
⊢ 𝐶 = ∪
𝐾 |
11 | 8, 10 | hmeof1o 21377 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝐵–1-1-onto→𝐶) |
12 | 6, 11 | ax-mp 5 |
. . . . . . . 8
⊢ 𝐹:𝐵–1-1-onto→𝐶 |
13 | | f1ocnvdm 6440 |
. . . . . . . 8
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝑎 ∈ 𝐶) → (◡𝐹‘𝑎) ∈ 𝐵) |
14 | 12, 13 | mpan 702 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐶 → (◡𝐹‘𝑎) ∈ 𝐵) |
15 | | f1ocnvdm 6440 |
. . . . . . . 8
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝑏 ∈ 𝐶) → (◡𝐹‘𝑏) ∈ 𝐵) |
16 | 12, 15 | mpan 702 |
. . . . . . 7
⊢ (𝑏 ∈ 𝐶 → (◡𝐹‘𝑏) ∈ 𝐵) |
17 | 14, 16 | anim12i 588 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) → ((◡𝐹‘𝑎) ∈ 𝐵 ∧ (◡𝐹‘𝑏) ∈ 𝐵)) |
18 | | mndpluscn.h |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦))) |
19 | 18 | rgen2a 2960 |
. . . . . 6
⊢
∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦)) |
20 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝐹‘𝑎) → (𝑥 + 𝑦) = ((◡𝐹‘𝑎) + 𝑦)) |
21 | 20 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = (◡𝐹‘𝑎) → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘((◡𝐹‘𝑎) + 𝑦))) |
22 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝐹‘𝑎) → (𝐹‘𝑥) = (𝐹‘(◡𝐹‘𝑎))) |
23 | 22 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑥 = (◡𝐹‘𝑎) → ((𝐹‘𝑥) ∗ (𝐹‘𝑦)) = ((𝐹‘(◡𝐹‘𝑎)) ∗ (𝐹‘𝑦))) |
24 | 21, 23 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = (◡𝐹‘𝑎) → ((𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦)) ↔ (𝐹‘((◡𝐹‘𝑎) + 𝑦)) = ((𝐹‘(◡𝐹‘𝑎)) ∗ (𝐹‘𝑦)))) |
25 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑦 = (◡𝐹‘𝑏) → ((◡𝐹‘𝑎) + 𝑦) = ((◡𝐹‘𝑎) + (◡𝐹‘𝑏))) |
26 | 25 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑦 = (◡𝐹‘𝑏) → (𝐹‘((◡𝐹‘𝑎) + 𝑦)) = (𝐹‘((◡𝐹‘𝑎) + (◡𝐹‘𝑏)))) |
27 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = (◡𝐹‘𝑏) → (𝐹‘𝑦) = (𝐹‘(◡𝐹‘𝑏))) |
28 | 27 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑦 = (◡𝐹‘𝑏) → ((𝐹‘(◡𝐹‘𝑎)) ∗ (𝐹‘𝑦)) = ((𝐹‘(◡𝐹‘𝑎)) ∗ (𝐹‘(◡𝐹‘𝑏)))) |
29 | 26, 28 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑦 = (◡𝐹‘𝑏) → ((𝐹‘((◡𝐹‘𝑎) + 𝑦)) = ((𝐹‘(◡𝐹‘𝑎)) ∗ (𝐹‘𝑦)) ↔ (𝐹‘((◡𝐹‘𝑎) + (◡𝐹‘𝑏))) = ((𝐹‘(◡𝐹‘𝑎)) ∗ (𝐹‘(◡𝐹‘𝑏))))) |
30 | 24, 29 | rspc2va 3294 |
. . . . . 6
⊢ ((((◡𝐹‘𝑎) ∈ 𝐵 ∧ (◡𝐹‘𝑏) ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦))) → (𝐹‘((◡𝐹‘𝑎) + (◡𝐹‘𝑏))) = ((𝐹‘(◡𝐹‘𝑎)) ∗ (𝐹‘(◡𝐹‘𝑏)))) |
31 | 17, 19, 30 | sylancl 693 |
. . . . 5
⊢ ((𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) → (𝐹‘((◡𝐹‘𝑎) + (◡𝐹‘𝑏))) = ((𝐹‘(◡𝐹‘𝑎)) ∗ (𝐹‘(◡𝐹‘𝑏)))) |
32 | | f1ocnvfv2 6433 |
. . . . . . 7
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝑎 ∈ 𝐶) → (𝐹‘(◡𝐹‘𝑎)) = 𝑎) |
33 | 12, 32 | mpan 702 |
. . . . . 6
⊢ (𝑎 ∈ 𝐶 → (𝐹‘(◡𝐹‘𝑎)) = 𝑎) |
34 | | f1ocnvfv2 6433 |
. . . . . . 7
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝑏 ∈ 𝐶) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏) |
35 | 12, 34 | mpan 702 |
. . . . . 6
⊢ (𝑏 ∈ 𝐶 → (𝐹‘(◡𝐹‘𝑏)) = 𝑏) |
36 | 33, 35 | oveqan12d 6568 |
. . . . 5
⊢ ((𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) → ((𝐹‘(◡𝐹‘𝑎)) ∗ (𝐹‘(◡𝐹‘𝑏))) = (𝑎 ∗ 𝑏)) |
37 | 31, 36 | eqtr2d 2645 |
. . . 4
⊢ ((𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) → (𝑎 ∗ 𝑏) = (𝐹‘((◡𝐹‘𝑎) + (◡𝐹‘𝑏)))) |
38 | 37 | mpt2eq3ia 6618 |
. . 3
⊢ (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ (𝑎 ∗ 𝑏)) = (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ (𝐹‘((◡𝐹‘𝑎) + (◡𝐹‘𝑏)))) |
39 | 5, 38 | eqtri 2632 |
. 2
⊢ ∗ =
(𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ (𝐹‘((◡𝐹‘𝑎) + (◡𝐹‘𝑏)))) |
40 | 9 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐾 ∈
(TopOn‘𝐶)) |
41 | 40, 40 | cnmpt1st 21281 |
. . . . . 6
⊢ (⊤
→ (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ 𝑎) ∈ ((𝐾 ×t 𝐾) Cn 𝐾)) |
42 | | hmeocnvcn 21374 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) |
43 | 6, 42 | mp1i 13 |
. . . . . 6
⊢ (⊤
→ ◡𝐹 ∈ (𝐾 Cn 𝐽)) |
44 | 40, 40, 41, 43 | cnmpt21f 21285 |
. . . . 5
⊢ (⊤
→ (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ (◡𝐹‘𝑎)) ∈ ((𝐾 ×t 𝐾) Cn 𝐽)) |
45 | 40, 40 | cnmpt2nd 21282 |
. . . . . 6
⊢ (⊤
→ (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ 𝑏) ∈ ((𝐾 ×t 𝐾) Cn 𝐾)) |
46 | 40, 40, 45, 43 | cnmpt21f 21285 |
. . . . 5
⊢ (⊤
→ (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ (◡𝐹‘𝑏)) ∈ ((𝐾 ×t 𝐾) Cn 𝐽)) |
47 | | mndpluscn.o |
. . . . . 6
⊢ + ∈
((𝐽 ×t
𝐽) Cn 𝐽) |
48 | 47 | a1i 11 |
. . . . 5
⊢ (⊤
→ +
∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
49 | 40, 40, 44, 46, 48 | cnmpt22f 21288 |
. . . 4
⊢ (⊤
→ (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ ((◡𝐹‘𝑎) + (◡𝐹‘𝑏))) ∈ ((𝐾 ×t 𝐾) Cn 𝐽)) |
50 | | hmeocn 21373 |
. . . . 5
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
51 | 6, 50 | mp1i 13 |
. . . 4
⊢ (⊤
→ 𝐹 ∈ (𝐽 Cn 𝐾)) |
52 | 40, 40, 49, 51 | cnmpt21f 21285 |
. . 3
⊢ (⊤
→ (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ (𝐹‘((◡𝐹‘𝑎) + (◡𝐹‘𝑏)))) ∈ ((𝐾 ×t 𝐾) Cn 𝐾)) |
53 | 52 | trud 1484 |
. 2
⊢ (𝑎 ∈ 𝐶, 𝑏 ∈ 𝐶 ↦ (𝐹‘((◡𝐹‘𝑎) + (◡𝐹‘𝑏)))) ∈ ((𝐾 ×t 𝐾) Cn 𝐾) |
54 | 39, 53 | eqeltri 2684 |
1
⊢ ∗ ∈
((𝐾 ×t
𝐾) Cn 𝐾) |