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 ‘ 𝑋 ) · ( √ ‘ ( 𝑌 , 𝑌 ) ) ) )