Theorem cnmpt2ip

Description: Continuity of inner product; analogue of cnmpt22f 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 ‘ 𝑋 ) )
	cnmpt2ip.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
	cnmpt2ip.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
	cnmpt2ip.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
Assertion	cnmpt2ip	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 , 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) 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		cnmpt2ip.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
7		cnmpt2ip.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
8		cnmpt2ip.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
9		txtopon	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
10	5 6 9	syl2anc	⊢ ( 𝜑 → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
11		cphngp	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
12		ngptps	⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ TopSp )
13	4 11 12	3syl	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
14		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
15	14 1	istps	⊢ ( 𝑊 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
16	13 15	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
17		cnf2	⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
18	10 16 7 17	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
19		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
20	19	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝑊 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
21	18 20	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝑊 ) )
22	21	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝑊 ) )
23	22	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ( Base ‘ 𝑊 ) )
24		cnf2	⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
25	10 16 8 24	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
26		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
27	26	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝑊 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
28	25 27	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝑊 ) )
29	28	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝑊 ) )
30	29	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ( Base ‘ 𝑊 ) )
31		eqid	⊢ ( ·if ‘ 𝑊 ) = ( ·if ‘ 𝑊 )
32	14 3 31	ipfval	⊢ ( ( 𝐴 ∈ ( Base ‘ 𝑊 ) ∧ 𝐵 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) = ( 𝐴 , 𝐵 ) )
33	23 30 32	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) = ( 𝐴 , 𝐵 ) )
34	33	3impa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) = ( 𝐴 , 𝐵 ) )
35	34	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 , 𝐵 ) ) )
36	31 1 2	ipcn	⊢ ( 𝑊 ∈ ℂPreHil → ( ·if ‘ 𝑊 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐶 ) )
37	4 36	syl	⊢ ( 𝜑 → ( ·if ‘ 𝑊 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐶 ) )
38	5 6 7 8 37	cnmpt22f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐶 ) )
39	35 38	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 , 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐶 ) )