Step | Hyp | Ref
| Expression |
1 | | tcphcph.1 |
. . . 4
β’ (π β π β PreHil) |
2 | | tcphval.n |
. . . . 5
β’ πΊ = (toβPreHilβπ) |
3 | 2 | tcphphl 24614 |
. . . 4
β’ (π β PreHil β πΊ β PreHil) |
4 | 1, 3 | sylib 217 |
. . 3
β’ (π β πΊ β PreHil) |
5 | | tcphcph.v |
. . . . . . 7
β’ π = (Baseβπ) |
6 | | tcphcph.h |
. . . . . . 7
β’ , =
(Β·πβπ) |
7 | 2, 5, 6 | tcphval 24605 |
. . . . . 6
β’ πΊ = (π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯)))) |
8 | | eqid 2733 |
. . . . . 6
β’
(-gβπ) = (-gβπ) |
9 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
10 | | phllmod 21057 |
. . . . . . . 8
β’ (π β PreHil β π β LMod) |
11 | 1, 10 | syl 17 |
. . . . . . 7
β’ (π β π β LMod) |
12 | | lmodgrp 20372 |
. . . . . . 7
β’ (π β LMod β π β Grp) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ (π β π β Grp) |
14 | | tcphcph.f |
. . . . . . . . 9
β’ πΉ = (Scalarβπ) |
15 | | tcphcph.2 |
. . . . . . . . 9
β’ (π β πΉ = (βfld
βΎs πΎ)) |
16 | 2, 5, 14, 1, 15, 6 | tcphcphlem3 24620 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (π₯ , π₯) β β) |
17 | | tcphcph.4 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) |
18 | 16, 17 | resqrtcld 15311 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (ββ(π₯ , π₯)) β β) |
19 | 18 | fmpttd 7067 |
. . . . . 6
β’ (π β (π₯ β π β¦ (ββ(π₯ , π₯))):πβΆβ) |
20 | | oveq12 7370 |
. . . . . . . . . . . 12
β’ ((π₯ = π¦ β§ π₯ = π¦) β (π₯ , π₯) = (π¦ , π¦)) |
21 | 20 | anidms 568 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π₯ , π₯) = (π¦ , π¦)) |
22 | 21 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (ββ(π₯ , π₯)) = (ββ(π¦ , π¦))) |
23 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β π β¦ (ββ(π₯ , π₯))) = (π₯ β π β¦ (ββ(π₯ , π₯))) |
24 | | fvex 6859 |
. . . . . . . . . 10
β’
(ββ(π₯
, π₯)) β V |
25 | 22, 23, 24 | fvmpt3i 6957 |
. . . . . . . . 9
β’ (π¦ β π β ((π₯ β π β¦ (ββ(π₯ , π₯)))βπ¦) = (ββ(π¦ , π¦))) |
26 | 25 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β ((π₯ β π β¦ (ββ(π₯ , π₯)))βπ¦) = (ββ(π¦ , π¦))) |
27 | 26 | eqeq1d 2735 |
. . . . . . 7
β’ ((π β§ π¦ β π) β (((π₯ β π β¦ (ββ(π₯ , π₯)))βπ¦) = 0 β (ββ(π¦ , π¦)) = 0)) |
28 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(BaseβπΉ) =
(BaseβπΉ) |
29 | | phllvec 21056 |
. . . . . . . . . . . . . . . . 17
β’ (π β PreHil β π β LVec) |
30 | 1, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β LVec) |
31 | 14 | lvecdrng 20610 |
. . . . . . . . . . . . . . . 16
β’ (π β LVec β πΉ β
DivRing) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ β DivRing) |
33 | 28, 15, 32 | cphsubrglem 24564 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ = (βfld
βΎs (BaseβπΉ)) β§ (BaseβπΉ) = (πΎ β© β) β§ (BaseβπΉ) β
(SubRingββfld))) |
34 | 33 | simp2d 1144 |
. . . . . . . . . . . . 13
β’ (π β (BaseβπΉ) = (πΎ β© β)) |
35 | | inss2 4193 |
. . . . . . . . . . . . 13
β’ (πΎ β© β) β
β |
36 | 34, 35 | eqsstrdi 4002 |
. . . . . . . . . . . 12
β’ (π β (BaseβπΉ) β
β) |
37 | 36 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β (BaseβπΉ) β β) |
38 | 14, 6, 5, 28 | ipcl 21060 |
. . . . . . . . . . . . 13
β’ ((π β PreHil β§ π¦ β π β§ π¦ β π) β (π¦ , π¦) β (BaseβπΉ)) |
39 | 38 | 3anidm23 1422 |
. . . . . . . . . . . 12
β’ ((π β PreHil β§ π¦ β π) β (π¦ , π¦) β (BaseβπΉ)) |
40 | 1, 39 | sylan 581 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β (π¦ , π¦) β (BaseβπΉ)) |
41 | 37, 40 | sseldd 3949 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π) β (π¦ , π¦) β β) |
42 | 41 | sqrtcld 15331 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β (ββ(π¦ , π¦)) β β) |
43 | | sqeq0 14034 |
. . . . . . . . 9
β’
((ββ(π¦
, π¦)) β β β
(((ββ(π¦ , π¦))β2) = 0 β
(ββ(π¦ , π¦)) = 0)) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (((ββ(π¦ , π¦))β2) = 0 β (ββ(π¦ , π¦)) = 0)) |
45 | 41 | sqsqrtd 15333 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β ((ββ(π¦ , π¦))β2) = (π¦ , π¦)) |
46 | 2, 5, 14, 1, 15 | phclm 24619 |
. . . . . . . . . . 11
β’ (π β π β βMod) |
47 | 14 | clm0 24458 |
. . . . . . . . . . 11
β’ (π β βMod β 0 =
(0gβπΉ)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . 10
β’ (π β 0 =
(0gβπΉ)) |
49 | 48 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β 0 = (0gβπΉ)) |
50 | 45, 49 | eqeq12d 2749 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (((ββ(π¦ , π¦))β2) = 0 β (π¦ , π¦) = (0gβπΉ))) |
51 | 44, 50 | bitr3d 281 |
. . . . . . 7
β’ ((π β§ π¦ β π) β ((ββ(π¦ , π¦)) = 0 β (π¦ , π¦) = (0gβπΉ))) |
52 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπΉ) = (0gβπΉ) |
53 | 14, 6, 5, 52, 9 | ipeq0 21065 |
. . . . . . . 8
β’ ((π β PreHil β§ π¦ β π) β ((π¦ , π¦) = (0gβπΉ) β π¦ = (0gβπ))) |
54 | 1, 53 | sylan 581 |
. . . . . . 7
β’ ((π β§ π¦ β π) β ((π¦ , π¦) = (0gβπΉ) β π¦ = (0gβπ))) |
55 | 27, 51, 54 | 3bitrd 305 |
. . . . . 6
β’ ((π β§ π¦ β π) β (((π₯ β π β¦ (ββ(π₯ , π₯)))βπ¦) = 0 β π¦ = (0gβπ))) |
56 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β π β PreHil) |
57 | 33 | simp1d 1143 |
. . . . . . . . 9
β’ (π β πΉ = (βfld
βΎs (BaseβπΉ))) |
58 | 57 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β πΉ = (βfld
βΎs (BaseβπΉ))) |
59 | | 3anass 1096 |
. . . . . . . . . . 11
β’ ((π₯ β (BaseβπΉ) β§ π₯ β β β§ 0 β€ π₯) β (π₯ β (BaseβπΉ) β§ (π₯ β β β§ 0 β€ π₯))) |
60 | | tcphcph.3 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) |
61 | | simpr2 1196 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β π₯ β β) |
62 | 61 | recnd 11191 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β π₯ β β) |
63 | 62 | sqrtcld 15331 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β
β) |
64 | 60, 63 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β ((ββπ₯) β πΎ β§ (ββπ₯) β β)) |
65 | 64 | ex 414 |
. . . . . . . . . . . 12
β’ (π β ((π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯) β ((ββπ₯) β πΎ β§ (ββπ₯) β β))) |
66 | 34 | eleq2d 2820 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π₯ β (BaseβπΉ) β π₯ β (πΎ β© β))) |
67 | | recn 11149 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β π₯ β
β) |
68 | | elin 3930 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (πΎ β© β) β (π₯ β πΎ β§ π₯ β β)) |
69 | 68 | rbaib 540 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β (π₯ β (πΎ β© β) β π₯ β πΎ)) |
70 | 67, 69 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β (π₯ β (πΎ β© β) β π₯ β πΎ)) |
71 | 66, 70 | sylan9bb 511 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β) β (π₯ β (BaseβπΉ) β π₯ β πΎ)) |
72 | 71 | adantrr 716 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β β§ 0 β€ π₯)) β (π₯ β (BaseβπΉ) β π₯ β πΎ)) |
73 | 72 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β ((π₯ β β β§ 0 β€ π₯) β (π₯ β (BaseβπΉ) β π₯ β πΎ))) |
74 | 73 | pm5.32rd 579 |
. . . . . . . . . . . . 13
β’ (π β ((π₯ β (BaseβπΉ) β§ (π₯ β β β§ 0 β€ π₯)) β (π₯ β πΎ β§ (π₯ β β β§ 0 β€ π₯)))) |
75 | | 3anass 1096 |
. . . . . . . . . . . . 13
β’ ((π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯) β (π₯ β πΎ β§ (π₯ β β β§ 0 β€ π₯))) |
76 | 74, 75 | bitr4di 289 |
. . . . . . . . . . . 12
β’ (π β ((π₯ β (BaseβπΉ) β§ (π₯ β β β§ 0 β€ π₯)) β (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯))) |
77 | 34 | eleq2d 2820 |
. . . . . . . . . . . . 13
β’ (π β ((ββπ₯) β (BaseβπΉ) β (ββπ₯) β (πΎ β© β))) |
78 | | elin 3930 |
. . . . . . . . . . . . 13
β’
((ββπ₯)
β (πΎ β© β)
β ((ββπ₯)
β πΎ β§
(ββπ₯) β
β)) |
79 | 77, 78 | bitrdi 287 |
. . . . . . . . . . . 12
β’ (π β ((ββπ₯) β (BaseβπΉ) β ((ββπ₯) β πΎ β§ (ββπ₯) β β))) |
80 | 65, 76, 79 | 3imtr4d 294 |
. . . . . . . . . . 11
β’ (π β ((π₯ β (BaseβπΉ) β§ (π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β (BaseβπΉ))) |
81 | 59, 80 | biimtrid 241 |
. . . . . . . . . 10
β’ (π β ((π₯ β (BaseβπΉ) β§ π₯ β β β§ 0 β€ π₯) β (ββπ₯) β (BaseβπΉ))) |
82 | 81 | imp 408 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (BaseβπΉ) β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β (BaseβπΉ)) |
83 | 82 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ (π¦ β π β§ π§ β π)) β§ (π₯ β (BaseβπΉ) β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β (BaseβπΉ)) |
84 | 17 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ (π¦ β π β§ π§ β π)) β§ π₯ β π) β 0 β€ (π₯ , π₯)) |
85 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β π¦ β π) |
86 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β π§ β π) |
87 | 2, 5, 14, 56, 58, 6, 83, 84, 28, 8, 85, 86 | tcphcphlem1 24622 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ π§ β π)) β (ββ((π¦(-gβπ)π§) , (π¦(-gβπ)π§))) β€ ((ββ(π¦ , π¦)) + (ββ(π§ , π§)))) |
88 | 5, 8 | grpsubcl 18835 |
. . . . . . . . . 10
β’ ((π β Grp β§ π¦ β π β§ π§ β π) β (π¦(-gβπ)π§) β π) |
89 | 88 | 3expb 1121 |
. . . . . . . . 9
β’ ((π β Grp β§ (π¦ β π β§ π§ β π)) β (π¦(-gβπ)π§) β π) |
90 | 13, 89 | sylan 581 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ π§ β π)) β (π¦(-gβπ)π§) β π) |
91 | | oveq12 7370 |
. . . . . . . . . . 11
β’ ((π₯ = (π¦(-gβπ)π§) β§ π₯ = (π¦(-gβπ)π§)) β (π₯ , π₯) = ((π¦(-gβπ)π§) , (π¦(-gβπ)π§))) |
92 | 91 | anidms 568 |
. . . . . . . . . 10
β’ (π₯ = (π¦(-gβπ)π§) β (π₯ , π₯) = ((π¦(-gβπ)π§) , (π¦(-gβπ)π§))) |
93 | 92 | fveq2d 6850 |
. . . . . . . . 9
β’ (π₯ = (π¦(-gβπ)π§) β (ββ(π₯ , π₯)) = (ββ((π¦(-gβπ)π§) , (π¦(-gβπ)π§)))) |
94 | 93, 23, 24 | fvmpt3i 6957 |
. . . . . . . 8
β’ ((π¦(-gβπ)π§) β π β ((π₯ β π β¦ (ββ(π₯ , π₯)))β(π¦(-gβπ)π§)) = (ββ((π¦(-gβπ)π§) , (π¦(-gβπ)π§)))) |
95 | 90, 94 | syl 17 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ π§ β π)) β ((π₯ β π β¦ (ββ(π₯ , π₯)))β(π¦(-gβπ)π§)) = (ββ((π¦(-gβπ)π§) , (π¦(-gβπ)π§)))) |
96 | | oveq12 7370 |
. . . . . . . . . . . 12
β’ ((π₯ = π§ β§ π₯ = π§) β (π₯ , π₯) = (π§ , π§)) |
97 | 96 | anidms 568 |
. . . . . . . . . . 11
β’ (π₯ = π§ β (π₯ , π₯) = (π§ , π§)) |
98 | 97 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π₯ = π§ β (ββ(π₯ , π₯)) = (ββ(π§ , π§))) |
99 | 98, 23, 24 | fvmpt3i 6957 |
. . . . . . . . 9
β’ (π§ β π β ((π₯ β π β¦ (ββ(π₯ , π₯)))βπ§) = (ββ(π§ , π§))) |
100 | 25, 99 | oveqan12d 7380 |
. . . . . . . 8
β’ ((π¦ β π β§ π§ β π) β (((π₯ β π β¦ (ββ(π₯ , π₯)))βπ¦) + ((π₯ β π β¦ (ββ(π₯ , π₯)))βπ§)) = ((ββ(π¦ , π¦)) + (ββ(π§ , π§)))) |
101 | 100 | adantl 483 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ π§ β π)) β (((π₯ β π β¦ (ββ(π₯ , π₯)))βπ¦) + ((π₯ β π β¦ (ββ(π₯ , π₯)))βπ§)) = ((ββ(π¦ , π¦)) + (ββ(π§ , π§)))) |
102 | 87, 95, 101 | 3brtr4d 5141 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ π§ β π)) β ((π₯ β π β¦ (ββ(π₯ , π₯)))β(π¦(-gβπ)π§)) β€ (((π₯ β π β¦ (ββ(π₯ , π₯)))βπ¦) + ((π₯ β π β¦ (ββ(π₯ , π₯)))βπ§))) |
103 | 7, 5, 8, 9, 13, 19, 55, 102 | tngngpd 24040 |
. . . . 5
β’ (π β πΊ β NrmGrp) |
104 | | phllmod 21057 |
. . . . . 6
β’ (πΊ β PreHil β πΊ β LMod) |
105 | 4, 104 | syl 17 |
. . . . 5
β’ (π β πΊ β LMod) |
106 | | cnnrg 24167 |
. . . . . . 7
β’
βfld β NrmRing |
107 | 33 | simp3d 1145 |
. . . . . . 7
β’ (π β (BaseβπΉ) β
(SubRingββfld)) |
108 | | eqid 2733 |
. . . . . . . 8
β’
(βfld βΎs (BaseβπΉ)) = (βfld
βΎs (BaseβπΉ)) |
109 | 108 | subrgnrg 24060 |
. . . . . . 7
β’
((βfld β NrmRing β§ (BaseβπΉ) β
(SubRingββfld)) β (βfld
βΎs (BaseβπΉ)) β NrmRing) |
110 | 106, 107,
109 | sylancr 588 |
. . . . . 6
β’ (π β (βfld
βΎs (BaseβπΉ)) β NrmRing) |
111 | 57, 110 | eqeltrd 2834 |
. . . . 5
β’ (π β πΉ β NrmRing) |
112 | 103, 105,
111 | 3jca 1129 |
. . . 4
β’ (π β (πΊ β NrmGrp β§ πΊ β LMod β§ πΉ β NrmRing)) |
113 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β π β PreHil) |
114 | 57 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β πΉ = (βfld
βΎs (BaseβπΉ))) |
115 | 82 | adantlr 714 |
. . . . . . 7
β’ (((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β§ (π₯ β (BaseβπΉ) β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β (BaseβπΉ)) |
116 | 17 | adantlr 714 |
. . . . . . 7
β’ (((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β§ π₯ β π) β 0 β€ (π₯ , π₯)) |
117 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
118 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β π¦ β (BaseβπΉ)) |
119 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β π§ β π) |
120 | 2, 5, 14, 113, 114, 6, 115, 116, 28, 117, 118, 119 | tcphcphlem2 24623 |
. . . . . 6
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β (ββ((π¦(
Β·π βπ)π§) , (π¦( Β·π
βπ)π§))) = ((absβπ¦) Β· (ββ(π§ , π§)))) |
121 | 5, 14, 117, 28 | lmodvscl 20383 |
. . . . . . . . 9
β’ ((π β LMod β§ π¦ β (BaseβπΉ) β§ π§ β π) β (π¦( Β·π
βπ)π§) β π) |
122 | 121 | 3expb 1121 |
. . . . . . . 8
β’ ((π β LMod β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β (π¦( Β·π
βπ)π§) β π) |
123 | 11, 122 | sylan 581 |
. . . . . . 7
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β (π¦( Β·π
βπ)π§) β π) |
124 | | eqid 2733 |
. . . . . . . 8
β’
(normβπΊ) =
(normβπΊ) |
125 | 2, 124, 5, 6 | tcphnmval 24616 |
. . . . . . 7
β’ ((π β Grp β§ (π¦(
Β·π βπ)π§) β π) β ((normβπΊ)β(π¦( Β·π
βπ)π§)) = (ββ((π¦( Β·π
βπ)π§) , (π¦( Β·π
βπ)π§)))) |
126 | 13, 123, 125 | syl2an2r 684 |
. . . . . 6
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β ((normβπΊ)β(π¦( Β·π
βπ)π§)) = (ββ((π¦( Β·π
βπ)π§) , (π¦( Β·π
βπ)π§)))) |
127 | 114 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β (normβπΉ) = (normβ(βfld
βΎs (BaseβπΉ)))) |
128 | 127 | fveq1d 6848 |
. . . . . . . 8
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β ((normβπΉ)βπ¦) = ((normβ(βfld
βΎs (BaseβπΉ)))βπ¦)) |
129 | | subrgsubg 20270 |
. . . . . . . . . 10
β’
((BaseβπΉ)
β (SubRingββfld) β (BaseβπΉ) β
(SubGrpββfld)) |
130 | 107, 129 | syl 17 |
. . . . . . . . 9
β’ (π β (BaseβπΉ) β
(SubGrpββfld)) |
131 | | cnfldnm 24165 |
. . . . . . . . . 10
β’ abs =
(normββfld) |
132 | | eqid 2733 |
. . . . . . . . . 10
β’
(normβ(βfld βΎs (BaseβπΉ))) =
(normβ(βfld βΎs (BaseβπΉ))) |
133 | 108, 131,
132 | subgnm2 24013 |
. . . . . . . . 9
β’
(((BaseβπΉ)
β (SubGrpββfld) β§ π¦ β (BaseβπΉ)) β
((normβ(βfld βΎs (BaseβπΉ)))βπ¦) = (absβπ¦)) |
134 | 130, 118,
133 | syl2an2r 684 |
. . . . . . . 8
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β
((normβ(βfld βΎs (BaseβπΉ)))βπ¦) = (absβπ¦)) |
135 | 128, 134 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β ((normβπΉ)βπ¦) = (absβπ¦)) |
136 | 2, 124, 5, 6 | tcphnmval 24616 |
. . . . . . . 8
β’ ((π β Grp β§ π§ β π) β ((normβπΊ)βπ§) = (ββ(π§ , π§))) |
137 | 13, 119, 136 | syl2an2r 684 |
. . . . . . 7
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β ((normβπΊ)βπ§) = (ββ(π§ , π§))) |
138 | 135, 137 | oveq12d 7379 |
. . . . . 6
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β (((normβπΉ)βπ¦) Β· ((normβπΊ)βπ§)) = ((absβπ¦) Β· (ββ(π§ , π§)))) |
139 | 120, 126,
138 | 3eqtr4d 2783 |
. . . . 5
β’ ((π β§ (π¦ β (BaseβπΉ) β§ π§ β π)) β ((normβπΊ)β(π¦( Β·π
βπ)π§)) = (((normβπΉ)βπ¦) Β· ((normβπΊ)βπ§))) |
140 | 139 | ralrimivva 3194 |
. . . 4
β’ (π β βπ¦ β (BaseβπΉ)βπ§ β π ((normβπΊ)β(π¦( Β·π
βπ)π§)) = (((normβπΉ)βπ¦) Β· ((normβπΊ)βπ§))) |
141 | 2, 5 | tcphbas 24606 |
. . . . 5
β’ π = (BaseβπΊ) |
142 | 2, 117 | tcphvsca 24611 |
. . . . 5
β’ (
Β·π βπ) = ( Β·π
βπΊ) |
143 | 2, 14 | tcphsca 24610 |
. . . . 5
β’ πΉ = (ScalarβπΊ) |
144 | | eqid 2733 |
. . . . 5
β’
(normβπΉ) =
(normβπΉ) |
145 | 141, 124,
142, 143, 28, 144 | isnlm 24062 |
. . . 4
β’ (πΊ β NrmMod β ((πΊ β NrmGrp β§ πΊ β LMod β§ πΉ β NrmRing) β§
βπ¦ β
(BaseβπΉ)βπ§ β π ((normβπΊ)β(π¦( Β·π
βπ)π§)) = (((normβπΉ)βπ¦) Β· ((normβπΊ)βπ§)))) |
146 | 112, 140,
145 | sylanbrc 584 |
. . 3
β’ (π β πΊ β NrmMod) |
147 | 4, 146, 57 | 3jca 1129 |
. 2
β’ (π β (πΊ β PreHil β§ πΊ β NrmMod β§ πΉ = (βfld
βΎs (BaseβπΉ)))) |
148 | | elin 3930 |
. . . . . 6
β’ (π₯ β ((BaseβπΉ) β© (0[,)+β)) β
(π₯ β (BaseβπΉ) β§ π₯ β (0[,)+β))) |
149 | | elrege0 13380 |
. . . . . . 7
β’ (π₯ β (0[,)+β) β
(π₯ β β β§ 0
β€ π₯)) |
150 | 149 | anbi2i 624 |
. . . . . 6
β’ ((π₯ β (BaseβπΉ) β§ π₯ β (0[,)+β)) β (π₯ β (BaseβπΉ) β§ (π₯ β β β§ 0 β€ π₯))) |
151 | 148, 150 | bitri 275 |
. . . . 5
β’ (π₯ β ((BaseβπΉ) β© (0[,)+β)) β
(π₯ β (BaseβπΉ) β§ (π₯ β β β§ 0 β€ π₯))) |
152 | 151, 80 | biimtrid 241 |
. . . 4
β’ (π β (π₯ β ((BaseβπΉ) β© (0[,)+β)) β
(ββπ₯) β
(BaseβπΉ))) |
153 | 152 | ralrimiv 3139 |
. . 3
β’ (π β βπ₯ β ((BaseβπΉ) β© (0[,)+β))(ββπ₯) β (BaseβπΉ)) |
154 | | sqrtf 15257 |
. . . . 5
β’
β:ββΆβ |
155 | | ffun 6675 |
. . . . 5
β’
(β:ββΆβ β Fun β) |
156 | 154, 155 | ax-mp 5 |
. . . 4
β’ Fun
β |
157 | | inss1 4192 |
. . . . . 6
β’
((BaseβπΉ)
β© (0[,)+β)) β (BaseβπΉ) |
158 | 157, 36 | sstrid 3959 |
. . . . 5
β’ (π β ((BaseβπΉ) β© (0[,)+β)) β
β) |
159 | 154 | fdmi 6684 |
. . . . 5
β’ dom
β = β |
160 | 158, 159 | sseqtrrdi 3999 |
. . . 4
β’ (π β ((BaseβπΉ) β© (0[,)+β)) β
dom β) |
161 | | funimass4 6911 |
. . . 4
β’ ((Fun
β β§ ((BaseβπΉ) β© (0[,)+β)) β dom β)
β ((β β ((BaseβπΉ) β© (0[,)+β))) β
(BaseβπΉ) β
βπ₯ β
((BaseβπΉ) β©
(0[,)+β))(ββπ₯) β (BaseβπΉ))) |
162 | 156, 160,
161 | sylancr 588 |
. . 3
β’ (π β ((β β
((BaseβπΉ) β©
(0[,)+β))) β (BaseβπΉ) β βπ₯ β ((BaseβπΉ) β© (0[,)+β))(ββπ₯) β (BaseβπΉ))) |
163 | 153, 162 | mpbird 257 |
. 2
β’ (π β (β β
((BaseβπΉ) β©
(0[,)+β))) β (BaseβπΉ)) |
164 | 42 | fmpttd 7067 |
. . . 4
β’ (π β (π¦ β π β¦ (ββ(π¦ , π¦))):πβΆβ) |
165 | 2, 5, 6 | tcphval 24605 |
. . . . 5
β’ πΊ = (π toNrmGrp (π¦ β π β¦ (ββ(π¦ , π¦)))) |
166 | | cnex 11140 |
. . . . 5
β’ β
β V |
167 | 165, 5, 166 | tngnm 24038 |
. . . 4
β’ ((π β Grp β§ (π¦ β π β¦ (ββ(π¦ , π¦))):πβΆβ) β (π¦ β π β¦ (ββ(π¦ , π¦))) = (normβπΊ)) |
168 | 13, 164, 167 | syl2anc 585 |
. . 3
β’ (π β (π¦ β π β¦ (ββ(π¦ , π¦))) = (normβπΊ)) |
169 | 168 | eqcomd 2739 |
. 2
β’ (π β (normβπΊ) = (π¦ β π β¦ (ββ(π¦ , π¦)))) |
170 | 2, 6 | tcphip 24612 |
. . 3
β’ , =
(Β·πβπΊ) |
171 | 141, 170,
124, 143, 28 | iscph 24557 |
. 2
β’ (πΊ β βPreHil β
((πΊ β PreHil β§
πΊ β NrmMod β§ πΉ = (βfld
βΎs (BaseβπΉ))) β§ (β β
((BaseβπΉ) β©
(0[,)+β))) β (BaseβπΉ) β§ (normβπΊ) = (π¦ β π β¦ (ββ(π¦ , π¦))))) |
172 | 147, 163,
169, 171 | syl3anbrc 1344 |
1
β’ (π β πΊ β βPreHil) |