Step | Hyp | Ref
| Expression |
1 | | abvcxp.a |
. . 3
β’ π΄ = (AbsValβπ
) |
2 | 1 | a1i 11 |
. 2
β’ ((πΉ β π΄ β§ π β (0(,]1)) β π΄ = (AbsValβπ
)) |
3 | | abvcxp.b |
. . 3
β’ π΅ = (Baseβπ
) |
4 | 3 | a1i 11 |
. 2
β’ ((πΉ β π΄ β§ π β (0(,]1)) β π΅ = (Baseβπ
)) |
5 | | eqidd 2734 |
. 2
β’ ((πΉ β π΄ β§ π β (0(,]1)) β
(+gβπ
) =
(+gβπ
)) |
6 | | eqidd 2734 |
. 2
β’ ((πΉ β π΄ β§ π β (0(,]1)) β
(.rβπ
) =
(.rβπ
)) |
7 | | eqidd 2734 |
. 2
β’ ((πΉ β π΄ β§ π β (0(,]1)) β
(0gβπ
) =
(0gβπ
)) |
8 | 1 | abvrcl 20323 |
. . 3
β’ (πΉ β π΄ β π
β Ring) |
9 | 8 | adantr 482 |
. 2
β’ ((πΉ β π΄ β§ π β (0(,]1)) β π
β Ring) |
10 | 1, 3 | abvcl 20326 |
. . . . 5
β’ ((πΉ β π΄ β§ π₯ β π΅) β (πΉβπ₯) β β) |
11 | 10 | adantlr 714 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π₯ β π΅) β (πΉβπ₯) β β) |
12 | 1, 3 | abvge0 20327 |
. . . . 5
β’ ((πΉ β π΄ β§ π₯ β π΅) β 0 β€ (πΉβπ₯)) |
13 | 12 | adantlr 714 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π₯ β π΅) β 0 β€ (πΉβπ₯)) |
14 | | simpr 486 |
. . . . . . 7
β’ ((πΉ β π΄ β§ π β (0(,]1)) β π β (0(,]1)) |
15 | | 0xr 11210 |
. . . . . . . 8
β’ 0 β
β* |
16 | | 1re 11163 |
. . . . . . . 8
β’ 1 β
β |
17 | | elioc2 13336 |
. . . . . . . 8
β’ ((0
β β* β§ 1 β β) β (π β (0(,]1) β (π β β β§ 0 < π β§ π β€ 1))) |
18 | 15, 16, 17 | mp2an 691 |
. . . . . . 7
β’ (π β (0(,]1) β (π β β β§ 0 <
π β§ π β€ 1)) |
19 | 14, 18 | sylib 217 |
. . . . . 6
β’ ((πΉ β π΄ β§ π β (0(,]1)) β (π β β β§ 0 < π β§ π β€ 1)) |
20 | 19 | simp1d 1143 |
. . . . 5
β’ ((πΉ β π΄ β§ π β (0(,]1)) β π β β) |
21 | 20 | adantr 482 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π₯ β π΅) β π β β) |
22 | 11, 13, 21 | recxpcld 26101 |
. . 3
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π₯ β π΅) β ((πΉβπ₯)βππ) β β) |
23 | | abvcxp.f |
. . 3
β’ πΊ = (π₯ β π΅ β¦ ((πΉβπ₯)βππ)) |
24 | 22, 23 | fmptd 7066 |
. 2
β’ ((πΉ β π΄ β§ π β (0(,]1)) β πΊ:π΅βΆβ) |
25 | | eqid 2733 |
. . . . . 6
β’
(0gβπ
) = (0gβπ
) |
26 | 3, 25 | ring0cl 19998 |
. . . . 5
β’ (π
β Ring β
(0gβπ
)
β π΅) |
27 | 9, 26 | syl 17 |
. . . 4
β’ ((πΉ β π΄ β§ π β (0(,]1)) β
(0gβπ
)
β π΅) |
28 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = (0gβπ
) β (πΉβπ₯) = (πΉβ(0gβπ
))) |
29 | 28 | oveq1d 7376 |
. . . . 5
β’ (π₯ = (0gβπ
) β ((πΉβπ₯)βππ) = ((πΉβ(0gβπ
))βππ)) |
30 | | ovex 7394 |
. . . . 5
β’ ((πΉβ(0gβπ
))βππ) β V |
31 | 29, 23, 30 | fvmpt 6952 |
. . . 4
β’
((0gβπ
) β π΅ β (πΊβ(0gβπ
)) = ((πΉβ(0gβπ
))βππ)) |
32 | 27, 31 | syl 17 |
. . 3
β’ ((πΉ β π΄ β§ π β (0(,]1)) β (πΊβ(0gβπ
)) = ((πΉβ(0gβπ
))βππ)) |
33 | 1, 25 | abv0 20333 |
. . . . . 6
β’ (πΉ β π΄ β (πΉβ(0gβπ
)) = 0) |
34 | 33 | adantr 482 |
. . . . 5
β’ ((πΉ β π΄ β§ π β (0(,]1)) β (πΉβ(0gβπ
)) = 0) |
35 | 34 | oveq1d 7376 |
. . . 4
β’ ((πΉ β π΄ β§ π β (0(,]1)) β ((πΉβ(0gβπ
))βππ) =
(0βππ)) |
36 | 20 | recnd 11191 |
. . . . 5
β’ ((πΉ β π΄ β§ π β (0(,]1)) β π β β) |
37 | 19 | simp2d 1144 |
. . . . . 6
β’ ((πΉ β π΄ β§ π β (0(,]1)) β 0 < π) |
38 | 37 | gt0ne0d 11727 |
. . . . 5
β’ ((πΉ β π΄ β§ π β (0(,]1)) β π β 0) |
39 | 36, 38 | 0cxpd 26088 |
. . . 4
β’ ((πΉ β π΄ β§ π β (0(,]1)) β
(0βππ) = 0) |
40 | 35, 39 | eqtrd 2773 |
. . 3
β’ ((πΉ β π΄ β§ π β (0(,]1)) β ((πΉβ(0gβπ
))βππ) = 0) |
41 | 32, 40 | eqtrd 2773 |
. 2
β’ ((πΉ β π΄ β§ π β (0(,]1)) β (πΊβ(0gβπ
)) = 0) |
42 | | simp1l 1198 |
. . . . . . 7
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β πΉ β π΄) |
43 | | simp2 1138 |
. . . . . . 7
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β π¦ β π΅) |
44 | 1, 3 | abvcl 20326 |
. . . . . . 7
β’ ((πΉ β π΄ β§ π¦ β π΅) β (πΉβπ¦) β β) |
45 | 42, 43, 44 | syl2anc 585 |
. . . . . 6
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β (πΉβπ¦) β β) |
46 | 1, 3, 25 | abvgt0 20330 |
. . . . . . 7
β’ ((πΉ β π΄ β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β 0 < (πΉβπ¦)) |
47 | 46 | 3adant1r 1178 |
. . . . . 6
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β 0 < (πΉβπ¦)) |
48 | 45, 47 | elrpd 12962 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β (πΉβπ¦) β
β+) |
49 | 20 | 3ad2ant1 1134 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β π β β) |
50 | 48, 49 | rpcxpcld 26110 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β ((πΉβπ¦)βππ) β
β+) |
51 | 50 | rpgt0d 12968 |
. . 3
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β 0 < ((πΉβπ¦)βππ)) |
52 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
53 | 52 | oveq1d 7376 |
. . . . 5
β’ (π₯ = π¦ β ((πΉβπ₯)βππ) = ((πΉβπ¦)βππ)) |
54 | | ovex 7394 |
. . . . 5
β’ ((πΉβπ¦)βππ) β V |
55 | 53, 23, 54 | fvmpt 6952 |
. . . 4
β’ (π¦ β π΅ β (πΊβπ¦) = ((πΉβπ¦)βππ)) |
56 | 43, 55 | syl 17 |
. . 3
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β (πΊβπ¦) = ((πΉβπ¦)βππ)) |
57 | 51, 56 | breqtrrd 5137 |
. 2
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ π¦ β π΅ β§ π¦ β (0gβπ
)) β 0 < (πΊβπ¦)) |
58 | | simp1l 1198 |
. . . . . 6
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β πΉ β π΄) |
59 | | simp2l 1200 |
. . . . . 6
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β π¦ β π΅) |
60 | | simp3l 1202 |
. . . . . 6
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β π§ β π΅) |
61 | | eqid 2733 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
62 | 1, 3, 61 | abvmul 20331 |
. . . . . 6
β’ ((πΉ β π΄ β§ π¦ β π΅ β§ π§ β π΅) β (πΉβ(π¦(.rβπ
)π§)) = ((πΉβπ¦) Β· (πΉβπ§))) |
63 | 58, 59, 60, 62 | syl3anc 1372 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΉβ(π¦(.rβπ
)π§)) = ((πΉβπ¦) Β· (πΉβπ§))) |
64 | 63 | oveq1d 7376 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΉβ(π¦(.rβπ
)π§))βππ) = (((πΉβπ¦) Β· (πΉβπ§))βππ)) |
65 | 58, 59, 44 | syl2anc 585 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΉβπ¦) β β) |
66 | 1, 3 | abvge0 20327 |
. . . . . 6
β’ ((πΉ β π΄ β§ π¦ β π΅) β 0 β€ (πΉβπ¦)) |
67 | 58, 59, 66 | syl2anc 585 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β 0 β€ (πΉβπ¦)) |
68 | 1, 3 | abvcl 20326 |
. . . . . 6
β’ ((πΉ β π΄ β§ π§ β π΅) β (πΉβπ§) β β) |
69 | 58, 60, 68 | syl2anc 585 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΉβπ§) β β) |
70 | 1, 3 | abvge0 20327 |
. . . . . 6
β’ ((πΉ β π΄ β§ π§ β π΅) β 0 β€ (πΉβπ§)) |
71 | 58, 60, 70 | syl2anc 585 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β 0 β€ (πΉβπ§)) |
72 | 36 | 3ad2ant1 1134 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β π β β) |
73 | 65, 67, 69, 71, 72 | mulcxpd 26106 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (((πΉβπ¦) Β· (πΉβπ§))βππ) = (((πΉβπ¦)βππ) Β· ((πΉβπ§)βππ))) |
74 | 64, 73 | eqtrd 2773 |
. . 3
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΉβ(π¦(.rβπ
)π§))βππ) = (((πΉβπ¦)βππ) Β· ((πΉβπ§)βππ))) |
75 | 9 | 3ad2ant1 1134 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β π
β Ring) |
76 | 3, 61 | ringcl 19989 |
. . . . 5
β’ ((π
β Ring β§ π¦ β π΅ β§ π§ β π΅) β (π¦(.rβπ
)π§) β π΅) |
77 | 75, 59, 60, 76 | syl3anc 1372 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (π¦(.rβπ
)π§) β π΅) |
78 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = (π¦(.rβπ
)π§) β (πΉβπ₯) = (πΉβ(π¦(.rβπ
)π§))) |
79 | 78 | oveq1d 7376 |
. . . . 5
β’ (π₯ = (π¦(.rβπ
)π§) β ((πΉβπ₯)βππ) = ((πΉβ(π¦(.rβπ
)π§))βππ)) |
80 | | ovex 7394 |
. . . . 5
β’ ((πΉβ(π¦(.rβπ
)π§))βππ) β V |
81 | 79, 23, 80 | fvmpt 6952 |
. . . 4
β’ ((π¦(.rβπ
)π§) β π΅ β (πΊβ(π¦(.rβπ
)π§)) = ((πΉβ(π¦(.rβπ
)π§))βππ)) |
82 | 77, 81 | syl 17 |
. . 3
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΊβ(π¦(.rβπ
)π§)) = ((πΉβ(π¦(.rβπ
)π§))βππ)) |
83 | 59, 55 | syl 17 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΊβπ¦) = ((πΉβπ¦)βππ)) |
84 | | fveq2 6846 |
. . . . . . 7
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
85 | 84 | oveq1d 7376 |
. . . . . 6
β’ (π₯ = π§ β ((πΉβπ₯)βππ) = ((πΉβπ§)βππ)) |
86 | | ovex 7394 |
. . . . . 6
β’ ((πΉβπ§)βππ) β V |
87 | 85, 23, 86 | fvmpt 6952 |
. . . . 5
β’ (π§ β π΅ β (πΊβπ§) = ((πΉβπ§)βππ)) |
88 | 60, 87 | syl 17 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΊβπ§) = ((πΉβπ§)βππ)) |
89 | 83, 88 | oveq12d 7379 |
. . 3
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΊβπ¦) Β· (πΊβπ§)) = (((πΉβπ¦)βππ) Β· ((πΉβπ§)βππ))) |
90 | 74, 82, 89 | 3eqtr4d 2783 |
. 2
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΊβ(π¦(.rβπ
)π§)) = ((πΊβπ¦) Β· (πΊβπ§))) |
91 | | ringgrp 19977 |
. . . . . . . 8
β’ (π
β Ring β π
β Grp) |
92 | 75, 91 | syl 17 |
. . . . . . 7
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β π
β Grp) |
93 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπ
) = (+gβπ
) |
94 | 3, 93 | grpcl 18764 |
. . . . . . 7
β’ ((π
β Grp β§ π¦ β π΅ β§ π§ β π΅) β (π¦(+gβπ
)π§) β π΅) |
95 | 92, 59, 60, 94 | syl3anc 1372 |
. . . . . 6
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (π¦(+gβπ
)π§) β π΅) |
96 | 1, 3 | abvcl 20326 |
. . . . . 6
β’ ((πΉ β π΄ β§ (π¦(+gβπ
)π§) β π΅) β (πΉβ(π¦(+gβπ
)π§)) β β) |
97 | 58, 95, 96 | syl2anc 585 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΉβ(π¦(+gβπ
)π§)) β β) |
98 | 1, 3 | abvge0 20327 |
. . . . . 6
β’ ((πΉ β π΄ β§ (π¦(+gβπ
)π§) β π΅) β 0 β€ (πΉβ(π¦(+gβπ
)π§))) |
99 | 58, 95, 98 | syl2anc 585 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β 0 β€ (πΉβ(π¦(+gβπ
)π§))) |
100 | 19 | 3ad2ant1 1134 |
. . . . . 6
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (π β β β§ 0 < π β§ π β€ 1)) |
101 | 100 | simp1d 1143 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β π β β) |
102 | 97, 99, 101 | recxpcld 26101 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΉβ(π¦(+gβπ
)π§))βππ) β β) |
103 | 65, 69 | readdcld 11192 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΉβπ¦) + (πΉβπ§)) β β) |
104 | 65, 69, 67, 71 | addge0d 11739 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β 0 β€ ((πΉβπ¦) + (πΉβπ§))) |
105 | 103, 104,
101 | recxpcld 26101 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (((πΉβπ¦) + (πΉβπ§))βππ) β β) |
106 | 65, 67, 101 | recxpcld 26101 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΉβπ¦)βππ) β β) |
107 | 69, 71, 101 | recxpcld 26101 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΉβπ§)βππ) β β) |
108 | 106, 107 | readdcld 11192 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (((πΉβπ¦)βππ) + ((πΉβπ§)βππ)) β β) |
109 | 1, 3, 93 | abvtri 20332 |
. . . . . 6
β’ ((πΉ β π΄ β§ π¦ β π΅ β§ π§ β π΅) β (πΉβ(π¦(+gβπ
)π§)) β€ ((πΉβπ¦) + (πΉβπ§))) |
110 | 58, 59, 60, 109 | syl3anc 1372 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΉβ(π¦(+gβπ
)π§)) β€ ((πΉβπ¦) + (πΉβπ§))) |
111 | 100 | simp2d 1144 |
. . . . . . 7
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β 0 < π) |
112 | 101, 111 | elrpd 12962 |
. . . . . 6
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β π β
β+) |
113 | 97, 99, 103, 104, 112 | cxple2d 26105 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΉβ(π¦(+gβπ
)π§)) β€ ((πΉβπ¦) + (πΉβπ§)) β ((πΉβ(π¦(+gβπ
)π§))βππ) β€ (((πΉβπ¦) + (πΉβπ§))βππ))) |
114 | 110, 113 | mpbid 231 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΉβ(π¦(+gβπ
)π§))βππ) β€ (((πΉβπ¦) + (πΉβπ§))βππ)) |
115 | 100 | simp3d 1145 |
. . . . 5
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β π β€ 1) |
116 | 65, 67, 69, 71, 112, 115 | cxpaddle 26128 |
. . . 4
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (((πΉβπ¦) + (πΉβπ§))βππ) β€ (((πΉβπ¦)βππ) + ((πΉβπ§)βππ))) |
117 | 102, 105,
108, 114, 116 | letrd 11320 |
. . 3
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΉβ(π¦(+gβπ
)π§))βππ) β€ (((πΉβπ¦)βππ) + ((πΉβπ§)βππ))) |
118 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = (π¦(+gβπ
)π§) β (πΉβπ₯) = (πΉβ(π¦(+gβπ
)π§))) |
119 | 118 | oveq1d 7376 |
. . . . 5
β’ (π₯ = (π¦(+gβπ
)π§) β ((πΉβπ₯)βππ) = ((πΉβ(π¦(+gβπ
)π§))βππ)) |
120 | | ovex 7394 |
. . . . 5
β’ ((πΉβ(π¦(+gβπ
)π§))βππ) β V |
121 | 119, 23, 120 | fvmpt 6952 |
. . . 4
β’ ((π¦(+gβπ
)π§) β π΅ β (πΊβ(π¦(+gβπ
)π§)) = ((πΉβ(π¦(+gβπ
)π§))βππ)) |
122 | 95, 121 | syl 17 |
. . 3
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΊβ(π¦(+gβπ
)π§)) = ((πΉβ(π¦(+gβπ
)π§))βππ)) |
123 | 83, 88 | oveq12d 7379 |
. . 3
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β ((πΊβπ¦) + (πΊβπ§)) = (((πΉβπ¦)βππ) + ((πΉβπ§)βππ))) |
124 | 117, 122,
123 | 3brtr4d 5141 |
. 2
β’ (((πΉ β π΄ β§ π β (0(,]1)) β§ (π¦ β π΅ β§ π¦ β (0gβπ
)) β§ (π§ β π΅ β§ π§ β (0gβπ
))) β (πΊβ(π¦(+gβπ
)π§)) β€ ((πΊβπ¦) + (πΊβπ§))) |
125 | 2, 4, 5, 6, 7, 9, 24, 41, 57, 90, 124 | isabvd 20322 |
1
β’ ((πΉ β π΄ β§ π β (0(,]1)) β πΊ β π΄) |