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	$⊢ J = TopOpen (W)$
	cnmpt1ip.c	$⊢ C = TopOpen (ℂ_{fld})$
	cnmpt1ip.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	cnmpt1ip.r	$⊢ φ \to W \in CPreHil$
	cnmpt1ip.k	$⊢ φ \to K \in TopOn (X)$
	cnmpt2ip.l	$⊢ φ \to L \in TopOn (Y)$
	cnmpt2ip.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)$
	cnmpt2ip.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)$
Assertion	cnmpt2ip	$⊢ φ \to (x \in X, y \in Y ⟼ A \underset{˙}{,} B) \in ((K \times_{t} L) Cn C)$

Proof

Step	Hyp	Ref	Expression
1		cnmpt1ip.j	$⊢ J = TopOpen (W)$
2		cnmpt1ip.c	$⊢ C = TopOpen (ℂ_{fld})$
3		cnmpt1ip.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
4		cnmpt1ip.r	$⊢ φ \to W \in CPreHil$
5		cnmpt1ip.k	$⊢ φ \to K \in TopOn (X)$
6		cnmpt2ip.l	$⊢ φ \to L \in TopOn (Y)$
7		cnmpt2ip.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)$
8		cnmpt2ip.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)$
9		txtopon	$⊢ (K \in TopOn (X) \land L \in TopOn (Y)) \to K \times_{t} L \in TopOn (X \times Y)$
10	5 6 9	syl2anc	$⊢ φ \to K \times_{t} L \in TopOn (X \times Y)$
11		cphngp	$⊢ W \in CPreHil \to W \in NrmGrp$
12		ngptps	$⊢ W \in NrmGrp \to W \in TopSp$
13	4 11 12	3syl	$⊢ φ \to W \in TopSp$
14		eqid	$⊢ {Base}_{W} = {Base}_{W}$
15	14 1	istps	$⊢ W \in TopSp \leftrightarrow J \in TopOn ({Base}_{W})$
16	13 15	sylib	$⊢ φ \to J \in TopOn ({Base}_{W})$
17		cnf2	$⊢ (K \times_{t} L \in TopOn (X \times Y) \land J \in TopOn ({Base}_{W}) \land (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)) \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{W}$
18	10 16 7 17	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{W}$
19		eqid	$⊢ (x \in X, y \in Y ⟼ A) = (x \in X, y \in Y ⟼ A)$
20	19	fmpo	$⊢ \forall x \in X \forall y \in Y A \in {Base}_{W} \leftrightarrow (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{W}$
21	18 20	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y A \in {Base}_{W}$
22	21	r19.21bi	$⊢ (φ \land x \in X) \to \forall y \in Y A \in {Base}_{W}$
23	22	r19.21bi	$⊢ ((φ \land x \in X) \land y \in Y) \to A \in {Base}_{W}$
24		cnf2	$⊢ (K \times_{t} L \in TopOn (X \times Y) \land J \in TopOn ({Base}_{W}) \land (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)) \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{W}$
25	10 16 8 24	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{W}$
26		eqid	$⊢ (x \in X, y \in Y ⟼ B) = (x \in X, y \in Y ⟼ B)$
27	26	fmpo	$⊢ \forall x \in X \forall y \in Y B \in {Base}_{W} \leftrightarrow (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{W}$
28	25 27	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y B \in {Base}_{W}$
29	28	r19.21bi	$⊢ (φ \land x \in X) \to \forall y \in Y B \in {Base}_{W}$
30	29	r19.21bi	$⊢ ((φ \land x \in X) \land y \in Y) \to B \in {Base}_{W}$
31		eqid	$⊢ \cdot_{if} (W) = \cdot_{if} (W)$
32	14 3 31	ipfval	$⊢ (A \in {Base}_{W} \land B \in {Base}_{W}) \to A \cdot_{if} (W) B = A \underset{˙}{,} B$
33	23 30 32	syl2anc	$⊢ ((φ \land x \in X) \land y \in Y) \to A \cdot_{if} (W) B = A \underset{˙}{,} B$
34	33	3impa	$⊢ (φ \land x \in X \land y \in Y) \to A \cdot_{if} (W) B = A \underset{˙}{,} B$
35	34	mpoeq3dva	$⊢ φ \to (x \in X, y \in Y ⟼ A \cdot_{if} (W) B) = (x \in X, y \in Y ⟼ A \underset{˙}{,} B)$
36	31 1 2	ipcn	$⊢ W \in CPreHil \to \cdot_{if} (W) \in ((J \times_{t} J) Cn C)$
37	4 36	syl	$⊢ φ \to \cdot_{if} (W) \in ((J \times_{t} J) Cn C)$
38	5 6 7 8 37	cnmpt22f	$⊢ φ \to (x \in X, y \in Y ⟼ A \cdot_{if} (W) B) \in ((K \times_{t} L) Cn C)$
39	35 38	eqeltrrd	$⊢ φ \to (x \in X, y \in Y ⟼ A \underset{˙}{,} B) \in ((K \times_{t} L) Cn C)$

Metamath Proof Explorer

Theorem cnmpt2ip

Proof