tcphcphlem3

Description: Lemma for tcphcph : real closure of an inner product of a vector with itself. (Contributed by Mario Carneiro, 10-Oct-2015)

	Ref	Expression
Hypotheses	tcphval.n	$⊢ G = toCPreHil (W)$
	tcphcph.v	$⊢ V = {Base}_{W}$
	tcphcph.f	$⊢ F = Scalar (W)$
	tcphcph.1	$⊢ φ \to W \in PreHil$
	tcphcph.2	$⊢ φ \to F = ℂ_{fld} ↾_{𝑠} K$
	tcphcph.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
Assertion	tcphcphlem3	$⊢ (φ \land X \in V) \to X \underset{˙}{,} X \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$⊢ G = toCPreHil (W)$
2		tcphcph.v	$⊢ V = {Base}_{W}$
3		tcphcph.f	$⊢ F = Scalar (W)$
4		tcphcph.1	$⊢ φ \to W \in PreHil$
5		tcphcph.2	$⊢ φ \to F = ℂ_{fld} ↾_{𝑠} K$
6		tcphcph.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
7	1 2 3 4 5	phclm	$⊢ φ \to W \in CMod$
8	7	adantr	$⊢ (φ \land X \in V) \to W \in CMod$
9		eqid	$⊢ {Base}_{F} = {Base}_{F}$
10	3 9	clmsscn	$⊢ W \in CMod \to {Base}_{F} \subseteq ℂ$
11	8 10	syl	$⊢ (φ \land X \in V) \to {Base}_{F} \subseteq ℂ$
12	3 6 2 9	ipcl	$⊢ (W \in PreHil \land X \in V \land X \in V) \to X \underset{˙}{,} X \in {Base}_{F}$
13	12	3anidm23	$⊢ (W \in PreHil \land X \in V) \to X \underset{˙}{,} X \in {Base}_{F}$
14	4 13	sylan	$⊢ (φ \land X \in V) \to X \underset{˙}{,} X \in {Base}_{F}$
15	11 14	sseldd	$⊢ (φ \land X \in V) \to X \underset{˙}{,} X \in ℂ$
16	3	clmcj	$⊢ W \in CMod \to * = *_{F}$
17	8 16	syl	$⊢ (φ \land X \in V) \to * = *_{F}$
18	17	fveq1d	$⊢ (φ \land X \in V) \to \overline{X \underset{˙}{,} X} = {(X \underset{˙}{,} X)}^{*_{F}}$
19	4	adantr	$⊢ (φ \land X \in V) \to W \in PreHil$
20		simpr	$⊢ (φ \land X \in V) \to X \in V$
21		eqid	$⊢ _{F} = _{F}$
22	3 6 2 21	ipcj	$⊢ (W \in PreHil \land X \in V \land X \in V) \to {(X \underset{˙}{,} X)}^{*_{F}} = X \underset{˙}{,} X$
23	19 20 20 22	syl3anc	$⊢ (φ \land X \in V) \to {(X \underset{˙}{,} X)}^{*_{F}} = X \underset{˙}{,} X$
24	18 23	eqtrd	$⊢ (φ \land X \in V) \to \overline{X \underset{˙}{,} X} = X \underset{˙}{,} X$
25	15 24	cjrebd	$⊢ (φ \land X \in V) \to X \underset{˙}{,} X \in ℝ$

Metamath Proof Explorer

Theorem tcphcphlem3

Proof