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	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	cnmpt1ip.c	⊢ 𝐶 = ( TopOpen ‘ ℂfld )
	cnmpt1ip.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	cnmpt1ip.r	⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
	cnmpt1ip.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt1ip.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) )
	cnmpt1ip.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) )
Assertion	cnmpt1ip	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 , 𝐵 ) ) ∈ ( 𝐾 Cn 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt1ip.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
2		cnmpt1ip.c	⊢ 𝐶 = ( TopOpen ‘ ℂfld )
3		cnmpt1ip.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
4		cnmpt1ip.r	⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
5		cnmpt1ip.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
6		cnmpt1ip.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) )
7		cnmpt1ip.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) )
8		cphngp	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
9		ngptps	⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ TopSp )
10	4 8 9	3syl	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
11		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12	11 1	istps	⊢ ( 𝑊 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
13	10 12	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
14		cnf2	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ( Base ‘ 𝑊 ) )
15	5 13 6 14	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ( Base ‘ 𝑊 ) )
16	15	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ( Base ‘ 𝑊 ) )
17		cnf2	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝑊 ) )
18	5 13 7 17	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝑊 ) )
19	18	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( Base ‘ 𝑊 ) )
20		eqid	⊢ ( ·if ‘ 𝑊 ) = ( ·if ‘ 𝑊 )
21	11 3 20	ipfval	⊢ ( ( 𝐴 ∈ ( Base ‘ 𝑊 ) ∧ 𝐵 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) = ( 𝐴 , 𝐵 ) )
22	16 19 21	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) = ( 𝐴 , 𝐵 ) )
23	22	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 , 𝐵 ) ) )
24	20 1 2	ipcn	⊢ ( 𝑊 ∈ ℂPreHil → ( ·if ‘ 𝑊 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐶 ) )
25	4 24	syl	⊢ ( 𝜑 → ( ·if ‘ 𝑊 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐶 ) )
26	5 6 7 25	cnmpt12f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) ) ∈ ( 𝐾 Cn 𝐶 ) )
27	23 26	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 , 𝐵 ) ) ∈ ( 𝐾 Cn 𝐶 ) )