Theorem 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	⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
	tcphcph.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	tcphcph.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	tcphcph.1	⊢ ( 𝜑 → 𝑊 ∈ PreHil )
	tcphcph.2	⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
	tcphcph.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
Assertion	tcphcphlem3	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 , 𝑋 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
2		tcphcph.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		tcphcph.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		tcphcph.1	⊢ ( 𝜑 → 𝑊 ∈ PreHil )
5		tcphcph.2	⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
6		tcphcph.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
7	1 2 3 4 5	phclm	⊢ ( 𝜑 → 𝑊 ∈ ℂMod )
8	7	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → 𝑊 ∈ ℂMod )
9		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
10	3 9	clmsscn	⊢ ( 𝑊 ∈ ℂMod → ( Base ‘ 𝐹 ) ⊆ ℂ )
11	8 10	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( Base ‘ 𝐹 ) ⊆ ℂ )
12	3 6 2 9	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 , 𝑋 ) ∈ ( Base ‘ 𝐹 ) )
13	12	3anidm23	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 , 𝑋 ) ∈ ( Base ‘ 𝐹 ) )
14	4 13	sylan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 , 𝑋 ) ∈ ( Base ‘ 𝐹 ) )
15	11 14	sseldd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 , 𝑋 ) ∈ ℂ )
16	3	clmcj	⊢ ( 𝑊 ∈ ℂMod → ∗ = ( *𝑟 ‘ 𝐹 ) )
17	8 16	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ∗ = ( *𝑟 ‘ 𝐹 ) )
18	17	fveq1d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( ∗ ‘ ( 𝑋 , 𝑋 ) ) = ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑋 , 𝑋 ) ) )
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → 𝑊 ∈ PreHil )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
21		eqid	⊢ ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ 𝐹 )
22	3 6 2 21	ipcj	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑋 , 𝑋 ) ) = ( 𝑋 , 𝑋 ) )
23	19 20 20 22	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑋 , 𝑋 ) ) = ( 𝑋 , 𝑋 ) )
24	18 23	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( ∗ ‘ ( 𝑋 , 𝑋 ) ) = ( 𝑋 , 𝑋 ) )
25	15 24	cjrebd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 , 𝑋 ) ∈ ℝ )