Step | Hyp | Ref
| Expression |
1 | | isabvd.2 |
. . . . . 6
β’ (π β πΉ:π΅βΆβ) |
2 | | isabvd.b |
. . . . . . 7
β’ (π β π΅ = (Baseβπ
)) |
3 | 2 | feq2d 6704 |
. . . . . 6
β’ (π β (πΉ:π΅βΆβ β πΉ:(Baseβπ
)βΆβ)) |
4 | 1, 3 | mpbid 231 |
. . . . 5
β’ (π β πΉ:(Baseβπ
)βΆβ) |
5 | 4 | ffnd 6719 |
. . . 4
β’ (π β πΉ Fn (Baseβπ
)) |
6 | 4 | ffvelcdmda 7087 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ
)) β (πΉβπ₯) β β) |
7 | | 0le0 12313 |
. . . . . . . . . 10
β’ 0 β€
0 |
8 | | isabvd.z |
. . . . . . . . . . . 12
β’ (π β 0 =
(0gβπ
)) |
9 | 8 | fveq2d 6896 |
. . . . . . . . . . 11
β’ (π β (πΉβ 0 ) = (πΉβ(0gβπ
))) |
10 | | isabvd.3 |
. . . . . . . . . . 11
β’ (π β (πΉβ 0 ) = 0) |
11 | 9, 10 | eqtr3d 2775 |
. . . . . . . . . 10
β’ (π β (πΉβ(0gβπ
)) = 0) |
12 | 7, 11 | breqtrrid 5187 |
. . . . . . . . 9
β’ (π β 0 β€ (πΉβ(0gβπ
))) |
13 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
)) β 0 β€ (πΉβ(0gβπ
))) |
14 | | fveq2 6892 |
. . . . . . . . 9
β’ (π₯ = (0gβπ
) β (πΉβπ₯) = (πΉβ(0gβπ
))) |
15 | 14 | breq2d 5161 |
. . . . . . . 8
β’ (π₯ = (0gβπ
) β (0 β€ (πΉβπ₯) β 0 β€ (πΉβ(0gβπ
)))) |
16 | 13, 15 | syl5ibrcom 246 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ
)) β (π₯ = (0gβπ
) β 0 β€ (πΉβπ₯))) |
17 | | simp1 1137 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β π) |
18 | | simp2 1138 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β π₯ β (Baseβπ
)) |
19 | 2 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β π΅ = (Baseβπ
)) |
20 | 18, 19 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β π₯ β π΅) |
21 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β π₯ β (0gβπ
)) |
22 | 8 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β 0 =
(0gβπ
)) |
23 | 21, 22 | neeqtrrd 3016 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β π₯ β 0 ) |
24 | | isabvd.4 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅ β§ π₯ β 0 ) β 0 < (πΉβπ₯)) |
25 | 17, 20, 23, 24 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β 0 < (πΉβπ₯)) |
26 | | 0re 11216 |
. . . . . . . . . 10
β’ 0 β
β |
27 | 6 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β (πΉβπ₯) β β) |
28 | | ltle 11302 |
. . . . . . . . . 10
β’ ((0
β β β§ (πΉβπ₯) β β) β (0 < (πΉβπ₯) β 0 β€ (πΉβπ₯))) |
29 | 26, 27, 28 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β (0 < (πΉβπ₯) β 0 β€ (πΉβπ₯))) |
30 | 25, 29 | mpd 15 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β 0 β€ (πΉβπ₯)) |
31 | 30 | 3expia 1122 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ
)) β (π₯ β (0gβπ
) β 0 β€ (πΉβπ₯))) |
32 | 16, 31 | pm2.61dne 3029 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ
)) β 0 β€ (πΉβπ₯)) |
33 | | elrege0 13431 |
. . . . . 6
β’ ((πΉβπ₯) β (0[,)+β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
34 | 6, 32, 33 | sylanbrc 584 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ
)) β (πΉβπ₯) β (0[,)+β)) |
35 | 34 | ralrimiva 3147 |
. . . 4
β’ (π β βπ₯ β (Baseβπ
)(πΉβπ₯) β (0[,)+β)) |
36 | | ffnfv 7118 |
. . . 4
β’ (πΉ:(Baseβπ
)βΆ(0[,)+β) β (πΉ Fn (Baseβπ
) β§ βπ₯ β (Baseβπ
)(πΉβπ₯) β (0[,)+β))) |
37 | 5, 35, 36 | sylanbrc 584 |
. . 3
β’ (π β πΉ:(Baseβπ
)βΆ(0[,)+β)) |
38 | 25 | gt0ne0d 11778 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
) β§ π₯ β (0gβπ
)) β (πΉβπ₯) β 0) |
39 | 38 | 3expia 1122 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ
)) β (π₯ β (0gβπ
) β (πΉβπ₯) β 0)) |
40 | 39 | necon4d 2965 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ
)) β ((πΉβπ₯) = 0 β π₯ = (0gβπ
))) |
41 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ
)) β (πΉβ(0gβπ
)) = 0) |
42 | | fveqeq2 6901 |
. . . . . . 7
β’ (π₯ = (0gβπ
) β ((πΉβπ₯) = 0 β (πΉβ(0gβπ
)) = 0)) |
43 | 41, 42 | syl5ibrcom 246 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ
)) β (π₯ = (0gβπ
) β (πΉβπ₯) = 0)) |
44 | 40, 43 | impbid 211 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ
)) β ((πΉβπ₯) = 0 β π₯ = (0gβπ
))) |
45 | 11 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (πΉβ(0gβπ
)) = 0) |
46 | 45 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (πΉβ(0gβπ
)) = 0) |
47 | | oveq1 7416 |
. . . . . . . . . . . 12
β’ (π₯ = (0gβπ
) β (π₯(.rβπ
)π¦) = ((0gβπ
)(.rβπ
)π¦)) |
48 | | isabvd.1 |
. . . . . . . . . . . . . 14
β’ (π β π
β Ring) |
49 | 48 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β π
β Ring) |
50 | | simp3 1139 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β π¦ β (Baseβπ
)) |
51 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Baseβπ
) =
(Baseβπ
) |
52 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(.rβπ
) = (.rβπ
) |
53 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(0gβπ
) = (0gβπ
) |
54 | 51, 52, 53 | ringlz 20107 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π¦ β (Baseβπ
)) β
((0gβπ
)(.rβπ
)π¦) = (0gβπ
)) |
55 | 49, 50, 54 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β ((0gβπ
)(.rβπ
)π¦) = (0gβπ
)) |
56 | 47, 55 | sylan9eqr 2795 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (π₯(.rβπ
)π¦) = (0gβπ
)) |
57 | 56 | fveq2d 6896 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (πΉβ(π₯(.rβπ
)π¦)) = (πΉβ(0gβπ
))) |
58 | 14, 45 | sylan9eqr 2795 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (πΉβπ₯) = 0) |
59 | 58 | oveq1d 7424 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β ((πΉβπ₯) Β· (πΉβπ¦)) = (0 Β· (πΉβπ¦))) |
60 | 4 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β πΉ:(Baseβπ
)βΆβ) |
61 | 60, 50 | ffvelcdmd 7088 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (πΉβπ¦) β β) |
62 | 61 | recnd 11242 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (πΉβπ¦) β β) |
63 | 62 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (πΉβπ¦) β β) |
64 | 63 | mul02d 11412 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (0 Β· (πΉβπ¦)) = 0) |
65 | 59, 64 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β ((πΉβπ₯) Β· (πΉβπ¦)) = 0) |
66 | 46, 57, 65 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
67 | 45 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (πΉβ(0gβπ
)) = 0) |
68 | | oveq2 7417 |
. . . . . . . . . . . 12
β’ (π¦ = (0gβπ
) β (π₯(.rβπ
)π¦) = (π₯(.rβπ
)(0gβπ
))) |
69 | | simp2 1138 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β π₯ β (Baseβπ
)) |
70 | 51, 52, 53 | ringrz 20108 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π₯ β (Baseβπ
)) β (π₯(.rβπ
)(0gβπ
)) = (0gβπ
)) |
71 | 49, 69, 70 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (π₯(.rβπ
)(0gβπ
)) = (0gβπ
)) |
72 | 68, 71 | sylan9eqr 2795 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (π₯(.rβπ
)π¦) = (0gβπ
)) |
73 | 72 | fveq2d 6896 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (πΉβ(π₯(.rβπ
)π¦)) = (πΉβ(0gβπ
))) |
74 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π¦ = (0gβπ
) β (πΉβπ¦) = (πΉβ(0gβπ
))) |
75 | 74, 45 | sylan9eqr 2795 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (πΉβπ¦) = 0) |
76 | 75 | oveq2d 7425 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β ((πΉβπ₯) Β· (πΉβπ¦)) = ((πΉβπ₯) Β· 0)) |
77 | 60, 69 | ffvelcdmd 7088 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (πΉβπ₯) β β) |
78 | 77 | recnd 11242 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (πΉβπ₯) β β) |
79 | 78 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (πΉβπ₯) β β) |
80 | 79 | mul01d 11413 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β ((πΉβπ₯) Β· 0) = 0) |
81 | 76, 80 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β ((πΉβπ₯) Β· (πΉβπ¦)) = 0) |
82 | 67, 73, 81 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
83 | | simpl1 1192 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β π) |
84 | | isabvd.t |
. . . . . . . . . . . . 13
β’ (π β Β· =
(.rβπ
)) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β Β· =
(.rβπ
)) |
86 | 85 | oveqd 7426 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β (π₯ Β· π¦) = (π₯(.rβπ
)π¦)) |
87 | 86 | fveq2d 6896 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β (πΉβ(π₯ Β· π¦)) = (πΉβ(π₯(.rβπ
)π¦))) |
88 | | simpl2 1193 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β π₯ β (Baseβπ
)) |
89 | 83, 2 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β π΅ = (Baseβπ
)) |
90 | 88, 89 | eleqtrrd 2837 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β π₯ β π΅) |
91 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β π₯ β (0gβπ
)) |
92 | 83, 8 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β 0 =
(0gβπ
)) |
93 | 91, 92 | neeqtrrd 3016 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β π₯ β 0 ) |
94 | | simpl3 1194 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β π¦ β (Baseβπ
)) |
95 | 94, 89 | eleqtrrd 2837 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β π¦ β π΅) |
96 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β π¦ β (0gβπ
)) |
97 | 96, 92 | neeqtrrd 3016 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β π¦ β 0 ) |
98 | | isabvd.5 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
99 | 83, 90, 93, 95, 97, 98 | syl122anc 1380 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β (πΉβ(π₯ Β· π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
100 | 87, 99 | eqtr3d 2775 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β (πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
101 | 66, 82, 100 | pm2.61da2ne 3031 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
102 | | oveq1 7416 |
. . . . . . . . . . . 12
β’ (π₯ = (0gβπ
) β (π₯(+gβπ
)π¦) = ((0gβπ
)(+gβπ
)π¦)) |
103 | | ringgrp 20061 |
. . . . . . . . . . . . . 14
β’ (π
β Ring β π
β Grp) |
104 | 49, 103 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β π
β Grp) |
105 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(+gβπ
) = (+gβπ
) |
106 | 51, 105, 53 | grplid 18852 |
. . . . . . . . . . . . 13
β’ ((π
β Grp β§ π¦ β (Baseβπ
)) β
((0gβπ
)(+gβπ
)π¦) = π¦) |
107 | 104, 50, 106 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β ((0gβπ
)(+gβπ
)π¦) = π¦) |
108 | 102, 107 | sylan9eqr 2795 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (π₯(+gβπ
)π¦) = π¦) |
109 | 108 | fveq2d 6896 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (πΉβ(π₯(+gβπ
)π¦)) = (πΉβπ¦)) |
110 | 7, 58 | breqtrrid 5187 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β 0 β€ (πΉβπ₯)) |
111 | 61, 77 | addge02d 11803 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (0 β€ (πΉβπ₯) β (πΉβπ¦) β€ ((πΉβπ₯) + (πΉβπ¦)))) |
112 | 111 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (0 β€ (πΉβπ₯) β (πΉβπ¦) β€ ((πΉβπ₯) + (πΉβπ¦)))) |
113 | 110, 112 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (πΉβπ¦) β€ ((πΉβπ₯) + (πΉβπ¦))) |
114 | 109, 113 | eqbrtrd 5171 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π₯ = (0gβπ
)) β (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
115 | | oveq2 7417 |
. . . . . . . . . . . 12
β’ (π¦ = (0gβπ
) β (π₯(+gβπ
)π¦) = (π₯(+gβπ
)(0gβπ
))) |
116 | 51, 105, 53 | grprid 18853 |
. . . . . . . . . . . . 13
β’ ((π
β Grp β§ π₯ β (Baseβπ
)) β (π₯(+gβπ
)(0gβπ
)) = π₯) |
117 | 104, 69, 116 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (π₯(+gβπ
)(0gβπ
)) = π₯) |
118 | 115, 117 | sylan9eqr 2795 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (π₯(+gβπ
)π¦) = π₯) |
119 | 118 | fveq2d 6896 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (πΉβ(π₯(+gβπ
)π¦)) = (πΉβπ₯)) |
120 | 7, 75 | breqtrrid 5187 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β 0 β€ (πΉβπ¦)) |
121 | 77, 61 | addge01d 11802 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (0 β€ (πΉβπ¦) β (πΉβπ₯) β€ ((πΉβπ₯) + (πΉβπ¦)))) |
122 | 121 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (0 β€ (πΉβπ¦) β (πΉβπ₯) β€ ((πΉβπ₯) + (πΉβπ¦)))) |
123 | 120, 122 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (πΉβπ₯) β€ ((πΉβπ₯) + (πΉβπ¦))) |
124 | 119, 123 | eqbrtrd 5171 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ π¦ = (0gβπ
)) β (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
125 | | isabvd.p |
. . . . . . . . . . . . 13
β’ (π β + =
(+gβπ
)) |
126 | 83, 125 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β + =
(+gβπ
)) |
127 | 126 | oveqd 7426 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β (π₯ + π¦) = (π₯(+gβπ
)π¦)) |
128 | 127 | fveq2d 6896 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β (πΉβ(π₯ + π¦)) = (πΉβ(π₯(+gβπ
)π¦))) |
129 | | isabvd.6 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΅ β§ π₯ β 0 ) β§ (π¦ β π΅ β§ π¦ β 0 )) β (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
130 | 83, 90, 93, 95, 97, 129 | syl122anc 1380 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β (πΉβ(π₯ + π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
131 | 128, 130 | eqbrtrrd 5173 |
. . . . . . . . 9
β’ (((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β§ (π₯ β (0gβπ
) β§ π¦ β (0gβπ
))) β (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
132 | 114, 124,
131 | pm2.61da2ne 3031 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) |
133 | 101, 132 | jca 513 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ
) β§ π¦ β (Baseβπ
)) β ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))) |
134 | 133 | 3expia 1122 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ
)) β (π¦ β (Baseβπ
) β ((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))) |
135 | 134 | ralrimiv 3146 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ
)) β βπ¦ β (Baseβπ
)((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦)))) |
136 | 44, 135 | jca 513 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ
)) β (((πΉβπ₯) = 0 β π₯ = (0gβπ
)) β§ βπ¦ β (Baseβπ
)((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))) |
137 | 136 | ralrimiva 3147 |
. . 3
β’ (π β βπ₯ β (Baseβπ
)(((πΉβπ₯) = 0 β π₯ = (0gβπ
)) β§ βπ¦ β (Baseβπ
)((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))) |
138 | | eqid 2733 |
. . . . 5
β’
(AbsValβπ
) =
(AbsValβπ
) |
139 | 138, 51, 105, 52, 53 | isabv 20427 |
. . . 4
β’ (π
β Ring β (πΉ β (AbsValβπ
) β (πΉ:(Baseβπ
)βΆ(0[,)+β) β§ βπ₯ β (Baseβπ
)(((πΉβπ₯) = 0 β π₯ = (0gβπ
)) β§ βπ¦ β (Baseβπ
)((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))))) |
140 | 48, 139 | syl 17 |
. . 3
β’ (π β (πΉ β (AbsValβπ
) β (πΉ:(Baseβπ
)βΆ(0[,)+β) β§ βπ₯ β (Baseβπ
)(((πΉβπ₯) = 0 β π₯ = (0gβπ
)) β§ βπ¦ β (Baseβπ
)((πΉβ(π₯(.rβπ
)π¦)) = ((πΉβπ₯) Β· (πΉβπ¦)) β§ (πΉβ(π₯(+gβπ
)π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))))))) |
141 | 37, 137, 140 | mpbir2and 712 |
. 2
β’ (π β πΉ β (AbsValβπ
)) |
142 | | isabvd.a |
. 2
β’ (π β π΄ = (AbsValβπ
)) |
143 | 141, 142 | eleqtrrd 2837 |
1
β’ (π β πΉ β π΄) |