Metamath Proof Explorer

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 𝐢 ) )