Step | Hyp | Ref
| Expression |
1 | | abvtriv.a |
. . 3
β’ π΄ = (AbsValβπ
) |
2 | 1 | a1i 11 |
. 2
β’ (π β π΄ = (AbsValβπ
)) |
3 | | abvtriv.b |
. . 3
β’ π΅ = (Baseβπ
) |
4 | 3 | a1i 11 |
. 2
β’ (π β π΅ = (Baseβπ
)) |
5 | | eqidd 2734 |
. 2
β’ (π β (+gβπ
) = (+gβπ
)) |
6 | | abvtrivd.1 |
. . 3
β’ Β· =
(.rβπ
) |
7 | 6 | a1i 11 |
. 2
β’ (π β Β· =
(.rβπ
)) |
8 | | abvtriv.z |
. . 3
β’ 0 =
(0gβπ
) |
9 | 8 | a1i 11 |
. 2
β’ (π β 0 =
(0gβπ
)) |
10 | | abvtrivd.2 |
. 2
β’ (π β π
β Ring) |
11 | | 0re 11162 |
. . . . 5
β’ 0 β
β |
12 | | 1re 11160 |
. . . . 5
β’ 1 β
β |
13 | 11, 12 | ifcli 4534 |
. . . 4
β’ if(π₯ = 0 , 0, 1) β
β |
14 | 13 | a1i 11 |
. . 3
β’ ((π β§ π₯ β π΅) β if(π₯ = 0 , 0, 1) β
β) |
15 | | abvtriv.f |
. . 3
β’ πΉ = (π₯ β π΅ β¦ if(π₯ = 0 , 0, 1)) |
16 | 14, 15 | fmptd 7063 |
. 2
β’ (π β πΉ:π΅βΆβ) |
17 | 3, 8 | ring0cl 19995 |
. . 3
β’ (π
β Ring β 0 β π΅) |
18 | | iftrue 4493 |
. . . 4
β’ (π₯ = 0 β if(π₯ = 0 , 0, 1) =
0) |
19 | | c0ex 11154 |
. . . 4
β’ 0 β
V |
20 | 18, 15, 19 | fvmpt 6949 |
. . 3
β’ ( 0 β π΅ β (πΉβ 0 ) = 0) |
21 | 10, 17, 20 | 3syl 18 |
. 2
β’ (π β (πΉβ 0 ) = 0) |
22 | | 0lt1 11682 |
. . 3
β’ 0 <
1 |
23 | | eqeq1 2737 |
. . . . . . 7
β’ (π₯ = π¦ β (π₯ = 0 β π¦ = 0 )) |
24 | 23 | ifbid 4510 |
. . . . . 6
β’ (π₯ = π¦ β if(π₯ = 0 , 0, 1) = if(π¦ = 0 , 0, 1)) |
25 | | 1ex 11156 |
. . . . . . 7
β’ 1 β
V |
26 | 19, 25 | ifex 4537 |
. . . . . 6
β’ if(π¦ = 0 , 0, 1) β
V |
27 | 24, 15, 26 | fvmpt 6949 |
. . . . 5
β’ (π¦ β π΅ β (πΉβπ¦) = if(π¦ = 0 , 0, 1)) |
28 | | ifnefalse 4499 |
. . . . 5
β’ (π¦ β 0 β if(π¦ = 0 , 0, 1) =
1) |
29 | 27, 28 | sylan9eq 2793 |
. . . 4
β’ ((π¦ β π΅ β§ π¦ β 0 ) β (πΉβπ¦) = 1) |
30 | 29 | 3adant1 1131 |
. . 3
β’ ((π β§ π¦ β π΅ β§ π¦ β 0 ) β (πΉβπ¦) = 1) |
31 | 22, 30 | breqtrrid 5144 |
. 2
β’ ((π β§ π¦ β π΅ β§ π¦ β 0 ) β 0 < (πΉβπ¦)) |
32 | | 1t1e1 12320 |
. . . 4
β’ (1
Β· 1) = 1 |
33 | 32 | eqcomi 2742 |
. . 3
β’ 1 = (1
Β· 1) |
34 | 10 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β π
β Ring) |
35 | | simp2l 1200 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β π¦ β π΅) |
36 | | simp3l 1202 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β π§ β π΅) |
37 | 3, 6 | ringcl 19986 |
. . . . . 6
β’ ((π
β Ring β§ π¦ β π΅ β§ π§ β π΅) β (π¦ Β· π§) β π΅) |
38 | 34, 35, 36, 37 | syl3anc 1372 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (π¦ Β· π§) β π΅) |
39 | | eqeq1 2737 |
. . . . . . 7
β’ (π₯ = (π¦ Β· π§) β (π₯ = 0 β (π¦ Β· π§) = 0 )) |
40 | 39 | ifbid 4510 |
. . . . . 6
β’ (π₯ = (π¦ Β· π§) β if(π₯ = 0 , 0, 1) = if((π¦ Β· π§) = 0 , 0, 1)) |
41 | 19, 25 | ifex 4537 |
. . . . . 6
β’ if((π¦ Β· π§) = 0 , 0, 1) β
V |
42 | 40, 15, 41 | fvmpt 6949 |
. . . . 5
β’ ((π¦ Β· π§) β π΅ β (πΉβ(π¦ Β· π§)) = if((π¦ Β· π§) = 0 , 0, 1)) |
43 | 38, 42 | syl 17 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (πΉβ(π¦ Β· π§)) = if((π¦ Β· π§) = 0 , 0, 1)) |
44 | | abvtrivd.3 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (π¦ Β· π§) β 0 ) |
45 | 44 | neneqd 2945 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β Β¬ (π¦ Β· π§) = 0 ) |
46 | 45 | iffalsed 4498 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β if((π¦ Β· π§) = 0 , 0, 1) =
1) |
47 | 43, 46 | eqtrd 2773 |
. . 3
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (πΉβ(π¦ Β· π§)) = 1) |
48 | 35, 27 | syl 17 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (πΉβπ¦) = if(π¦ = 0 , 0, 1)) |
49 | | simp2r 1201 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β π¦ β 0 ) |
50 | 49 | neneqd 2945 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β Β¬ π¦ = 0 ) |
51 | 50 | iffalsed 4498 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β if(π¦ = 0 , 0, 1) =
1) |
52 | 48, 51 | eqtrd 2773 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (πΉβπ¦) = 1) |
53 | | eqeq1 2737 |
. . . . . . . 8
β’ (π₯ = π§ β (π₯ = 0 β π§ = 0 )) |
54 | 53 | ifbid 4510 |
. . . . . . 7
β’ (π₯ = π§ β if(π₯ = 0 , 0, 1) = if(π§ = 0 , 0, 1)) |
55 | 19, 25 | ifex 4537 |
. . . . . . 7
β’ if(π§ = 0 , 0, 1) β
V |
56 | 54, 15, 55 | fvmpt 6949 |
. . . . . 6
β’ (π§ β π΅ β (πΉβπ§) = if(π§ = 0 , 0, 1)) |
57 | 36, 56 | syl 17 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (πΉβπ§) = if(π§ = 0 , 0, 1)) |
58 | | simp3r 1203 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β π§ β 0 ) |
59 | 58 | neneqd 2945 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β Β¬ π§ = 0 ) |
60 | 59 | iffalsed 4498 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β if(π§ = 0 , 0, 1) =
1) |
61 | 57, 60 | eqtrd 2773 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (πΉβπ§) = 1) |
62 | 52, 61 | oveq12d 7376 |
. . 3
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β ((πΉβπ¦) Β· (πΉβπ§)) = (1 Β· 1)) |
63 | 33, 47, 62 | 3eqtr4a 2799 |
. 2
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (πΉβ(π¦ Β· π§)) = ((πΉβπ¦) Β· (πΉβπ§))) |
64 | | breq1 5109 |
. . . . . 6
β’ (0 =
if((π¦(+gβπ
)π§) = 0 , 0, 1) β (0 β€ 2
β if((π¦(+gβπ
)π§) = 0 , 0, 1) β€
2)) |
65 | | breq1 5109 |
. . . . . 6
β’ (1 =
if((π¦(+gβπ
)π§) = 0 , 0, 1) β (1 β€ 2
β if((π¦(+gβπ
)π§) = 0 , 0, 1) β€
2)) |
66 | | 0le2 12260 |
. . . . . 6
β’ 0 β€
2 |
67 | | 1le2 12367 |
. . . . . 6
β’ 1 β€
2 |
68 | 64, 65, 66, 67 | keephyp 4558 |
. . . . 5
β’ if((π¦(+gβπ
)π§) = 0 , 0, 1) β€
2 |
69 | | df-2 12221 |
. . . . 5
β’ 2 = (1 +
1) |
70 | 68, 69 | breqtri 5131 |
. . . 4
β’ if((π¦(+gβπ
)π§) = 0 , 0, 1) β€ (1 +
1) |
71 | 70 | a1i 11 |
. . 3
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β if((π¦(+gβπ
)π§) = 0 , 0, 1) β€ (1 +
1)) |
72 | | ringgrp 19974 |
. . . . . . 7
β’ (π
β Ring β π
β Grp) |
73 | 10, 72 | syl 17 |
. . . . . 6
β’ (π β π
β Grp) |
74 | 73 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β π
β Grp) |
75 | | eqid 2733 |
. . . . . 6
β’
(+gβπ
) = (+gβπ
) |
76 | 3, 75 | grpcl 18761 |
. . . . 5
β’ ((π
β Grp β§ π¦ β π΅ β§ π§ β π΅) β (π¦(+gβπ
)π§) β π΅) |
77 | 74, 35, 36, 76 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (π¦(+gβπ
)π§) β π΅) |
78 | | eqeq1 2737 |
. . . . . 6
β’ (π₯ = (π¦(+gβπ
)π§) β (π₯ = 0 β (π¦(+gβπ
)π§) = 0 )) |
79 | 78 | ifbid 4510 |
. . . . 5
β’ (π₯ = (π¦(+gβπ
)π§) β if(π₯ = 0 , 0, 1) = if((π¦(+gβπ
)π§) = 0 , 0, 1)) |
80 | 19, 25 | ifex 4537 |
. . . . 5
β’ if((π¦(+gβπ
)π§) = 0 , 0, 1) β
V |
81 | 79, 15, 80 | fvmpt 6949 |
. . . 4
β’ ((π¦(+gβπ
)π§) β π΅ β (πΉβ(π¦(+gβπ
)π§)) = if((π¦(+gβπ
)π§) = 0 , 0, 1)) |
82 | 77, 81 | syl 17 |
. . 3
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (πΉβ(π¦(+gβπ
)π§)) = if((π¦(+gβπ
)π§) = 0 , 0, 1)) |
83 | 52, 61 | oveq12d 7376 |
. . 3
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β ((πΉβπ¦) + (πΉβπ§)) = (1 + 1)) |
84 | 71, 82, 83 | 3brtr4d 5138 |
. 2
β’ ((π β§ (π¦ β π΅ β§ π¦ β 0 ) β§ (π§ β π΅ β§ π§ β 0 )) β (πΉβ(π¦(+gβπ
)π§)) β€ ((πΉβπ¦) + (πΉβπ§))) |
85 | 2, 4, 5, 7, 9, 10,
16, 21, 31, 63, 84 | isabvd 20293 |
1
β’ (π β πΉ β π΄) |