Step | Hyp | Ref
| Expression |
1 | | omndadd2d.m |
. . 3
β’ (π β π β oMnd) |
2 | | omndtos 31962 |
. . 3
β’ (π β oMnd β π β Toset) |
3 | | tospos 18314 |
. . 3
β’ (π β Toset β π β Poset) |
4 | 1, 2, 3 | 3syl 18 |
. 2
β’ (π β π β Poset) |
5 | | omndmnd 31961 |
. . . . 5
β’ (π β oMnd β π β Mnd) |
6 | 1, 5 | syl 17 |
. . . 4
β’ (π β π β Mnd) |
7 | | omndadd2d.x |
. . . 4
β’ (π β π β π΅) |
8 | | omndadd2d.y |
. . . 4
β’ (π β π β π΅) |
9 | | omndadd.0 |
. . . . 5
β’ π΅ = (Baseβπ) |
10 | | omndadd.2 |
. . . . 5
β’ + =
(+gβπ) |
11 | 9, 10 | mndcl 18569 |
. . . 4
β’ ((π β Mnd β§ π β π΅ β§ π β π΅) β (π + π) β π΅) |
12 | 6, 7, 8, 11 | syl3anc 1372 |
. . 3
β’ (π β (π + π) β π΅) |
13 | | omndadd2d.z |
. . . 4
β’ (π β π β π΅) |
14 | 9, 10 | mndcl 18569 |
. . . 4
β’ ((π β Mnd β§ π β π΅ β§ π β π΅) β (π + π) β π΅) |
15 | 6, 13, 8, 14 | syl3anc 1372 |
. . 3
β’ (π β (π + π) β π΅) |
16 | | omndadd2d.w |
. . . 4
β’ (π β π β π΅) |
17 | 9, 10 | mndcl 18569 |
. . . 4
β’ ((π β Mnd β§ π β π΅ β§ π β π΅) β (π + π) β π΅) |
18 | 6, 13, 16, 17 | syl3anc 1372 |
. . 3
β’ (π β (π + π) β π΅) |
19 | 12, 15, 18 | 3jca 1129 |
. 2
β’ (π β ((π + π) β π΅ β§ (π + π) β π΅ β§ (π + π) β π΅)) |
20 | | omndadd2d.1 |
. . 3
β’ (π β π β€ π) |
21 | | omndadd.1 |
. . . 4
β’ β€ =
(leβπ) |
22 | 9, 21, 10 | omndadd 31963 |
. . 3
β’ ((π β oMnd β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π + π) β€ (π + π)) |
23 | 1, 7, 13, 8, 20, 22 | syl131anc 1384 |
. 2
β’ (π β (π + π) β€ (π + π)) |
24 | | omndadd2d.2 |
. . . 4
β’ (π β π β€ π) |
25 | 9, 21, 10 | omndadd 31963 |
. . . 4
β’ ((π β oMnd β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π + π) β€ (π + π)) |
26 | 1, 8, 16, 13, 24, 25 | syl131anc 1384 |
. . 3
β’ (π β (π + π) β€ (π + π)) |
27 | | omndadd2d.c |
. . . 4
β’ (π β π β CMnd) |
28 | 9, 10 | cmncom 19585 |
. . . 4
β’ ((π β CMnd β§ π β π΅ β§ π β π΅) β (π + π) = (π + π)) |
29 | 27, 8, 13, 28 | syl3anc 1372 |
. . 3
β’ (π β (π + π) = (π + π)) |
30 | 9, 10 | cmncom 19585 |
. . . 4
β’ ((π β CMnd β§ π β π΅ β§ π β π΅) β (π + π) = (π + π)) |
31 | 27, 16, 13, 30 | syl3anc 1372 |
. . 3
β’ (π β (π + π) = (π + π)) |
32 | 26, 29, 31 | 3brtr3d 5137 |
. 2
β’ (π β (π + π) β€ (π + π)) |
33 | 9, 21 | postr 18214 |
. . 3
β’ ((π β Poset β§ ((π + π) β π΅ β§ (π + π) β π΅ β§ (π + π) β π΅)) β (((π + π) β€ (π + π) β§ (π + π) β€ (π + π)) β (π + π) β€ (π + π))) |
34 | 33 | imp 408 |
. 2
β’ (((π β Poset β§ ((π + π) β π΅ β§ (π + π) β π΅ β§ (π + π) β π΅)) β§ ((π + π) β€ (π + π) β§ (π + π) β€ (π + π))) β (π + π) β€ (π + π)) |
35 | 4, 19, 23, 32, 34 | syl22anc 838 |
1
β’ (π β (π + π) β€ (π + π)) |