Step | Hyp | Ref
| Expression |
1 | | mdegaddle.y |
. . . . . . . . . 10
β’ π = (πΌ mPoly π
) |
2 | | mdegaddle.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
3 | | eqid 2733 |
. . . . . . . . . 10
β’
(+gβπ
) = (+gβπ
) |
4 | | mdegaddle.p |
. . . . . . . . . 10
β’ + =
(+gβπ) |
5 | | mdegaddle.f |
. . . . . . . . . 10
β’ (π β πΉ β π΅) |
6 | | mdegaddle.g |
. . . . . . . . . 10
β’ (π β πΊ β π΅) |
7 | 1, 2, 3, 4, 5, 6 | mpladd 21436 |
. . . . . . . . 9
β’ (π β (πΉ + πΊ) = (πΉ βf
(+gβπ
)πΊ)) |
8 | 7 | fveq1d 6848 |
. . . . . . . 8
β’ (π β ((πΉ + πΊ)βπ) = ((πΉ βf
(+gβπ
)πΊ)βπ)) |
9 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((πΉ + πΊ)βπ) = ((πΉ βf
(+gβπ
)πΊ)βπ)) |
10 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
11 | | eqid 2733 |
. . . . . . . . . . 11
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
12 | 1, 10, 2, 11, 5 | mplelf 21427 |
. . . . . . . . . 10
β’ (π β πΉ:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ
)) |
13 | 12 | ffnd 6673 |
. . . . . . . . 9
β’ (π β πΉ Fn {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
14 | 13 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β πΉ Fn {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
15 | 1, 10, 2, 11, 6 | mplelf 21427 |
. . . . . . . . . 10
β’ (π β πΊ:{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆ(Baseβπ
)) |
16 | 15 | ffnd 6673 |
. . . . . . . . 9
β’ (π β πΊ Fn {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
17 | 16 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β πΊ Fn {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
18 | | ovex 7394 |
. . . . . . . . . 10
β’
(β0 βm πΌ) β V |
19 | 18 | rabex 5293 |
. . . . . . . . 9
β’ {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β
V |
20 | 19 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β
V) |
21 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β π β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
22 | | fnfvof 7638 |
. . . . . . . 8
β’ (((πΉ Fn {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ πΊ Fn {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β§ ({π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β V β§
π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin})) β
((πΉ βf
(+gβπ
)πΊ)βπ) = ((πΉβπ)(+gβπ
)(πΊβπ))) |
23 | 14, 17, 20, 21, 22 | syl22anc 838 |
. . . . . . 7
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((πΉ βf
(+gβπ
)πΊ)βπ) = ((πΉβπ)(+gβπ
)(πΊβπ))) |
24 | 9, 23 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((πΉ + πΊ)βπ) = ((πΉβπ)(+gβπ
)(πΊβπ))) |
25 | 24 | adantrr 716 |
. . . . 5
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β ((πΉ + πΊ)βπ) = ((πΉβπ)(+gβπ
)(πΊβπ))) |
26 | | mdegaddle.d |
. . . . . . . 8
β’ π· = (πΌ mDeg π
) |
27 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
28 | | eqid 2733 |
. . . . . . . 8
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) = (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)) |
29 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β πΉ β π΅) |
30 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β π β {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}) |
31 | 26, 1, 2 | mdegxrcl 25455 |
. . . . . . . . . . . . 13
β’ (πΉ β π΅ β (π·βπΉ) β
β*) |
32 | 5, 31 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π·βπΉ) β
β*) |
33 | 32 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π·βπΉ) β
β*) |
34 | 26, 1, 2 | mdegxrcl 25455 |
. . . . . . . . . . . . . 14
β’ (πΊ β π΅ β (π·βπΊ) β
β*) |
35 | 6, 34 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π·βπΊ) β
β*) |
36 | 35, 32 | ifcld 4536 |
. . . . . . . . . . . 12
β’ (π β if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β
β*) |
37 | 36 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β
β*) |
38 | | nn0ssre 12425 |
. . . . . . . . . . . . 13
β’
β0 β β |
39 | | ressxr 11207 |
. . . . . . . . . . . . 13
β’ β
β β* |
40 | 38, 39 | sstri 3957 |
. . . . . . . . . . . 12
β’
β0 β β* |
41 | 11, 28 | tdeglem1 25443 |
. . . . . . . . . . . . . 14
β’ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)):{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆβ0 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π)):{π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin}βΆβ0) |
43 | 42 | ffvelcdmda 7039 |
. . . . . . . . . . . 12
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β
β0) |
44 | 40, 43 | sselid 3946 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β
β*) |
45 | 33, 37, 44 | 3jca 1129 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π·βπΉ) β β* β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β β* β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β
β*)) |
46 | 45 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β ((π·βπΉ) β β* β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β β* β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β
β*)) |
47 | | xrmax1 13103 |
. . . . . . . . . . . 12
β’ (((π·βπΉ) β β* β§ (π·βπΊ) β β*) β (π·βπΉ) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) |
48 | 32, 35, 47 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π·βπΉ) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) |
49 | 48 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β (π·βπΉ) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) |
50 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ)) |
51 | 49, 50 | jca 513 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β ((π·βπΉ) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) |
52 | | xrlelttr 13084 |
. . . . . . . . 9
β’ (((π·βπΉ) β β* β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β β* β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β β*) β (((π·βπΉ) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ)) β (π·βπΉ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) |
53 | 46, 51, 52 | sylc 65 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β (π·βπΉ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ)) |
54 | 26, 1, 2, 27, 11, 28, 29, 30, 53 | mdeglt 25453 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β (πΉβπ) = (0gβπ
)) |
55 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β πΊ β π΅) |
56 | 35 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β (π·βπΊ) β
β*) |
57 | 56, 37, 44 | 3jca 1129 |
. . . . . . . . . 10
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β ((π·βπΊ) β β* β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β β* β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β
β*)) |
58 | 57 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β ((π·βπΊ) β β* β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β β* β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β
β*)) |
59 | | xrmax2 13104 |
. . . . . . . . . . . 12
β’ (((π·βπΉ) β β* β§ (π·βπΊ) β β*) β (π·βπΊ) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) |
60 | 32, 35, 59 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π·βπΊ) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) |
61 | 60 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β (π·βπΊ) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) |
62 | 61, 50 | jca 513 |
. . . . . . . . 9
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β ((π·βπΊ) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) |
63 | | xrlelttr 13084 |
. . . . . . . . 9
β’ (((π·βπΊ) β β* β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β β* β§ ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β β*) β (((π·βπΊ) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ)) β (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) |
64 | 58, 62, 63 | sylc 65 |
. . . . . . . 8
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β (π·βπΊ) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ)) |
65 | 26, 1, 2, 27, 11, 28, 55, 30, 64 | mdeglt 25453 |
. . . . . . 7
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β (πΊβπ) = (0gβπ
)) |
66 | 54, 65 | oveq12d 7379 |
. . . . . 6
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β ((πΉβπ)(+gβπ
)(πΊβπ)) = ((0gβπ
)(+gβπ
)(0gβπ
))) |
67 | | mdegaddle.r |
. . . . . . . . 9
β’ (π β π
β Ring) |
68 | | ringgrp 19977 |
. . . . . . . . 9
β’ (π
β Ring β π
β Grp) |
69 | 67, 68 | syl 17 |
. . . . . . . 8
β’ (π β π
β Grp) |
70 | 10, 27 | ring0cl 19998 |
. . . . . . . . 9
β’ (π
β Ring β
(0gβπ
)
β (Baseβπ
)) |
71 | 67, 70 | syl 17 |
. . . . . . . 8
β’ (π β (0gβπ
) β (Baseβπ
)) |
72 | 10, 3, 27 | grplid 18788 |
. . . . . . . 8
β’ ((π
β Grp β§
(0gβπ
)
β (Baseβπ
))
β ((0gβπ
)(+gβπ
)(0gβπ
)) = (0gβπ
)) |
73 | 69, 71, 72 | syl2anc 585 |
. . . . . . 7
β’ (π β
((0gβπ
)(+gβπ
)(0gβπ
)) = (0gβπ
)) |
74 | 73 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β ((0gβπ
)(+gβπ
)(0gβπ
)) = (0gβπ
)) |
75 | 66, 74 | eqtrd 2773 |
. . . . 5
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β ((πΉβπ)(+gβπ
)(πΊβπ)) = (0gβπ
)) |
76 | 25, 75 | eqtrd 2773 |
. . . 4
β’ ((π β§ (π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ))) β ((πΉ + πΊ)βπ) = (0gβπ
)) |
77 | 76 | expr 458 |
. . 3
β’ ((π β§ π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin}) β
(if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β ((πΉ + πΊ)βπ) = (0gβπ
))) |
78 | 77 | ralrimiva 3140 |
. 2
β’ (π β βπ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β ((πΉ + πΊ)βπ) = (0gβπ
))) |
79 | | mdegaddle.i |
. . . . 5
β’ (π β πΌ β π) |
80 | 1 | mplring 21447 |
. . . . 5
β’ ((πΌ β π β§ π
β Ring) β π β Ring) |
81 | 79, 67, 80 | syl2anc 585 |
. . . 4
β’ (π β π β Ring) |
82 | 2, 4 | ringacl 20007 |
. . . 4
β’ ((π β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (πΉ + πΊ) β π΅) |
83 | 81, 5, 6, 82 | syl3anc 1372 |
. . 3
β’ (π β (πΉ + πΊ) β π΅) |
84 | 26, 1, 2, 27, 11, 28 | mdegleb 25452 |
. . 3
β’ (((πΉ + πΊ) β π΅ β§ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β β*) β
((π·β(πΉ + πΊ)) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β βπ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β ((πΉ + πΊ)βπ) = (0gβπ
)))) |
85 | 83, 36, 84 | syl2anc 585 |
. 2
β’ (π β ((π·β(πΉ + πΊ)) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) β βπ β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} (if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ)) < ((π β {π β (β0
βm πΌ)
β£ (β‘π β β) β Fin} β¦
(βfld Ξ£g π))βπ) β ((πΉ + πΊ)βπ) = (0gβπ
)))) |
86 | 78, 85 | mpbird 257 |
1
β’ (π β (π·β(πΉ + πΊ)) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) |