Step | Hyp | Ref
| Expression |
1 | | tcphval.n |
. . . . . . 7
β’ πΊ = (toβPreHilβπ) |
2 | | tcphcph.v |
. . . . . . 7
β’ π = (Baseβπ) |
3 | | tcphcph.f |
. . . . . . 7
β’ πΉ = (Scalarβπ) |
4 | | tcphcph.1 |
. . . . . . 7
β’ (π β π β PreHil) |
5 | | tcphcph.2 |
. . . . . . 7
β’ (π β πΉ = (βfld
βΎs πΎ)) |
6 | 1, 2, 3, 4, 5 | phclm 24619 |
. . . . . 6
β’ (π β π β βMod) |
7 | | tcphcph.k |
. . . . . . 7
β’ πΎ = (BaseβπΉ) |
8 | 3, 7 | clmsscn 24465 |
. . . . . 6
β’ (π β βMod β πΎ β
β) |
9 | 6, 8 | syl 17 |
. . . . 5
β’ (π β πΎ β β) |
10 | | tcphcphlem2.3 |
. . . . 5
β’ (π β π β πΎ) |
11 | 9, 10 | sseldd 3949 |
. . . 4
β’ (π β π β β) |
12 | 11 | cjmulrcld 15100 |
. . 3
β’ (π β (π Β· (ββπ)) β β) |
13 | 11 | cjmulge0d 15102 |
. . 3
β’ (π β 0 β€ (π Β· (ββπ))) |
14 | | tcphcphlem2.4 |
. . . 4
β’ (π β π β π) |
15 | | tcphcph.h |
. . . . 5
β’ , =
(Β·πβπ) |
16 | 1, 2, 3, 4, 5, 15 | tcphcphlem3 24620 |
. . . 4
β’ ((π β§ π β π) β (π , π) β β) |
17 | 14, 16 | mpdan 686 |
. . 3
β’ (π β (π , π) β β) |
18 | | oveq12 7370 |
. . . . . 6
β’ ((π₯ = π β§ π₯ = π) β (π₯ , π₯) = (π , π)) |
19 | 18 | anidms 568 |
. . . . 5
β’ (π₯ = π β (π₯ , π₯) = (π , π)) |
20 | 19 | breq2d 5121 |
. . . 4
β’ (π₯ = π β (0 β€ (π₯ , π₯) β 0 β€ (π , π))) |
21 | | tcphcph.4 |
. . . . 5
β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) |
22 | 21 | ralrimiva 3140 |
. . . 4
β’ (π β βπ₯ β π 0 β€ (π₯ , π₯)) |
23 | 20, 22, 14 | rspcdva 3584 |
. . 3
β’ (π β 0 β€ (π , π)) |
24 | 12, 13, 17, 23 | sqrtmuld 15318 |
. 2
β’ (π β (ββ((π Β· (ββπ)) Β· (π , π))) = ((ββ(π Β· (ββπ))) Β· (ββ(π , π)))) |
25 | | phllmod 21057 |
. . . . . . 7
β’ (π β PreHil β π β LMod) |
26 | 4, 25 | syl 17 |
. . . . . 6
β’ (π β π β LMod) |
27 | | tcphcph.s |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
28 | 2, 3, 27, 7 | lmodvscl 20383 |
. . . . . 6
β’ ((π β LMod β§ π β πΎ β§ π β π) β (π Β· π) β π) |
29 | 26, 10, 14, 28 | syl3anc 1372 |
. . . . 5
β’ (π β (π Β· π) β π) |
30 | | eqid 2733 |
. . . . . 6
β’
(.rβπΉ) = (.rβπΉ) |
31 | | eqid 2733 |
. . . . . 6
β’
(*πβπΉ) = (*πβπΉ) |
32 | 3, 15, 2, 7, 27, 30, 31 | ipassr 21073 |
. . . . 5
β’ ((π β PreHil β§ ((π Β· π) β π β§ π β π β§ π β πΎ)) β ((π Β· π) , (π Β· π)) = (((π Β· π) , π)(.rβπΉ)((*πβπΉ)βπ))) |
33 | 4, 29, 14, 10, 32 | syl13anc 1373 |
. . . 4
β’ (π β ((π Β· π) , (π Β· π)) = (((π Β· π) , π)(.rβπΉ)((*πβπΉ)βπ))) |
34 | 3 | clmmul 24461 |
. . . . . 6
β’ (π β βMod β
Β· = (.rβπΉ)) |
35 | 6, 34 | syl 17 |
. . . . 5
β’ (π β Β· =
(.rβπΉ)) |
36 | 35 | oveqd 7378 |
. . . . . 6
β’ (π β (π Β· (π , π)) = (π(.rβπΉ)(π , π))) |
37 | 3, 15, 2, 7, 27, 30 | ipass 21072 |
. . . . . . 7
β’ ((π β PreHil β§ (π β πΎ β§ π β π β§ π β π)) β ((π Β· π) , π) = (π(.rβπΉ)(π , π))) |
38 | 4, 10, 14, 14, 37 | syl13anc 1373 |
. . . . . 6
β’ (π β ((π Β· π) , π) = (π(.rβπΉ)(π , π))) |
39 | 36, 38 | eqtr4d 2776 |
. . . . 5
β’ (π β (π Β· (π , π)) = ((π Β· π) , π)) |
40 | 3 | clmcj 24462 |
. . . . . . 7
β’ (π β βMod β
β = (*πβπΉ)) |
41 | 6, 40 | syl 17 |
. . . . . 6
β’ (π β β =
(*πβπΉ)) |
42 | 41 | fveq1d 6848 |
. . . . 5
β’ (π β (ββπ) =
((*πβπΉ)βπ)) |
43 | 35, 39, 42 | oveq123d 7382 |
. . . 4
β’ (π β ((π Β· (π , π)) Β· (ββπ)) = (((π Β· π) , π)(.rβπΉ)((*πβπΉ)βπ))) |
44 | 17 | recnd 11191 |
. . . . 5
β’ (π β (π , π) β β) |
45 | 11 | cjcld 15090 |
. . . . 5
β’ (π β (ββπ) β
β) |
46 | 11, 44, 45 | mul32d 11373 |
. . . 4
β’ (π β ((π Β· (π , π)) Β· (ββπ)) = ((π Β· (ββπ)) Β· (π , π))) |
47 | 33, 43, 46 | 3eqtr2d 2779 |
. . 3
β’ (π β ((π Β· π) , (π Β· π)) = ((π Β· (ββπ)) Β· (π , π))) |
48 | 47 | fveq2d 6850 |
. 2
β’ (π β (ββ((π Β· π) , (π Β· π))) = (ββ((π Β· (ββπ)) Β· (π , π)))) |
49 | | absval 15132 |
. . . 4
β’ (π β β β
(absβπ) =
(ββ(π Β·
(ββπ)))) |
50 | 11, 49 | syl 17 |
. . 3
β’ (π β (absβπ) = (ββ(π Β· (ββπ)))) |
51 | 50 | oveq1d 7376 |
. 2
β’ (π β ((absβπ) Β· (ββ(π , π))) = ((ββ(π Β· (ββπ))) Β· (ββ(π , π)))) |
52 | 24, 48, 51 | 3eqtr4d 2783 |
1
β’ (π β (ββ((π Β· π) , (π Β· π))) = ((absβπ) Β· (ββ(π , π)))) |