iscph

Description: A subcomplex pre-Hilbert space is exactly a pre-Hilbert space over a subfield of the field of complex numbers closed under square roots of nonnegative reals equipped with a norm. (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Hypotheses	iscph.v	$⊢ V = {Base}_{W}$
	iscph.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	iscph.n	$⊢ N = norm (W)$
	iscph.f	$⊢ F = Scalar (W)$
	iscph.k	$⊢ K = {Base}_{F}$
Assertion	iscph	$⊢ W \in CPreHil \leftrightarrow ((W \in PreHil \land W \in NrmMod \land F = ℂ_{fld} ↾_{𝑠} K) \land \sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))$

Proof

Step	Hyp	Ref	Expression
1		iscph.v	$⊢ V = {Base}_{W}$
2		iscph.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		iscph.n	$⊢ N = norm (W)$
4		iscph.f	$⊢ F = Scalar (W)$
5		iscph.k	$⊢ K = {Base}_{F}$
6		elin	$⊢ W \in (PreHil \cap NrmMod) \leftrightarrow (W \in PreHil \land W \in NrmMod)$
7	6	anbi1i	$⊢ (W \in (PreHil \cap NrmMod) \land F = ℂ_{fld} ↾_{𝑠} K) \leftrightarrow ((W \in PreHil \land W \in NrmMod) \land F = ℂ_{fld} ↾_{𝑠} K)$
8		df-3an	$⊢ (W \in PreHil \land W \in NrmMod \land F = ℂ_{fld} ↾_{𝑠} K) \leftrightarrow ((W \in PreHil \land W \in NrmMod) \land F = ℂ_{fld} ↾_{𝑠} K)$
9	7 8	bitr4i	$⊢ (W \in (PreHil \cap NrmMod) \land F = ℂ_{fld} ↾_{𝑠} K) \leftrightarrow (W \in PreHil \land W \in NrmMod \land F = ℂ_{fld} ↾_{𝑠} K)$
10	9	anbi1i	$⊢ ((W \in (PreHil \cap NrmMod) \land F = ℂ_{fld} ↾_{𝑠} K) \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))) \leftrightarrow ((W \in PreHil \land W \in NrmMod \land F = ℂ_{fld} ↾_{𝑠} K) \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})))$
11		fvexd	$⊢ w = W \to Scalar (w) \in V$
12		fvexd	$⊢ (w = W \land f = Scalar (w)) \to {Base}_{f} \in V$
13		simplr	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to f = Scalar (w)$
14		simpll	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to w = W$
15	14	fveq2d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to Scalar (w) = Scalar (W)$
16	15 4	eqtr4di	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to Scalar (w) = F$
17	13 16	eqtrd	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to f = F$
18		simpr	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to k = {Base}_{f}$
19	17	fveq2d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to {Base}_{f} = {Base}_{F}$
20	19 5	eqtr4di	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to {Base}_{f} = K$
21	18 20	eqtrd	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to k = K$
22	21	oveq2d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to ℂ_{fld} ↾_{𝑠} k = ℂ_{fld} ↾_{𝑠} K$
23	17 22	eqeq12d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to (f = ℂ_{fld} ↾_{𝑠} k \leftrightarrow F = ℂ_{fld} ↾_{𝑠} K)$
24	21	ineq1d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to k \cap [0, +∞) = K \cap [0, +∞)$
25	24	imaeq2d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to \sqrt [k \cap [0, +∞)] = \sqrt [K \cap [0, +∞)]$
26	25 21	sseq12d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to (\sqrt [k \cap [0, +∞)] \subseteq k \leftrightarrow \sqrt [K \cap [0, +∞)] \subseteq K)$
27	14	fveq2d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to norm (w) = norm (W)$
28	27 3	eqtr4di	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to norm (w) = N$
29	14	fveq2d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to {Base}_{w} = {Base}_{W}$
30	29 1	eqtr4di	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to {Base}_{w} = V$
31	14	fveq2d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to \cdot_{𝑖} (w) = \cdot_{𝑖} (W)$
32	31 2	eqtr4di	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to \cdot_{𝑖} (w) = \underset{˙}{,}$
33	32	oveqd	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to x \cdot_{𝑖} (w) x = x \underset{˙}{,} x$
34	33	fveq2d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to \sqrt{x \cdot_{𝑖} (w) x} = \sqrt{x \underset{˙}{,} x}$
35	30 34	mpteq12dv	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to (x \in {Base}_{w} ⟼ \sqrt{x \cdot_{𝑖} (w) x}) = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})$
36	28 35	eqeq12d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to (norm (w) = (x \in {Base}_{w} ⟼ \sqrt{x \cdot_{𝑖} (w) x}) \leftrightarrow N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))$
37	23 26 36	3anbi123d	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to ((f = ℂ_{fld} ↾_{𝑠} k \land \sqrt [k \cap [0, +∞)] \subseteq k \land norm (w) = (x \in {Base}_{w} ⟼ \sqrt{x \cdot_{𝑖} (w) x})) \leftrightarrow (F = ℂ_{fld} ↾_{𝑠} K \land \sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})))$
38		3anass	$⊢ (F = ℂ_{fld} ↾_{𝑠} K \land \sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})) \leftrightarrow (F = ℂ_{fld} ↾_{𝑠} K \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})))$
39	37 38	bitrdi	$⊢ ((w = W \land f = Scalar (w)) \land k = {Base}_{f}) \to ((f = ℂ_{fld} ↾_{𝑠} k \land \sqrt [k \cap [0, +∞)] \subseteq k \land norm (w) = (x \in {Base}_{w} ⟼ \sqrt{x \cdot_{𝑖} (w) x})) \leftrightarrow (F = ℂ_{fld} ↾_{𝑠} K \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))))$
40	12 39	sbcied	$⊢ (w = W \land f = Scalar (w)) \to (\underset{˙}{[} {Base}_{f} / k \underset{˙}{]} (f = ℂ_{fld} ↾_{𝑠} k \land \sqrt [k \cap [0, +∞)] \subseteq k \land norm (w) = (x \in {Base}_{w} ⟼ \sqrt{x \cdot_{𝑖} (w) x})) \leftrightarrow (F = ℂ_{fld} ↾_{𝑠} K \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))))$
41	11 40	sbcied	$⊢ w = W \to (\underset{˙}{[} Scalar (w) / f \underset{˙}{]} \underset{˙}{[} {Base}_{f} / k \underset{˙}{]} (f = ℂ_{fld} ↾_{𝑠} k \land \sqrt [k \cap [0, +∞)] \subseteq k \land norm (w) = (x \in {Base}_{w} ⟼ \sqrt{x \cdot_{𝑖} (w) x})) \leftrightarrow (F = ℂ_{fld} ↾_{𝑠} K \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))))$
42		df-cph	$⊢ CPreHil = \{w \in (PreHil \cap NrmMod) \| \underset{˙}{[} Scalar (w) / f \underset{˙}{]} \underset{˙}{[} {Base}_{f} / k \underset{˙}{]} (f = ℂ_{fld} ↾_{𝑠} k \land \sqrt [k \cap [0, +∞)] \subseteq k \land norm (w) = (x \in {Base}_{w} ⟼ \sqrt{x \cdot_{𝑖} (w) x}))\}$
43	41 42	elrab2	$⊢ W \in CPreHil \leftrightarrow (W \in (PreHil \cap NrmMod) \land (F = ℂ_{fld} ↾_{𝑠} K \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))))$
44		anass	$⊢ ((W \in (PreHil \cap NrmMod) \land F = ℂ_{fld} ↾_{𝑠} K) \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))) \leftrightarrow (W \in (PreHil \cap NrmMod) \land (F = ℂ_{fld} ↾_{𝑠} K \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))))$
45	43 44	bitr4i	$⊢ W \in CPreHil \leftrightarrow ((W \in (PreHil \cap NrmMod) \land F = ℂ_{fld} ↾_{𝑠} K) \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})))$
46		3anass	$⊢ ((W \in PreHil \land W \in NrmMod \land F = ℂ_{fld} ↾_{𝑠} K) \land \sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})) \leftrightarrow ((W \in PreHil \land W \in NrmMod \land F = ℂ_{fld} ↾_{𝑠} K) \land (\sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x})))$
47	10 45 46	3bitr4i	$⊢ W \in CPreHil \leftrightarrow ((W \in PreHil \land W \in NrmMod \land F = ℂ_{fld} ↾_{𝑠} K) \land \sqrt [K \cap [0, +∞)] \subseteq K \land N = (x \in V ⟼ \sqrt{x \underset{˙}{,} x}))$

Metamath Proof Explorer

Theorem iscph

Proof