Metamath Proof Explorer

Theorem cnmpt1ip

Description: Continuity of inner product; analogue of cnmpt12f which cannot be used directly because .i is not a function. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses cnmpt1ip.j ⊢ J = TopOpen ⁡ W
cnmpt1ip.c ⊢ C = TopOpen ⁡ ℂ fld
cnmpt1ip.h ⊢ , ˙ = ⋅ 𝑖 ⁡ W
cnmpt1ip.r ⊢ φ → W ∈ CPreHil
cnmpt1ip.k ⊢ φ → K ∈ TopOn ⁡ X
cnmpt1ip.a ⊢ φ → x ∈ X ⟼ A ∈ K Cn J
cnmpt1ip.b ⊢ φ → x ∈ X ⟼ B ∈ K Cn J
Assertion cnmpt1ip ⊢ φ → x ∈ X ⟼ A , ˙ B ∈ K Cn C

Proof

Step Hyp Ref Expression
1 cnmpt1ip.j ⊢ J = TopOpen ⁡ W
2 cnmpt1ip.c ⊢ C = TopOpen ⁡ ℂ fld
3 cnmpt1ip.h ⊢ , ˙ = ⋅ 𝑖 ⁡ W
4 cnmpt1ip.r ⊢ φ → W ∈ CPreHil
5 cnmpt1ip.k ⊢ φ → K ∈ TopOn ⁡ X
6 cnmpt1ip.a ⊢ φ → x ∈ X ⟼ A ∈ K Cn J
7 cnmpt1ip.b ⊢ φ → x ∈ X ⟼ B ∈ K Cn J
8 cphngp ⊢ W ∈ CPreHil → W ∈ NrmGrp
9 ngptps ⊢ W ∈ NrmGrp → W ∈ TopSp
10 4 8 9 3syl ⊢ φ → W ∈ TopSp
11 eqid ⊢ Base W = Base W
12 11 1 istps ⊢ W ∈ TopSp ↔ J ∈ TopOn ⁡ Base W
13 10 12 sylib ⊢ φ → J ∈ TopOn ⁡ Base W
14 cnf2 ⊢ K ∈ TopOn ⁡ X ∧ J ∈ TopOn ⁡ Base W ∧ x ∈ X ⟼ A ∈ K Cn J → x ∈ X ⟼ A : X ⟶ Base W
15 5 13 6 14 syl3anc ⊢ φ → x ∈ X ⟼ A : X ⟶ Base W
16 15 fvmptelrn ⊢ φ ∧ x ∈ X → A ∈ Base W
17 cnf2 ⊢ K ∈ TopOn ⁡ X ∧ J ∈ TopOn ⁡ Base W ∧ x ∈ X ⟼ B ∈ K Cn J → x ∈ X ⟼ B : X ⟶ Base W
18 5 13 7 17 syl3anc ⊢ φ → x ∈ X ⟼ B : X ⟶ Base W
19 18 fvmptelrn ⊢ φ ∧ x ∈ X → B ∈ Base W
20 eqid ⊢ ⋅ if ⁡ W = ⋅ if ⁡ W
21 11 3 20 ipfval ⊢ A ∈ Base W ∧ B ∈ Base W → A ⋅ if ⁡ W B = A , ˙ B
22 16 19 21 syl2anc ⊢ φ ∧ x ∈ X → A ⋅ if ⁡ W B = A , ˙ B
23 22 mpteq2dva ⊢ φ → x ∈ X ⟼ A ⋅ if ⁡ W B = x ∈ X ⟼ A , ˙ B
24 20 1 2 ipcn ⊢ W ∈ CPreHil → ⋅ if ⁡ W ∈ J × t J Cn C
25 4 24 syl ⊢ φ → ⋅ if ⁡ W ∈ J × t J Cn C
26 5 6 7 25 cnmpt12f ⊢ φ → x ∈ X ⟼ A ⋅ if ⁡ W B ∈ K Cn C
27 23 26 eqeltrrd ⊢ φ → x ∈ X ⟼ A , ˙ B ∈ K Cn C