Step |
Hyp |
Ref |
Expression |
1 |
|
tgpcn.j |
⊢ 𝐽 = ( TopOpen ‘ 𝐺 ) |
2 |
|
cnmpt1plusg.p |
⊢ + = ( +g ‘ 𝐺 ) |
3 |
|
cnmpt1plusg.g |
⊢ ( 𝜑 → 𝐺 ∈ TopMnd ) |
4 |
|
cnmpt1plusg.k |
⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) |
5 |
|
cnmpt1plusg.a |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) ) |
6 |
|
cnmpt1plusg.b |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) ) |
7 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
8 |
1 7
|
tmdtopon |
⊢ ( 𝐺 ∈ TopMnd → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ) |
9 |
3 8
|
syl |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ) |
10 |
|
cnf2 |
⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) ) |
11 |
4 9 5 10
|
syl3anc |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) ) |
12 |
11
|
fvmptelrn |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) ) |
13 |
|
cnf2 |
⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) ) |
14 |
4 9 6 13
|
syl3anc |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) ) |
15 |
14
|
fvmptelrn |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( Base ‘ 𝐺 ) ) |
16 |
|
eqid |
⊢ ( +𝑓 ‘ 𝐺 ) = ( +𝑓 ‘ 𝐺 ) |
17 |
7 2 16
|
plusfval |
⊢ ( ( 𝐴 ∈ ( Base ‘ 𝐺 ) ∧ 𝐵 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) = ( 𝐴 + 𝐵 ) ) |
18 |
12 15 17
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) = ( 𝐴 + 𝐵 ) ) |
19 |
18
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝐵 ) ) ) |
20 |
1 16
|
tmdcn |
⊢ ( 𝐺 ∈ TopMnd → ( +𝑓 ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |
21 |
3 20
|
syl |
⊢ ( 𝜑 → ( +𝑓 ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |
22 |
4 5 6 21
|
cnmpt12f |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) ) ∈ ( 𝐾 Cn 𝐽 ) ) |
23 |
19 22
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝐵 ) ) ∈ ( 𝐾 Cn 𝐽 ) ) |