Proof of Theorem omndadd2d
Step | Hyp | Ref
| Expression |
1 | | omndadd2d.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ oMnd) |
2 | | omndtos 31310 |
. . 3
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) |
3 | | tospos 18119 |
. . 3
⊢ (𝑀 ∈ Toset → 𝑀 ∈ Poset) |
4 | 1, 2, 3 | 3syl 18 |
. 2
⊢ (𝜑 → 𝑀 ∈ Poset) |
5 | | omndmnd 31309 |
. . . . 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 18374 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
12 | 6, 7, 8, 11 | syl3anc 1369 |
. . 3
⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) |
13 | | omndadd2d.z |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
14 | 9, 10 | mndcl 18374 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑍 + 𝑌) ∈ 𝐵) |
15 | 6, 13, 8, 14 | syl3anc 1369 |
. . 3
⊢ (𝜑 → (𝑍 + 𝑌) ∈ 𝐵) |
16 | | omndadd2d.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ 𝐵) |
17 | 9, 10 | mndcl 18374 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑍 + 𝑊) ∈ 𝐵) |
18 | 6, 13, 16, 17 | syl3anc 1369 |
. . 3
⊢ (𝜑 → (𝑍 + 𝑊) ∈ 𝐵) |
19 | 12, 15, 18 | 3jca 1126 |
. 2
⊢ (𝜑 → ((𝑋 + 𝑌) ∈ 𝐵 ∧ (𝑍 + 𝑌) ∈ 𝐵 ∧ (𝑍 + 𝑊) ∈ 𝐵)) |
20 | | omndadd2d.1 |
. . 3
⊢ (𝜑 → 𝑋 ≤ 𝑍) |
21 | | omndadd.1 |
. . . 4
⊢ ≤ =
(le‘𝑀) |
22 | 9, 21, 10 | omndadd 31311 |
. . 3
⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑍) → (𝑋 + 𝑌) ≤ (𝑍 + 𝑌)) |
23 | 1, 7, 13, 8, 20, 22 | syl131anc 1381 |
. 2
⊢ (𝜑 → (𝑋 + 𝑌) ≤ (𝑍 + 𝑌)) |
24 | | omndadd2d.2 |
. . . 4
⊢ (𝜑 → 𝑌 ≤ 𝑊) |
25 | 9, 21, 10 | omndadd 31311 |
. . . 4
⊢ ((𝑀 ∈ oMnd ∧ (𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑌 ≤ 𝑊) → (𝑌 + 𝑍) ≤ (𝑊 + 𝑍)) |
26 | 1, 8, 16, 13, 24, 25 | syl131anc 1381 |
. . 3
⊢ (𝜑 → (𝑌 + 𝑍) ≤ (𝑊 + 𝑍)) |
27 | | omndadd2d.c |
. . . 4
⊢ (𝜑 → 𝑀 ∈ CMnd) |
28 | 9, 10 | cmncom 19384 |
. . . 4
⊢ ((𝑀 ∈ CMnd ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) = (𝑍 + 𝑌)) |
29 | 27, 8, 13, 28 | syl3anc 1369 |
. . 3
⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌)) |
30 | 9, 10 | cmncom 19384 |
. . . 4
⊢ ((𝑀 ∈ CMnd ∧ 𝑊 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑊 + 𝑍) = (𝑍 + 𝑊)) |
31 | 27, 16, 13, 30 | syl3anc 1369 |
. . 3
⊢ (𝜑 → (𝑊 + 𝑍) = (𝑍 + 𝑊)) |
32 | 26, 29, 31 | 3brtr3d 5109 |
. 2
⊢ (𝜑 → (𝑍 + 𝑌) ≤ (𝑍 + 𝑊)) |
33 | 9, 21 | postr 18019 |
. . 3
⊢ ((𝑀 ∈ Poset ∧ ((𝑋 + 𝑌) ∈ 𝐵 ∧ (𝑍 + 𝑌) ∈ 𝐵 ∧ (𝑍 + 𝑊) ∈ 𝐵)) → (((𝑋 + 𝑌) ≤ (𝑍 + 𝑌) ∧ (𝑍 + 𝑌) ≤ (𝑍 + 𝑊)) → (𝑋 + 𝑌) ≤ (𝑍 + 𝑊))) |
34 | 33 | imp 406 |
. 2
⊢ (((𝑀 ∈ Poset ∧ ((𝑋 + 𝑌) ∈ 𝐵 ∧ (𝑍 + 𝑌) ∈ 𝐵 ∧ (𝑍 + 𝑊) ∈ 𝐵)) ∧ ((𝑋 + 𝑌) ≤ (𝑍 + 𝑌) ∧ (𝑍 + 𝑌) ≤ (𝑍 + 𝑊))) → (𝑋 + 𝑌) ≤ (𝑍 + 𝑊)) |
35 | 4, 19, 23, 32, 34 | syl22anc 835 |
1
⊢ (𝜑 → (𝑋 + 𝑌) ≤ (𝑍 + 𝑊)) |