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 ⊒ ( ( πœ‘ ∧ 𝑋 ∈ 𝑉 ) β†’ ( 𝑋 , 𝑋 ) ∈ ℝ )