occllem

Description: Lemma for occl . (Contributed by NM, 7-Aug-2000) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	occl.1	$⊢ φ \to A \subseteq ℋ$
	occl.2	$⊢ φ \to F \in Cauchy$
	occl.3	$⊢ φ \to F : ℕ ⟶ ⊥ (A)$
	occl.4	$⊢ φ \to B \in A$
Assertion	occllem	$⊢ φ \to \underset{v}{⇝} (F) \cdot_{ih} B = 0$

Proof

Step	Hyp	Ref	Expression
1		occl.1	$⊢ φ \to A \subseteq ℋ$
2		occl.2	$⊢ φ \to F \in Cauchy$
3		occl.3	$⊢ φ \to F : ℕ ⟶ ⊥ (A)$
4		occl.4	$⊢ φ \to B \in A$
5		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
6	5	cnfldhaus	$⊢ TopOpen (ℂ_{fld}) \in Haus$
7	6	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Haus$
8		ax-hcompl	$⊢ F \in Cauchy \to \exists x \in ℋ F \underset{v}{⇝} x$
9		hlimf	$⊢ \underset{v}{⇝} : dom \underset{v}{⇝} ⟶ ℋ$
10		ffn	$⊢ \underset{v}{⇝} : dom \underset{v}{⇝} ⟶ ℋ \to \underset{v}{⇝} Fn dom \underset{v}{⇝}$
11	9 10	ax-mp	$⊢ \underset{v}{⇝} Fn dom \underset{v}{⇝}$
12		fnbr	$⊢ (\underset{v}{⇝} Fn dom \underset{v}{⇝} \land F \underset{v}{⇝} x) \to F \in dom \underset{v}{⇝}$
13	11 12	mpan	$⊢ F \underset{v}{⇝} x \to F \in dom \underset{v}{⇝}$
14	13	rexlimivw	$⊢ \exists x \in ℋ F \underset{v}{⇝} x \to F \in dom \underset{v}{⇝}$
15	2 8 14	3syl	$⊢ φ \to F \in dom \underset{v}{⇝}$
16		ffun	$⊢ \underset{v}{⇝} : dom \underset{v}{⇝} ⟶ ℋ \to Fun \underset{v}{⇝}$
17		funfvbrb	$⊢ Fun \underset{v}{⇝} \to (F \in dom \underset{v}{⇝} \leftrightarrow F \underset{v}{⇝} \underset{v}{⇝} (F))$
18	9 16 17	mp2b	$⊢ F \in dom \underset{v}{⇝} \leftrightarrow F \underset{v}{⇝} \underset{v}{⇝} (F)$
19	15 18	sylib	$⊢ φ \to F \underset{v}{⇝} \underset{v}{⇝} (F)$
20		eqid	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
21		eqid	$⊢ {norm}_{ℎ} \circ -_{ℎ} = {norm}_{ℎ} \circ -_{ℎ}$
22	20 21	hhims	$⊢ {norm}_{ℎ} \circ -_{ℎ} = IndMet (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
23		eqid	$⊢ MetOpen ({norm}_{ℎ} \circ -_{ℎ}) = MetOpen ({norm}_{ℎ} \circ -_{ℎ})$
24	20 22 23	hhlm	$⊢ \underset{v}{⇝} = {\underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) ↾}_{(ℋ^{ℕ})}$
25		resss	$⊢ {\underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) ↾}_{(ℋ^{ℕ})} \subseteq \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
26	24 25	eqsstri	$⊢ \underset{v}{⇝} \subseteq \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
27	26	ssbri	$⊢ F \underset{v}{⇝} \underset{v}{⇝} (F) \to F \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) \underset{v}{⇝} (F)$
28	19 27	syl	$⊢ φ \to F \underset{t}{⇝} (MetOpen ({norm}_{ℎ} \circ -_{ℎ})) \underset{v}{⇝} (F)$
29	21	hilxmet	$⊢ {norm}_{ℎ} \circ -_{ℎ} \in ∞Met (ℋ)$
30	23	mopntopon	$⊢ {norm}_{ℎ} \circ -_{ℎ} \in ∞Met (ℋ) \to MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \in TopOn (ℋ)$
31	29 30	mp1i	$⊢ φ \to MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \in TopOn (ℋ)$
32	31	cnmptid	$⊢ φ \to (x \in ℋ ⟼ x) \in (MetOpen ({norm}_{ℎ} \circ -_{ℎ}) Cn MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
33	1 4	sseldd	$⊢ φ \to B \in ℋ$
34	31 31 33	cnmptc	$⊢ φ \to (x \in ℋ ⟼ B) \in (MetOpen ({norm}_{ℎ} \circ -_{ℎ}) Cn MetOpen ({norm}_{ℎ} \circ -_{ℎ}))$
35	20	hhnv	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ \in NrmCVec$
36	20	hhip	$⊢ \cdot_{ih} = \cdot_{𝑖OLD} (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
37	36 22 23 5	dipcn	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ \in NrmCVec \to \cdot_{ih} \in ((MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \times_{t} MetOpen ({norm}_{ℎ} \circ -_{ℎ})) Cn TopOpen (ℂ_{fld}))$
38	35 37	mp1i	$⊢ φ \to \cdot_{ih} \in ((MetOpen ({norm}_{ℎ} \circ -_{ℎ}) \times_{t} MetOpen ({norm}_{ℎ} \circ -_{ℎ})) Cn TopOpen (ℂ_{fld}))$
39	31 32 34 38	cnmpt12f	$⊢ φ \to (x \in ℋ ⟼ x \cdot_{ih} B) \in (MetOpen ({norm}_{ℎ} \circ -_{ℎ}) Cn TopOpen (ℂ_{fld}))$
40	28 39	lmcn	$⊢ φ \to ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F) \underset{t}{⇝} (TopOpen (ℂ_{fld})) (x \in ℋ ⟼ x \cdot_{ih} B) (\underset{v}{⇝} (F))$
41	3	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to F (k) \in ⊥ (A)$
42		ocel	$⊢ A \subseteq ℋ \to (F (k) \in ⊥ (A) \leftrightarrow (F (k) \in ℋ \land \forall x \in A F (k) \cdot_{ih} x = 0))$
43	1 42	syl	$⊢ φ \to (F (k) \in ⊥ (A) \leftrightarrow (F (k) \in ℋ \land \forall x \in A F (k) \cdot_{ih} x = 0))$
44	43	adantr	$⊢ (φ \land k \in ℕ) \to (F (k) \in ⊥ (A) \leftrightarrow (F (k) \in ℋ \land \forall x \in A F (k) \cdot_{ih} x = 0))$
45	41 44	mpbid	$⊢ (φ \land k \in ℕ) \to (F (k) \in ℋ \land \forall x \in A F (k) \cdot_{ih} x = 0)$
46	45	simpld	$⊢ (φ \land k \in ℕ) \to F (k) \in ℋ$
47		oveq1	$⊢ x = F (k) \to x \cdot_{ih} B = F (k) \cdot_{ih} B$
48		eqid	$⊢ (x \in ℋ ⟼ x \cdot_{ih} B) = (x \in ℋ ⟼ x \cdot_{ih} B)$
49		ovex	$⊢ F (k) \cdot_{ih} B \in V$
50	47 48 49	fvmpt	$⊢ F (k) \in ℋ \to (x \in ℋ ⟼ x \cdot_{ih} B) (F (k)) = F (k) \cdot_{ih} B$
51	46 50	syl	$⊢ (φ \land k \in ℕ) \to (x \in ℋ ⟼ x \cdot_{ih} B) (F (k)) = F (k) \cdot_{ih} B$
52		oveq2	$⊢ x = B \to F (k) \cdot_{ih} x = F (k) \cdot_{ih} B$
53	52	eqeq1d	$⊢ x = B \to (F (k) \cdot_{ih} x = 0 \leftrightarrow F (k) \cdot_{ih} B = 0)$
54	45	simprd	$⊢ (φ \land k \in ℕ) \to \forall x \in A F (k) \cdot_{ih} x = 0$
55	4	adantr	$⊢ (φ \land k \in ℕ) \to B \in A$
56	53 54 55	rspcdva	$⊢ (φ \land k \in ℕ) \to F (k) \cdot_{ih} B = 0$
57	51 56	eqtrd	$⊢ (φ \land k \in ℕ) \to (x \in ℋ ⟼ x \cdot_{ih} B) (F (k)) = 0$
58		ocss	$⊢ A \subseteq ℋ \to ⊥ (A) \subseteq ℋ$
59	1 58	syl	$⊢ φ \to ⊥ (A) \subseteq ℋ$
60	3 59	fssd	$⊢ φ \to F : ℕ ⟶ ℋ$
61		fvco3	$⊢ (F : ℕ ⟶ ℋ \land k \in ℕ) \to ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F) (k) = (x \in ℋ ⟼ x \cdot_{ih} B) (F (k))$
62	60 61	sylan	$⊢ (φ \land k \in ℕ) \to ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F) (k) = (x \in ℋ ⟼ x \cdot_{ih} B) (F (k))$
63		c0ex	$⊢ 0 \in V$
64	63	fvconst2	$⊢ k \in ℕ \to (ℕ \times \{0\}) (k) = 0$
65	64	adantl	$⊢ (φ \land k \in ℕ) \to (ℕ \times \{0\}) (k) = 0$
66	57 62 65	3eqtr4d	$⊢ (φ \land k \in ℕ) \to ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F) (k) = (ℕ \times \{0\}) (k)$
67	66	ralrimiva	$⊢ φ \to \forall k \in ℕ ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F) (k) = (ℕ \times \{0\}) (k)$
68		ovex	$⊢ x \cdot_{ih} B \in V$
69	68 48	fnmpti	$⊢ (x \in ℋ ⟼ x \cdot_{ih} B) Fn ℋ$
70		fnfco	$⊢ ((x \in ℋ ⟼ x \cdot_{ih} B) Fn ℋ \land F : ℕ ⟶ ℋ) \to ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F) Fn ℕ$
71	69 60 70	sylancr	$⊢ φ \to ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F) Fn ℕ$
72	63	fconst	$⊢ (ℕ \times \{0\}) : ℕ ⟶ \{0\}$
73		ffn	$⊢ (ℕ \times \{0\}) : ℕ ⟶ \{0\} \to (ℕ \times \{0\}) Fn ℕ$
74	72 73	ax-mp	$⊢ (ℕ \times \{0\}) Fn ℕ$
75		eqfnfv	$⊢ (((x \in ℋ ⟼ x \cdot_{ih} B) \circ F) Fn ℕ \land (ℕ \times \{0\}) Fn ℕ) \to ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F = ℕ \times \{0\} \leftrightarrow \forall k \in ℕ ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F) (k) = (ℕ \times \{0\}) (k))$
76	71 74 75	sylancl	$⊢ φ \to ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F = ℕ \times \{0\} \leftrightarrow \forall k \in ℕ ((x \in ℋ ⟼ x \cdot_{ih} B) \circ F) (k) = (ℕ \times \{0\}) (k))$
77	67 76	mpbird	$⊢ φ \to (x \in ℋ ⟼ x \cdot_{ih} B) \circ F = ℕ \times \{0\}$
78		fvex	$⊢ \underset{v}{⇝} (F) \in V$
79	78	hlimveci	$⊢ F \underset{v}{⇝} \underset{v}{⇝} (F) \to \underset{v}{⇝} (F) \in ℋ$
80		oveq1	$⊢ x = \underset{v}{⇝} (F) \to x \cdot_{ih} B = \underset{v}{⇝} (F) \cdot_{ih} B$
81		ovex	$⊢ \underset{v}{⇝} (F) \cdot_{ih} B \in V$
82	80 48 81	fvmpt	$⊢ \underset{v}{⇝} (F) \in ℋ \to (x \in ℋ ⟼ x \cdot_{ih} B) (\underset{v}{⇝} (F)) = \underset{v}{⇝} (F) \cdot_{ih} B$
83	19 79 82	3syl	$⊢ φ \to (x \in ℋ ⟼ x \cdot_{ih} B) (\underset{v}{⇝} (F)) = \underset{v}{⇝} (F) \cdot_{ih} B$
84	40 77 83	3brtr3d	$⊢ φ \to (ℕ \times \{0\}) \underset{t}{⇝} (TopOpen (ℂ_{fld})) (\underset{v}{⇝} (F) \cdot_{ih} B)$
85	5	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
86	85	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
87		0cnd	$⊢ φ \to 0 \in ℂ$
88		1zzd	$⊢ φ \to 1 \in ℤ$
89		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
90	89	lmconst	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land 0 \in ℂ \land 1 \in ℤ) \to (ℕ \times \{0\}) \underset{t}{⇝} (TopOpen (ℂ_{fld})) 0$
91	86 87 88 90	syl3anc	$⊢ φ \to (ℕ \times \{0\}) \underset{t}{⇝} (TopOpen (ℂ_{fld})) 0$
92	7 84 91	lmmo	$⊢ φ \to \underset{v}{⇝} (F) \cdot_{ih} B = 0$

Metamath Proof Explorer

Theorem occllem

Proof