Metamath Proof Explorer

Theorem tcphcphlem2

Description: Lemma for tcphcph : homogeneity. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses tcphval.n ⊒ 𝐺 = ( toβ„‚PreHil β€˜ π‘Š )
tcphcph.v ⊒ 𝑉 = ( Base β€˜ π‘Š )
tcphcph.f ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
tcphcph.1 ⊒ ( πœ‘ β†’ π‘Š ∈ PreHil )
tcphcph.2 ⊒ ( πœ‘ β†’ 𝐹 = ( β„‚fld β†Ύs 𝐾 ) )
tcphcph.h ⊒ , = ( ·𝑖 β€˜ π‘Š )
tcphcph.3 ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ 𝐾 ∧ π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯ ) ) β†’ ( √ β€˜ π‘₯ ) ∈ 𝐾 )
tcphcph.4 ⊒ ( ( πœ‘ ∧ π‘₯ ∈ 𝑉 ) β†’ 0 ≀ ( π‘₯ , π‘₯ ) )
tcphcph.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
tcphcph.s ⊒ Β· = ( ·𝑠 β€˜ π‘Š )
tcphcphlem2.3 ⊒ ( πœ‘ β†’ 𝑋 ∈ 𝐾 )
tcphcphlem2.4 ⊒ ( πœ‘ β†’ π‘Œ ∈ 𝑉 )
Assertion tcphcphlem2 ( πœ‘ β†’ ( √ β€˜ ( ( 𝑋 Β· π‘Œ ) , ( 𝑋 Β· π‘Œ ) ) ) = ( ( abs β€˜ 𝑋 ) Β· ( √ β€˜ ( π‘Œ , π‘Œ ) ) ) )

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 tcphcph.3 ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ 𝐾 ∧ π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯ ) ) β†’ ( √ β€˜ π‘₯ ) ∈ 𝐾 )
8 tcphcph.4 ⊒ ( ( πœ‘ ∧ π‘₯ ∈ 𝑉 ) β†’ 0 ≀ ( π‘₯ , π‘₯ ) )
9 tcphcph.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
10 tcphcph.s ⊒ Β· = ( ·𝑠 β€˜ π‘Š )
11 tcphcphlem2.3 ⊒ ( πœ‘ β†’ 𝑋 ∈ 𝐾 )
12 tcphcphlem2.4 ⊒ ( πœ‘ β†’ π‘Œ ∈ 𝑉 )
13 1 2 3 4 5 phclm ⊒ ( πœ‘ β†’ π‘Š ∈ β„‚Mod )
14 3 9 clmsscn ⊒ ( π‘Š ∈ β„‚Mod β†’ 𝐾 βŠ† β„‚ )
15 13 14 syl ⊒ ( πœ‘ β†’ 𝐾 βŠ† β„‚ )
16 15 11 sseldd ⊒ ( πœ‘ β†’ 𝑋 ∈ β„‚ )
17 16 cjmulrcld ⊒ ( πœ‘ β†’ ( 𝑋 Β· ( βˆ— β€˜ 𝑋 ) ) ∈ ℝ )
18 16 cjmulge0d ⊒ ( πœ‘ β†’ 0 ≀ ( 𝑋 Β· ( βˆ— β€˜ 𝑋 ) ) )
19 1 2 3 4 5 6 tcphcphlem3 ⊒ ( ( πœ‘ ∧ π‘Œ ∈ 𝑉 ) β†’ ( π‘Œ , π‘Œ ) ∈ ℝ )
20 12 19 mpdan ⊒ ( πœ‘ β†’ ( π‘Œ , π‘Œ ) ∈ ℝ )
21 oveq12 ⊒ ( ( π‘₯ = π‘Œ ∧ π‘₯ = π‘Œ ) β†’ ( π‘₯ , π‘₯ ) = ( π‘Œ , π‘Œ ) )
22 21 anidms ⊒ ( π‘₯ = π‘Œ β†’ ( π‘₯ , π‘₯ ) = ( π‘Œ , π‘Œ ) )
23 22 breq2d ⊒ ( π‘₯ = π‘Œ β†’ ( 0 ≀ ( π‘₯ , π‘₯ ) ↔ 0 ≀ ( π‘Œ , π‘Œ ) ) )
24 8 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝑉 0 ≀ ( π‘₯ , π‘₯ ) )
25 23 24 12 rspcdva ⊒ ( πœ‘ β†’ 0 ≀ ( π‘Œ , π‘Œ ) )
26 17 18 20 25 sqrtmuld ⊒ ( πœ‘ β†’ ( √ β€˜ ( ( 𝑋 Β· ( βˆ— β€˜ 𝑋 ) ) Β· ( π‘Œ , π‘Œ ) ) ) = ( ( √ β€˜ ( 𝑋 Β· ( βˆ— β€˜ 𝑋 ) ) ) Β· ( √ β€˜ ( π‘Œ , π‘Œ ) ) ) )
27 phllmod ⊒ ( π‘Š ∈ PreHil β†’ π‘Š ∈ LMod )
28 4 27 syl ⊒ ( πœ‘ β†’ π‘Š ∈ LMod )
29 2 3 10 9 lmodvscl ⊒ ( ( π‘Š ∈ LMod ∧ 𝑋 ∈ 𝐾 ∧ π‘Œ ∈ 𝑉 ) β†’ ( 𝑋 Β· π‘Œ ) ∈ 𝑉 )
30 28 11 12 29 syl3anc ⊒ ( πœ‘ β†’ ( 𝑋 Β· π‘Œ ) ∈ 𝑉 )
31 eqid ⊒ ( .r β€˜ 𝐹 ) = ( .r β€˜ 𝐹 )
32 eqid ⊒ ( *π‘Ÿ β€˜ 𝐹 ) = ( *π‘Ÿ β€˜ 𝐹 )
33 3 6 2 9 10 31 32 ipassr ⊒ ( ( π‘Š ∈ PreHil ∧ ( ( 𝑋 Β· π‘Œ ) ∈ 𝑉 ∧ π‘Œ ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) ) β†’ ( ( 𝑋 Β· π‘Œ ) , ( 𝑋 Β· π‘Œ ) ) = ( ( ( 𝑋 Β· π‘Œ ) , π‘Œ ) ( .r β€˜ 𝐹 ) ( ( *π‘Ÿ β€˜ 𝐹 ) β€˜ 𝑋 ) ) )
34 4 30 12 11 33 syl13anc ⊒ ( πœ‘ β†’ ( ( 𝑋 Β· π‘Œ ) , ( 𝑋 Β· π‘Œ ) ) = ( ( ( 𝑋 Β· π‘Œ ) , π‘Œ ) ( .r β€˜ 𝐹 ) ( ( *π‘Ÿ β€˜ 𝐹 ) β€˜ 𝑋 ) ) )
35 3 clmmul ⊒ ( π‘Š ∈ β„‚Mod β†’ Β· = ( .r β€˜ 𝐹 ) )
36 13 35 syl ⊒ ( πœ‘ β†’ Β· = ( .r β€˜ 𝐹 ) )
37 36 oveqd ⊒ ( πœ‘ β†’ ( 𝑋 Β· ( π‘Œ , π‘Œ ) ) = ( 𝑋 ( .r β€˜ 𝐹 ) ( π‘Œ , π‘Œ ) ) )
38 3 6 2 9 10 31 ipass ⊒ ( ( π‘Š ∈ PreHil ∧ ( 𝑋 ∈ 𝐾 ∧ π‘Œ ∈ 𝑉 ∧ π‘Œ ∈ 𝑉 ) ) β†’ ( ( 𝑋 Β· π‘Œ ) , π‘Œ ) = ( 𝑋 ( .r β€˜ 𝐹 ) ( π‘Œ , π‘Œ ) ) )
39 4 11 12 12 38 syl13anc ⊒ ( πœ‘ β†’ ( ( 𝑋 Β· π‘Œ ) , π‘Œ ) = ( 𝑋 ( .r β€˜ 𝐹 ) ( π‘Œ , π‘Œ ) ) )
40 37 39 eqtr4d ⊒ ( πœ‘ β†’ ( 𝑋 Β· ( π‘Œ , π‘Œ ) ) = ( ( 𝑋 Β· π‘Œ ) , π‘Œ ) )
41 3 clmcj ⊒ ( π‘Š ∈ β„‚Mod β†’ βˆ— = ( *π‘Ÿ β€˜ 𝐹 ) )
42 13 41 syl ⊒ ( πœ‘ β†’ βˆ— = ( *π‘Ÿ β€˜ 𝐹 ) )
43 42 fveq1d ⊒ ( πœ‘ β†’ ( βˆ— β€˜ 𝑋 ) = ( ( *π‘Ÿ β€˜ 𝐹 ) β€˜ 𝑋 ) )
44 36 40 43 oveq123d ⊒ ( πœ‘ β†’ ( ( 𝑋 Β· ( π‘Œ , π‘Œ ) ) Β· ( βˆ— β€˜ 𝑋 ) ) = ( ( ( 𝑋 Β· π‘Œ ) , π‘Œ ) ( .r β€˜ 𝐹 ) ( ( *π‘Ÿ β€˜ 𝐹 ) β€˜ 𝑋 ) ) )
45 20 recnd ⊒ ( πœ‘ β†’ ( π‘Œ , π‘Œ ) ∈ β„‚ )
46 16 cjcld ⊒ ( πœ‘ β†’ ( βˆ— β€˜ 𝑋 ) ∈ β„‚ )
47 16 45 46 mul32d ⊒ ( πœ‘ β†’ ( ( 𝑋 Β· ( π‘Œ , π‘Œ ) ) Β· ( βˆ— β€˜ 𝑋 ) ) = ( ( 𝑋 Β· ( βˆ— β€˜ 𝑋 ) ) Β· ( π‘Œ , π‘Œ ) ) )
48 34 44 47 3eqtr2d ⊒ ( πœ‘ β†’ ( ( 𝑋 Β· π‘Œ ) , ( 𝑋 Β· π‘Œ ) ) = ( ( 𝑋 Β· ( βˆ— β€˜ 𝑋 ) ) Β· ( π‘Œ , π‘Œ ) ) )
49 48 fveq2d ⊒ ( πœ‘ β†’ ( √ β€˜ ( ( 𝑋 Β· π‘Œ ) , ( 𝑋 Β· π‘Œ ) ) ) = ( √ β€˜ ( ( 𝑋 Β· ( βˆ— β€˜ 𝑋 ) ) Β· ( π‘Œ , π‘Œ ) ) ) )
50 absval ⊒ ( 𝑋 ∈ β„‚ β†’ ( abs β€˜ 𝑋 ) = ( √ β€˜ ( 𝑋 Β· ( βˆ— β€˜ 𝑋 ) ) ) )
51 16 50 syl ⊒ ( πœ‘ β†’ ( abs β€˜ 𝑋 ) = ( √ β€˜ ( 𝑋 Β· ( βˆ— β€˜ 𝑋 ) ) ) )
52 51 oveq1d ⊒ ( πœ‘ β†’ ( ( abs β€˜ 𝑋 ) Β· ( √ β€˜ ( π‘Œ , π‘Œ ) ) ) = ( ( √ β€˜ ( 𝑋 Β· ( βˆ— β€˜ 𝑋 ) ) ) Β· ( √ β€˜ ( π‘Œ , π‘Œ ) ) ) )
53 26 49 52 3eqtr4d ⊒ ( πœ‘ β†’ ( √ β€˜ ( ( 𝑋 Β· π‘Œ ) , ( 𝑋 Β· π‘Œ ) ) ) = ( ( abs β€˜ 𝑋 ) Β· ( √ β€˜ ( π‘Œ , π‘Œ ) ) ) )