Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . . . . 7
β’ (π = (0gβπ) β (π , π) = (π , (0gβπ))) |
2 | 1 | oveq1d 7376 |
. . . . . 6
β’ (π = (0gβπ) β ((π , π) Β· (π , π)) = ((π , (0gβπ)) Β· (π , π))) |
3 | 2 | breq1d 5119 |
. . . . 5
β’ (π = (0gβπ) β (((π , π) Β· (π , π)) β€ ((π , π) Β· (π , π)) β ((π , (0gβπ)) Β· (π , π)) β€ ((π , π) Β· (π , π)))) |
4 | | tcphval.n |
. . . . . . . . . . . . 13
β’ πΊ = (toβPreHilβπ) |
5 | | tcphcph.v |
. . . . . . . . . . . . 13
β’ π = (Baseβπ) |
6 | | tcphcph.f |
. . . . . . . . . . . . 13
β’ πΉ = (Scalarβπ) |
7 | | tcphcph.1 |
. . . . . . . . . . . . 13
β’ (π β π β PreHil) |
8 | | tcphcph.2 |
. . . . . . . . . . . . 13
β’ (π β πΉ = (βfld
βΎs πΎ)) |
9 | 4, 5, 6, 7, 8 | phclm 24619 |
. . . . . . . . . . . 12
β’ (π β π β βMod) |
10 | | tcphcph.k |
. . . . . . . . . . . . 13
β’ πΎ = (BaseβπΉ) |
11 | 6, 10 | clmsscn 24465 |
. . . . . . . . . . . 12
β’ (π β βMod β πΎ β
β) |
12 | 9, 11 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΎ β β) |
13 | | ipcau2.3 |
. . . . . . . . . . . 12
β’ (π β π β π) |
14 | | ipcau2.4 |
. . . . . . . . . . . 12
β’ (π β π β π) |
15 | | tcphcph.h |
. . . . . . . . . . . . 13
β’ , =
(Β·πβπ) |
16 | 6, 15, 5, 10 | ipcl 21060 |
. . . . . . . . . . . 12
β’ ((π β PreHil β§ π β π β§ π β π) β (π , π) β πΎ) |
17 | 7, 13, 14, 16 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (π , π) β πΎ) |
18 | 12, 17 | sseldd 3949 |
. . . . . . . . . 10
β’ (π β (π , π) β β) |
19 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0gβπ)) β (π , π) β β) |
20 | 6, 15, 5, 10 | ipcl 21060 |
. . . . . . . . . . . 12
β’ ((π β PreHil β§ π β π β§ π β π) β (π , π) β πΎ) |
21 | 7, 14, 13, 20 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (π , π) β πΎ) |
22 | 12, 21 | sseldd 3949 |
. . . . . . . . . 10
β’ (π β (π , π) β β) |
23 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0gβπ)) β (π , π) β β) |
24 | 4, 5, 6, 7, 8, 15 | tcphcphlem3 24620 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π , π) β β) |
25 | 14, 24 | mpdan 686 |
. . . . . . . . . . 11
β’ (π β (π , π) β β) |
26 | 25 | recnd 11191 |
. . . . . . . . . 10
β’ (π β (π , π) β β) |
27 | 26 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0gβπ)) β (π , π) β β) |
28 | 6 | clm0 24458 |
. . . . . . . . . . . . . 14
β’ (π β βMod β 0 =
(0gβπΉ)) |
29 | 9, 28 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β 0 =
(0gβπΉ)) |
30 | 29 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π β ((π , π) = 0 β (π , π) = (0gβπΉ))) |
31 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(0gβπΉ) = (0gβπΉ) |
32 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(0gβπ) = (0gβπ) |
33 | 6, 15, 5, 31, 32 | ipeq0 21065 |
. . . . . . . . . . . . 13
β’ ((π β PreHil β§ π β π) β ((π , π) = (0gβπΉ) β π = (0gβπ))) |
34 | 7, 14, 33 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((π , π) = (0gβπΉ) β π = (0gβπ))) |
35 | 30, 34 | bitrd 279 |
. . . . . . . . . . 11
β’ (π β ((π , π) = 0 β π = (0gβπ))) |
36 | 35 | necon3bid 2985 |
. . . . . . . . . 10
β’ (π β ((π , π) β 0 β π β (0gβπ))) |
37 | 36 | biimpar 479 |
. . . . . . . . 9
β’ ((π β§ π β (0gβπ)) β (π , π) β 0) |
38 | 19, 23, 27, 37 | divassd 11974 |
. . . . . . . 8
β’ ((π β§ π β (0gβπ)) β (((π , π) Β· (π , π)) / (π , π)) = ((π , π) Β· ((π , π) / (π , π)))) |
39 | | ipcau2.c |
. . . . . . . . 9
β’ πΆ = ((π , π) / (π , π)) |
40 | 39 | oveq2i 7372 |
. . . . . . . 8
β’ ((π , π) Β· πΆ) = ((π , π) Β· ((π , π) / (π , π))) |
41 | 38, 40 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ π β (0gβπ)) β (((π , π) Β· (π , π)) / (π , π)) = ((π , π) Β· πΆ)) |
42 | | oveq12 7370 |
. . . . . . . . . . . 12
β’ ((π₯ = (π(-gβπ)((ββπΆ)( Β·π
βπ)π)) β§ π₯ = (π(-gβπ)((ββπΆ)( Β·π
βπ)π))) β (π₯ , π₯) = ((π(-gβπ)((ββπΆ)( Β·π
βπ)π)) , (π(-gβπ)((ββπΆ)( Β·π
βπ)π)))) |
43 | 42 | anidms 568 |
. . . . . . . . . . 11
β’ (π₯ = (π(-gβπ)((ββπΆ)( Β·π
βπ)π)) β (π₯ , π₯) = ((π(-gβπ)((ββπΆ)( Β·π
βπ)π)) , (π(-gβπ)((ββπΆ)( Β·π
βπ)π)))) |
44 | 43 | breq2d 5121 |
. . . . . . . . . 10
β’ (π₯ = (π(-gβπ)((ββπΆ)( Β·π
βπ)π)) β (0 β€ (π₯ , π₯) β 0 β€ ((π(-gβπ)((ββπΆ)( Β·π
βπ)π)) , (π(-gβπ)((ββπΆ)( Β·π
βπ)π))))) |
45 | | tcphcph.4 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) |
46 | 45 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β βπ₯ β π 0 β€ (π₯ , π₯)) |
47 | 46 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0gβπ)) β βπ₯ β π 0 β€ (π₯ , π₯)) |
48 | | phllmod 21057 |
. . . . . . . . . . . . 13
β’ (π β PreHil β π β LMod) |
49 | 7, 48 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β LMod) |
50 | 49 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0gβπ)) β π β LMod) |
51 | 13 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0gβπ)) β π β π) |
52 | 39 | fveq2i 6849 |
. . . . . . . . . . . . . . 15
β’
(ββπΆ) =
(ββ((π , π) / (π , π))) |
53 | 23, 27, 37 | cjdivd 15117 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0gβπ)) β (ββ((π , π) / (π , π))) = ((ββ(π , π)) / (ββ(π , π)))) |
54 | 52, 53 | eqtrid 2785 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0gβπ)) β (ββπΆ) = ((ββ(π , π)) / (ββ(π , π)))) |
55 | 8 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(*πβπΉ) =
(*πβ(βfld βΎs πΎ))) |
56 | 10 | fvexi 6860 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ πΎ β V |
57 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βfld βΎs πΎ) = (βfld
βΎs πΎ) |
58 | | cnfldcj 20826 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ β
= (*πββfld) |
59 | 57, 58 | ressstarv 17197 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΎ β V β β =
(*πβ(βfld βΎs πΎ))) |
60 | 56, 59 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β
= (*πβ(βfld βΎs πΎ)) |
61 | 55, 60 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(*πβπΉ) = β) |
62 | 61 | fveq1d 6848 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
((*πβπΉ)β(π , π)) = (ββ(π , π))) |
63 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(*πβπΉ) = (*πβπΉ) |
64 | 6, 15, 5, 63 | ipcj 21061 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β PreHil β§ π β π β§ π β π) β ((*πβπΉ)β(π , π)) = (π , π)) |
65 | 7, 13, 14, 64 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
((*πβπΉ)β(π , π)) = (π , π)) |
66 | 62, 65 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (ββ(π , π)) = (π , π)) |
67 | 66 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0gβπ)) β (ββ(π , π)) = (π , π)) |
68 | 67 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0gβπ)) β
(ββ(ββ(π , π))) = (ββ(π , π))) |
69 | 19 | cjcjd 15093 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0gβπ)) β
(ββ(ββ(π , π))) = (π , π)) |
70 | 68, 69 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0gβπ)) β (ββ(π , π)) = (π , π)) |
71 | 25 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0gβπ)) β (π , π) β β) |
72 | 71 | cjred 15120 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0gβπ)) β (ββ(π , π)) = (π , π)) |
73 | 70, 72 | oveq12d 7379 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0gβπ)) β ((ββ(π , π)) / (ββ(π , π))) = ((π , π) / (π , π))) |
74 | 19, 27, 37 | divrecd 11942 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0gβπ)) β ((π , π) / (π , π)) = ((π , π) Β· (1 / (π , π)))) |
75 | 54, 73, 74 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β (ββπΆ) = ((π , π) Β· (1 / (π , π)))) |
76 | 9 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0gβπ)) β π β βMod) |
77 | 17 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0gβπ)) β (π , π) β πΎ) |
78 | 6, 15, 5, 10 | ipcl 21060 |
. . . . . . . . . . . . . . . . 17
β’ ((π β PreHil β§ π β π β§ π β π) β (π , π) β πΎ) |
79 | 7, 14, 14, 78 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β (π , π) β πΎ) |
80 | 79 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0gβπ)) β (π , π) β πΎ) |
81 | 8 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0gβπ)) β πΉ = (βfld
βΎs πΎ)) |
82 | | phllvec 21056 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β PreHil β π β LVec) |
83 | 7, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β LVec) |
84 | 6 | lvecdrng 20610 |
. . . . . . . . . . . . . . . . . 18
β’ (π β LVec β πΉ β
DivRing) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ β DivRing) |
86 | 85 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0gβπ)) β πΉ β DivRing) |
87 | 10, 81, 86 | cphreccllem 24565 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0gβπ)) β§ (π , π) β πΎ β§ (π , π) β 0) β (1 / (π , π)) β πΎ) |
88 | 80, 37, 87 | mpd3an23 1464 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0gβπ)) β (1 / (π , π)) β πΎ) |
89 | 6, 10 | clmmcl 24471 |
. . . . . . . . . . . . . 14
β’ ((π β βMod β§ (π , π) β πΎ β§ (1 / (π , π)) β πΎ) β ((π , π) Β· (1 / (π , π))) β πΎ) |
90 | 76, 77, 88, 89 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β ((π , π) Β· (1 / (π , π))) β πΎ) |
91 | 75, 90 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β (ββπΆ) β πΎ) |
92 | 14 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β π β π) |
93 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (
Β·π βπ) = ( Β·π
βπ) |
94 | 5, 6, 93, 10 | lmodvscl 20383 |
. . . . . . . . . . . 12
β’ ((π β LMod β§
(ββπΆ) β
πΎ β§ π β π) β ((ββπΆ)( Β·π
βπ)π) β π) |
95 | 50, 91, 92, 94 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π β (0gβπ)) β ((ββπΆ)( Β·π
βπ)π) β π) |
96 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(-gβπ) = (-gβπ) |
97 | 5, 96 | lmodvsubcl 20411 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β π β§ ((ββπΆ)( Β·π
βπ)π) β π) β (π(-gβπ)((ββπΆ)( Β·π
βπ)π)) β π) |
98 | 50, 51, 95, 97 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π β (0gβπ)) β (π(-gβπ)((ββπΆ)( Β·π
βπ)π)) β π) |
99 | 44, 47, 98 | rspcdva 3584 |
. . . . . . . . 9
β’ ((π β§ π β (0gβπ)) β 0 β€ ((π(-gβπ)((ββπΆ)( Β·π
βπ)π)) , (π(-gβπ)((ββπΆ)( Β·π
βπ)π)))) |
100 | | eqid 2733 |
. . . . . . . . . . 11
β’
(-gβπΉ) = (-gβπΉ) |
101 | | eqid 2733 |
. . . . . . . . . . 11
β’
(+gβπΉ) = (+gβπΉ) |
102 | 7 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0gβπ)) β π β PreHil) |
103 | 6, 15, 5, 96, 100, 101, 102, 51, 95, 51, 95 | ip2subdi 21071 |
. . . . . . . . . 10
β’ ((π β§ π β (0gβπ)) β ((π(-gβπ)((ββπΆ)( Β·π
βπ)π)) , (π(-gβπ)((ββπΆ)( Β·π
βπ)π))) = (((π , π)(+gβπΉ)(((ββπΆ)( Β·π
βπ)π) , ((ββπΆ)(
Β·π βπ)π)))(-gβπΉ)((π , ((ββπΆ)(
Β·π βπ)π))(+gβπΉ)(((ββπΆ)( Β·π
βπ)π) , π)))) |
104 | 81 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β (+gβπΉ) =
(+gβ(βfld βΎs πΎ))) |
105 | | cnfldadd 20824 |
. . . . . . . . . . . . . . 15
β’ + =
(+gββfld) |
106 | 57, 105 | ressplusg 17179 |
. . . . . . . . . . . . . 14
β’ (πΎ β V β + =
(+gβ(βfld βΎs πΎ))) |
107 | 56, 106 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ + =
(+gβ(βfld βΎs πΎ)) |
108 | 104, 107 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β (+gβπΉ) = + ) |
109 | | eqidd 2734 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β (π , π) = (π , π)) |
110 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(.rβπΉ) = (.rβπΉ) |
111 | 6, 15, 5, 10, 93, 110 | ipass 21072 |
. . . . . . . . . . . . . 14
β’ ((π β PreHil β§
((ββπΆ) β
πΎ β§ π β π β§ ((ββπΆ)( Β·π
βπ)π) β π)) β (((ββπΆ)(
Β·π βπ)π) , ((ββπΆ)(
Β·π βπ)π)) = ((ββπΆ)(.rβπΉ)(π , ((ββπΆ)(
Β·π βπ)π)))) |
112 | 102, 91, 92, 95, 111 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β (((ββπΆ)(
Β·π βπ)π) , ((ββπΆ)(
Β·π βπ)π)) = ((ββπΆ)(.rβπΉ)(π , ((ββπΆ)(
Β·π βπ)π)))) |
113 | 81 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0gβπ)) β (.rβπΉ) =
(.rβ(βfld βΎs πΎ))) |
114 | | cnfldmul 20825 |
. . . . . . . . . . . . . . . . 17
β’ Β·
= (.rββfld) |
115 | 57, 114 | ressmulr 17196 |
. . . . . . . . . . . . . . . 16
β’ (πΎ β V β Β· =
(.rβ(βfld βΎs πΎ))) |
116 | 56, 115 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ Β·
= (.rβ(βfld βΎs πΎ)) |
117 | 113, 116 | eqtr4di 2791 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0gβπ)) β (.rβπΉ) = Β· ) |
118 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0gβπ)) β (ββπΆ) = (ββπΆ)) |
119 | 23, 27, 37 | divrecd 11942 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0gβπ)) β ((π , π) / (π , π)) = ((π , π) Β· (1 / (π , π)))) |
120 | 39, 119 | eqtrid 2785 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0gβπ)) β πΆ = ((π , π) Β· (1 / (π , π)))) |
121 | 21 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0gβπ)) β (π , π) β πΎ) |
122 | 6, 10 | clmmcl 24471 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β βMod β§ (π , π) β πΎ β§ (1 / (π , π)) β πΎ) β ((π , π) Β· (1 / (π , π))) β πΎ) |
123 | 76, 121, 88, 122 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0gβπ)) β ((π , π) Β· (1 / (π , π))) β πΎ) |
124 | 120, 123 | eqeltrd 2834 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0gβπ)) β πΆ β πΎ) |
125 | 6, 15, 5, 10, 93, 110, 63 | ipassr2 21074 |
. . . . . . . . . . . . . . . 16
β’ ((π β PreHil β§ (π β π β§ π β π β§ πΆ β πΎ)) β ((π , π)(.rβπΉ)πΆ) = (π ,
(((*πβπΉ)βπΆ)( Β·π
βπ)π))) |
126 | 102, 92, 92, 124, 125 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0gβπ)) β ((π , π)(.rβπΉ)πΆ) = (π ,
(((*πβπΉ)βπΆ)( Β·π
βπ)π))) |
127 | 117 | oveqd 7378 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0gβπ)) β ((π , π)(.rβπΉ)πΆ) = ((π , π) Β· πΆ)) |
128 | 39 | oveq2i 7372 |
. . . . . . . . . . . . . . . . 17
β’ ((π , π) Β· πΆ) = ((π , π) Β· ((π , π) / (π , π))) |
129 | 23, 27, 37 | divcan2d 11941 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0gβπ)) β ((π , π) Β· ((π , π) / (π , π))) = (π , π)) |
130 | 128, 129 | eqtrid 2785 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0gβπ)) β ((π , π) Β· πΆ) = (π , π)) |
131 | 127, 130 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0gβπ)) β ((π , π)(.rβπΉ)πΆ) = (π , π)) |
132 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0gβπ)) β (*πβπΉ) = β) |
133 | 132 | fveq1d 6848 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0gβπ)) β
((*πβπΉ)βπΆ) = (ββπΆ)) |
134 | 133 | oveq1d 7376 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0gβπ)) β
(((*πβπΉ)βπΆ)( Β·π
βπ)π) = ((ββπΆ)( Β·π
βπ)π)) |
135 | 134 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0gβπ)) β (π ,
(((*πβπΉ)βπΆ)( Β·π
βπ)π)) = (π , ((ββπΆ)(
Β·π βπ)π))) |
136 | 126, 131,
135 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0gβπ)) β (π , ((ββπΆ)(
Β·π βπ)π)) = (π , π)) |
137 | 117, 118,
136 | oveq123d 7382 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β ((ββπΆ)(.rβπΉ)(π , ((ββπΆ)(
Β·π βπ)π))) = ((ββπΆ) Β· (π , π))) |
138 | 112, 137 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β (((ββπΆ)(
Β·π βπ)π) , ((ββπΆ)(
Β·π βπ)π)) = ((ββπΆ) Β· (π , π))) |
139 | 108, 109,
138 | oveq123d 7382 |
. . . . . . . . . . 11
β’ ((π β§ π β (0gβπ)) β ((π , π)(+gβπΉ)(((ββπΆ)( Β·π
βπ)π) , ((ββπΆ)(
Β·π βπ)π))) = ((π , π) + ((ββπΆ) Β· (π , π)))) |
140 | 6, 15, 5, 10, 93, 110, 63 | ipassr2 21074 |
. . . . . . . . . . . . . 14
β’ ((π β PreHil β§ (π β π β§ π β π β§ πΆ β πΎ)) β ((π , π)(.rβπΉ)πΆ) = (π ,
(((*πβπΉ)βπΆ)( Β·π
βπ)π))) |
141 | 102, 51, 92, 124, 140 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β ((π , π)(.rβπΉ)πΆ) = (π ,
(((*πβπΉ)βπΆ)( Β·π
βπ)π))) |
142 | 117 | oveqd 7378 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β ((π , π)(.rβπΉ)πΆ) = ((π , π) Β· πΆ)) |
143 | 134 | oveq2d 7377 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β (π ,
(((*πβπΉ)βπΆ)( Β·π
βπ)π)) = (π , ((ββπΆ)(
Β·π βπ)π))) |
144 | 141, 142,
143 | 3eqtr3rd 2782 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β (π , ((ββπΆ)(
Β·π βπ)π)) = ((π , π) Β· πΆ)) |
145 | 6, 15, 5, 10, 93, 110 | ipass 21072 |
. . . . . . . . . . . . . 14
β’ ((π β PreHil β§
((ββπΆ) β
πΎ β§ π β π β§ π β π)) β (((ββπΆ)(
Β·π βπ)π) , π) = ((ββπΆ)(.rβπΉ)(π , π))) |
146 | 102, 91, 92, 51, 145 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β (((ββπΆ)(
Β·π βπ)π) , π) = ((ββπΆ)(.rβπΉ)(π , π))) |
147 | 117 | oveqd 7378 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β ((ββπΆ)(.rβπΉ)(π , π)) = ((ββπΆ) Β· (π , π))) |
148 | 146, 147 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β (((ββπΆ)(
Β·π βπ)π) , π) = ((ββπΆ) Β· (π , π))) |
149 | 108, 144,
148 | oveq123d 7382 |
. . . . . . . . . . 11
β’ ((π β§ π β (0gβπ)) β ((π , ((ββπΆ)(
Β·π βπ)π))(+gβπΉ)(((ββπΆ)( Β·π
βπ)π) , π)) = (((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π)))) |
150 | 139, 149 | oveq12d 7379 |
. . . . . . . . . 10
β’ ((π β§ π β (0gβπ)) β (((π , π)(+gβπΉ)(((ββπΆ)( Β·π
βπ)π) , ((ββπΆ)(
Β·π βπ)π)))(-gβπΉ)((π , ((ββπΆ)(
Β·π βπ)π))(+gβπΉ)(((ββπΆ)( Β·π
βπ)π) , π))) = (((π , π) + ((ββπΆ) Β· (π , π)))(-gβπΉ)(((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π))))) |
151 | 6, 15, 5, 10 | ipcl 21060 |
. . . . . . . . . . . . . 14
β’ ((π β PreHil β§ π β π β§ π β π) β (π , π) β πΎ) |
152 | 102, 51, 51, 151 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β (π , π) β πΎ) |
153 | 6, 10 | clmmcl 24471 |
. . . . . . . . . . . . . 14
β’ ((π β βMod β§
(ββπΆ) β
πΎ β§ (π , π) β πΎ) β ((ββπΆ) Β· (π , π)) β πΎ) |
154 | 76, 91, 121, 153 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β ((ββπΆ) Β· (π , π)) β πΎ) |
155 | 6, 10 | clmacl 24470 |
. . . . . . . . . . . . 13
β’ ((π β βMod β§ (π , π) β πΎ β§ ((ββπΆ) Β· (π , π)) β πΎ) β ((π , π) + ((ββπΆ) Β· (π , π))) β πΎ) |
156 | 76, 152, 154, 155 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β ((π , π) + ((ββπΆ) Β· (π , π))) β πΎ) |
157 | 6, 10 | clmmcl 24471 |
. . . . . . . . . . . . . 14
β’ ((π β βMod β§ (π , π) β πΎ β§ πΆ β πΎ) β ((π , π) Β· πΆ) β πΎ) |
158 | 76, 77, 124, 157 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β ((π , π) Β· πΆ) β πΎ) |
159 | 6, 10 | clmacl 24470 |
. . . . . . . . . . . . 13
β’ ((π β βMod β§ ((π , π) Β· πΆ) β πΎ β§ ((ββπΆ) Β· (π , π)) β πΎ) β (((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π))) β πΎ) |
160 | 76, 158, 154, 159 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β (((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π))) β πΎ) |
161 | 6, 10 | clmsub 24466 |
. . . . . . . . . . . 12
β’ ((π β βMod β§ ((π , π) + ((ββπΆ) Β· (π , π))) β πΎ β§ (((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π))) β πΎ) β (((π , π) + ((ββπΆ) Β· (π , π))) β (((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π)))) = (((π , π) + ((ββπΆ) Β· (π , π)))(-gβπΉ)(((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π))))) |
162 | 76, 156, 160, 161 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π β (0gβπ)) β (((π , π) + ((ββπΆ) Β· (π , π))) β (((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π)))) = (((π , π) + ((ββπΆ) Β· (π , π)))(-gβπΉ)(((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π))))) |
163 | 4, 5, 6, 7, 8, 15 | tcphcphlem3 24620 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β (π , π) β β) |
164 | 13, 163 | mpdan 686 |
. . . . . . . . . . . . . 14
β’ (π β (π , π) β β) |
165 | 164 | recnd 11191 |
. . . . . . . . . . . . 13
β’ (π β (π , π) β β) |
166 | 165 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β (π , π) β β) |
167 | 18 | absvalsqd 15336 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((absβ(π , π))β2) = ((π , π) Β· (ββ(π , π)))) |
168 | 66 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π , π) Β· (ββ(π , π))) = ((π , π) Β· (π , π))) |
169 | 167, 168 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((absβ(π , π))β2) = ((π , π) Β· (π , π))) |
170 | 18 | abscld 15330 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (absβ(π , π)) β β) |
171 | 170 | resqcld 14039 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((absβ(π , π))β2) β β) |
172 | 169, 171 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π , π) Β· (π , π)) β β) |
173 | 172 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0gβπ)) β ((π , π) Β· (π , π)) β β) |
174 | 173, 71, 37 | redivcld 11991 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0gβπ)) β (((π , π) Β· (π , π)) / (π , π)) β β) |
175 | 41, 174 | eqeltrrd 2835 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β ((π , π) Β· πΆ) β β) |
176 | 175 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β ((π , π) Β· πΆ) β β) |
177 | 76, 11 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0gβπ)) β πΎ β β) |
178 | 177, 154 | sseldd 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0gβπ)) β ((ββπΆ) Β· (π , π)) β β) |
179 | 166, 176,
178 | pnpcan2d 11558 |
. . . . . . . . . . 11
β’ ((π β§ π β (0gβπ)) β (((π , π) + ((ββπΆ) Β· (π , π))) β (((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π)))) = ((π , π) β ((π , π) Β· πΆ))) |
180 | 162, 179 | eqtr3d 2775 |
. . . . . . . . . 10
β’ ((π β§ π β (0gβπ)) β (((π , π) + ((ββπΆ) Β· (π , π)))(-gβπΉ)(((π , π) Β· πΆ) + ((ββπΆ) Β· (π , π)))) = ((π , π) β ((π , π) Β· πΆ))) |
181 | 103, 150,
180 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π β (0gβπ)) β ((π(-gβπ)((ββπΆ)( Β·π
βπ)π)) , (π(-gβπ)((ββπΆ)( Β·π
βπ)π))) = ((π , π) β ((π , π) Β· πΆ))) |
182 | 99, 181 | breqtrd 5135 |
. . . . . . . 8
β’ ((π β§ π β (0gβπ)) β 0 β€ ((π , π) β ((π , π) Β· πΆ))) |
183 | 164 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0gβπ)) β (π , π) β β) |
184 | 183, 175 | subge0d 11753 |
. . . . . . . 8
β’ ((π β§ π β (0gβπ)) β (0 β€ ((π , π) β ((π , π) Β· πΆ)) β ((π , π) Β· πΆ) β€ (π , π))) |
185 | 182, 184 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π β (0gβπ)) β ((π , π) Β· πΆ) β€ (π , π)) |
186 | 41, 185 | eqbrtrd 5131 |
. . . . . 6
β’ ((π β§ π β (0gβπ)) β (((π , π) Β· (π , π)) / (π , π)) β€ (π , π)) |
187 | | oveq12 7370 |
. . . . . . . . . . . 12
β’ ((π₯ = π β§ π₯ = π) β (π₯ , π₯) = (π , π)) |
188 | 187 | anidms 568 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯ , π₯) = (π , π)) |
189 | 188 | breq2d 5121 |
. . . . . . . . . 10
β’ (π₯ = π β (0 β€ (π₯ , π₯) β 0 β€ (π , π))) |
190 | 189, 46, 14 | rspcdva 3584 |
. . . . . . . . 9
β’ (π β 0 β€ (π , π)) |
191 | 190 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0gβπ)) β 0 β€ (π , π)) |
192 | 71, 191, 37 | ne0gt0d 11300 |
. . . . . . 7
β’ ((π β§ π β (0gβπ)) β 0 < (π , π)) |
193 | | ledivmul2 12042 |
. . . . . . 7
β’ ((((π , π) Β· (π , π)) β β β§ (π , π) β β β§ ((π , π) β β β§ 0 < (π , π))) β ((((π , π) Β· (π , π)) / (π , π)) β€ (π , π) β ((π , π) Β· (π , π)) β€ ((π , π) Β· (π , π)))) |
194 | 173, 183,
71, 192, 193 | syl112anc 1375 |
. . . . . 6
β’ ((π β§ π β (0gβπ)) β ((((π , π) Β· (π , π)) / (π , π)) β€ (π , π) β ((π , π) Β· (π , π)) β€ ((π , π) Β· (π , π)))) |
195 | 186, 194 | mpbid 231 |
. . . . 5
β’ ((π β§ π β (0gβπ)) β ((π , π) Β· (π , π)) β€ ((π , π) Β· (π , π))) |
196 | 6, 15, 5, 31, 32 | ip0r 21064 |
. . . . . . . . . 10
β’ ((π β PreHil β§ π β π) β (π , (0gβπ)) = (0gβπΉ)) |
197 | 7, 13, 196 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π , (0gβπ)) = (0gβπΉ)) |
198 | 197, 29 | eqtr4d 2776 |
. . . . . . . 8
β’ (π β (π , (0gβπ)) = 0) |
199 | 198 | oveq1d 7376 |
. . . . . . 7
β’ (π β ((π , (0gβπ)) Β· (π , π)) = (0 Β· (π , π))) |
200 | 22 | mul02d 11361 |
. . . . . . 7
β’ (π β (0 Β· (π , π)) = 0) |
201 | 199, 200 | eqtrd 2773 |
. . . . . 6
β’ (π β ((π , (0gβπ)) Β· (π , π)) = 0) |
202 | | oveq12 7370 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π₯ = π) β (π₯ , π₯) = (π , π)) |
203 | 202 | anidms 568 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ , π₯) = (π , π)) |
204 | 203 | breq2d 5121 |
. . . . . . . 8
β’ (π₯ = π β (0 β€ (π₯ , π₯) β 0 β€ (π , π))) |
205 | 204, 46, 13 | rspcdva 3584 |
. . . . . . 7
β’ (π β 0 β€ (π , π)) |
206 | 164, 25, 205, 190 | mulge0d 11740 |
. . . . . 6
β’ (π β 0 β€ ((π , π) Β· (π , π))) |
207 | 201, 206 | eqbrtrd 5131 |
. . . . 5
β’ (π β ((π , (0gβπ)) Β· (π , π)) β€ ((π , π) Β· (π , π))) |
208 | 3, 195, 207 | pm2.61ne 3027 |
. . . 4
β’ (π β ((π , π) Β· (π , π)) β€ ((π , π) Β· (π , π))) |
209 | 164, 205 | resqrtcld 15311 |
. . . . . . 7
β’ (π β (ββ(π , π)) β β) |
210 | 209 | recnd 11191 |
. . . . . 6
β’ (π β (ββ(π , π)) β β) |
211 | 25, 190 | resqrtcld 15311 |
. . . . . . 7
β’ (π β (ββ(π , π)) β β) |
212 | 211 | recnd 11191 |
. . . . . 6
β’ (π β (ββ(π , π)) β β) |
213 | 210, 212 | sqmuld 14072 |
. . . . 5
β’ (π β (((ββ(π , π)) Β· (ββ(π , π)))β2) = (((ββ(π , π))β2) Β· ((ββ(π , π))β2))) |
214 | 165 | sqsqrtd 15333 |
. . . . . 6
β’ (π β ((ββ(π , π))β2) = (π , π)) |
215 | 26 | sqsqrtd 15333 |
. . . . . 6
β’ (π β ((ββ(π , π))β2) = (π , π)) |
216 | 214, 215 | oveq12d 7379 |
. . . . 5
β’ (π β (((ββ(π , π))β2) Β· ((ββ(π , π))β2)) = ((π , π) Β· (π , π))) |
217 | 213, 216 | eqtrd 2773 |
. . . 4
β’ (π β (((ββ(π , π)) Β· (ββ(π , π)))β2) = ((π , π) Β· (π , π))) |
218 | 208, 169,
217 | 3brtr4d 5141 |
. . 3
β’ (π β ((absβ(π , π))β2) β€ (((ββ(π , π)) Β· (ββ(π , π)))β2)) |
219 | 209, 211 | remulcld 11193 |
. . . 4
β’ (π β ((ββ(π , π)) Β· (ββ(π , π))) β β) |
220 | 18 | absge0d 15338 |
. . . 4
β’ (π β 0 β€ (absβ(π , π))) |
221 | 164, 205 | sqrtge0d 15314 |
. . . . 5
β’ (π β 0 β€
(ββ(π , π))) |
222 | 25, 190 | sqrtge0d 15314 |
. . . . 5
β’ (π β 0 β€
(ββ(π , π))) |
223 | 209, 211,
221, 222 | mulge0d 11740 |
. . . 4
β’ (π β 0 β€
((ββ(π , π)) Β·
(ββ(π , π)))) |
224 | 170, 219,
220, 223 | le2sqd 14169 |
. . 3
β’ (π β ((absβ(π , π)) β€ ((ββ(π , π)) Β· (ββ(π , π))) β ((absβ(π , π))β2) β€ (((ββ(π , π)) Β· (ββ(π , π)))β2))) |
225 | 218, 224 | mpbird 257 |
. 2
β’ (π β (absβ(π , π)) β€ ((ββ(π , π)) Β· (ββ(π , π)))) |
226 | | lmodgrp 20372 |
. . . . 5
β’ (π β LMod β π β Grp) |
227 | 49, 226 | syl 17 |
. . . 4
β’ (π β π β Grp) |
228 | | ipcau2.n |
. . . . 5
β’ π = (normβπΊ) |
229 | 4, 228, 5, 15 | tcphnmval 24616 |
. . . 4
β’ ((π β Grp β§ π β π) β (πβπ) = (ββ(π , π))) |
230 | 227, 13, 229 | syl2anc 585 |
. . 3
β’ (π β (πβπ) = (ββ(π , π))) |
231 | 4, 228, 5, 15 | tcphnmval 24616 |
. . . 4
β’ ((π β Grp β§ π β π) β (πβπ) = (ββ(π , π))) |
232 | 227, 14, 231 | syl2anc 585 |
. . 3
β’ (π β (πβπ) = (ββ(π , π))) |
233 | 230, 232 | oveq12d 7379 |
. 2
β’ (π β ((πβπ) Β· (πβπ)) = ((ββ(π , π)) Β· (ββ(π , π)))) |
234 | 225, 233 | breqtrrd 5137 |
1
β’ (π β (absβ(π , π)) β€ ((πβπ) Β· (πβπ))) |