This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 , 𝑋 ) ∈ ℝ )