| Step | Hyp | Ref
| Expression |
| 1 | | dmaddsr 11125 |
. 2
⊢ dom
+R = (R ×
R) |
| 2 | | ltrelsr 11108 |
. 2
⊢
<R ⊆ (R ×
R) |
| 3 | | 0nsr 11119 |
. 2
⊢ ¬
∅ ∈ R |
| 4 | | df-nr 11096 |
. . . 4
⊢
R = ((P × P) /
~R ) |
| 5 | | oveq1 7438 |
. . . . . 6
⊢
([〈𝑣, 𝑢〉]
~R = 𝐶 → ([〈𝑣, 𝑢〉] ~R
+R [〈𝑥, 𝑦〉] ~R ) =
(𝐶
+R [〈𝑥, 𝑦〉] ~R
)) |
| 6 | | oveq1 7438 |
. . . . . 6
⊢
([〈𝑣, 𝑢〉]
~R = 𝐶 → ([〈𝑣, 𝑢〉] ~R
+R [〈𝑧, 𝑤〉] ~R ) =
(𝐶
+R [〈𝑧, 𝑤〉] ~R
)) |
| 7 | 5, 6 | breq12d 5156 |
. . . . 5
⊢
([〈𝑣, 𝑢〉]
~R = 𝐶 → (([〈𝑣, 𝑢〉] ~R
+R [〈𝑥, 𝑦〉] ~R )
<R ([〈𝑣, 𝑢〉] ~R
+R [〈𝑧, 𝑤〉] ~R ) ↔
(𝐶
+R [〈𝑥, 𝑦〉] ~R )
<R (𝐶 +R [〈𝑧, 𝑤〉] ~R
))) |
| 8 | 7 | bibi2d 342 |
. . . 4
⊢
([〈𝑣, 𝑢〉]
~R = 𝐶 → (([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
([〈𝑣, 𝑢〉]
~R +R [〈𝑥, 𝑦〉] ~R )
<R ([〈𝑣, 𝑢〉] ~R
+R [〈𝑧, 𝑤〉] ~R )) ↔
([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ↔
(𝐶
+R [〈𝑥, 𝑦〉] ~R )
<R (𝐶 +R [〈𝑧, 𝑤〉] ~R
)))) |
| 9 | | breq1 5146 |
. . . . 5
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → ([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
𝐴
<R [〈𝑧, 𝑤〉] ~R
)) |
| 10 | | oveq2 7439 |
. . . . . 6
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → (𝐶 +R [〈𝑥, 𝑦〉] ~R ) =
(𝐶
+R 𝐴)) |
| 11 | 10 | breq1d 5153 |
. . . . 5
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → ((𝐶 +R [〈𝑥, 𝑦〉] ~R )
<R (𝐶 +R [〈𝑧, 𝑤〉] ~R ) ↔
(𝐶
+R 𝐴) <R (𝐶 +R
[〈𝑧, 𝑤〉]
~R ))) |
| 12 | 9, 11 | bibi12d 345 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → (([〈𝑥, 𝑦〉] ~R
<R [〈𝑧, 𝑤〉] ~R ↔
(𝐶
+R [〈𝑥, 𝑦〉] ~R )
<R (𝐶 +R [〈𝑧, 𝑤〉] ~R )) ↔
(𝐴
<R [〈𝑧, 𝑤〉] ~R ↔
(𝐶
+R 𝐴) <R (𝐶 +R
[〈𝑧, 𝑤〉]
~R )))) |
| 13 | | breq2 5147 |
. . . . 5
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → (𝐴 <R [〈𝑧, 𝑤〉] ~R ↔
𝐴
<R 𝐵)) |
| 14 | | oveq2 7439 |
. . . . . 6
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → (𝐶 +R [〈𝑧, 𝑤〉] ~R ) =
(𝐶
+R 𝐵)) |
| 15 | 14 | breq2d 5155 |
. . . . 5
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → ((𝐶 +R 𝐴) <R
(𝐶
+R [〈𝑧, 𝑤〉] ~R ) ↔
(𝐶
+R 𝐴) <R (𝐶 +R
𝐵))) |
| 16 | 13, 15 | bibi12d 345 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → ((𝐴 <R [〈𝑧, 𝑤〉] ~R ↔
(𝐶
+R 𝐴) <R (𝐶 +R
[〈𝑧, 𝑤〉]
~R )) ↔ (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R
(𝐶
+R 𝐵)))) |
| 17 | | addclpr 11058 |
. . . . . . 7
⊢ ((𝑣 ∈ P ∧
𝑢 ∈ P)
→ (𝑣
+P 𝑢) ∈ P) |
| 18 | 17 | 3ad2ant1 1134 |
. . . . . 6
⊢ (((𝑣 ∈ P ∧
𝑢 ∈ P)
∧ (𝑥 ∈
P ∧ 𝑦
∈ P) ∧ (𝑧 ∈ P ∧ 𝑤 ∈ P)) →
(𝑣
+P 𝑢) ∈ P) |
| 19 | | ltapr 11085 |
. . . . . . 7
⊢ ((𝑣 +P
𝑢) ∈ P
→ ((𝑥
+P 𝑤)<P (𝑦 +P
𝑧) ↔ ((𝑣 +P
𝑢)
+P (𝑥 +P 𝑤))<P
((𝑣
+P 𝑢) +P (𝑦 +P
𝑧)))) |
| 20 | | ltsrpr 11117 |
. . . . . . 7
⊢
([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ↔
(𝑥
+P 𝑤)<P (𝑦 +P
𝑧)) |
| 21 | | ltsrpr 11117 |
. . . . . . . 8
⊢
([〈(𝑣
+P 𝑥), (𝑢 +P 𝑦)〉]
~R <R [〈(𝑣 +P
𝑧), (𝑢 +P 𝑤)〉]
~R ↔ ((𝑣 +P 𝑥) +P
(𝑢
+P 𝑤))<P ((𝑢 +P
𝑦)
+P (𝑣 +P 𝑧))) |
| 22 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑣 ∈ V |
| 23 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 24 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
| 25 | | addcompr 11061 |
. . . . . . . . . 10
⊢ (𝑦 +P
𝑧) = (𝑧 +P 𝑦) |
| 26 | | addasspr 11062 |
. . . . . . . . . 10
⊢ ((𝑦 +P
𝑧)
+P 𝑓) = (𝑦 +P (𝑧 +P
𝑓)) |
| 27 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑤 ∈ V |
| 28 | 22, 23, 24, 25, 26, 27 | caov4 7664 |
. . . . . . . . 9
⊢ ((𝑣 +P
𝑥)
+P (𝑢 +P 𝑤)) = ((𝑣 +P 𝑢) +P
(𝑥
+P 𝑤)) |
| 29 | | addcompr 11061 |
. . . . . . . . . 10
⊢ ((𝑢 +P
𝑦)
+P (𝑣 +P 𝑧)) = ((𝑣 +P 𝑧) +P
(𝑢
+P 𝑦)) |
| 30 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
| 31 | | addcompr 11061 |
. . . . . . . . . . 11
⊢ (𝑥 +P
𝑤) = (𝑤 +P 𝑥) |
| 32 | | addasspr 11062 |
. . . . . . . . . . 11
⊢ ((𝑥 +P
𝑤)
+P 𝑓) = (𝑥 +P (𝑤 +P
𝑓)) |
| 33 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
| 34 | 22, 30, 24, 31, 32, 33 | caov42 7666 |
. . . . . . . . . 10
⊢ ((𝑣 +P
𝑧)
+P (𝑢 +P 𝑦)) = ((𝑣 +P 𝑢) +P
(𝑦
+P 𝑧)) |
| 35 | 29, 34 | eqtri 2765 |
. . . . . . . . 9
⊢ ((𝑢 +P
𝑦)
+P (𝑣 +P 𝑧)) = ((𝑣 +P 𝑢) +P
(𝑦
+P 𝑧)) |
| 36 | 28, 35 | breq12i 5152 |
. . . . . . . 8
⊢ (((𝑣 +P
𝑥)
+P (𝑢 +P 𝑤))<P
((𝑢
+P 𝑦) +P (𝑣 +P
𝑧)) ↔ ((𝑣 +P
𝑢)
+P (𝑥 +P 𝑤))<P
((𝑣
+P 𝑢) +P (𝑦 +P
𝑧))) |
| 37 | 21, 36 | bitri 275 |
. . . . . . 7
⊢
([〈(𝑣
+P 𝑥), (𝑢 +P 𝑦)〉]
~R <R [〈(𝑣 +P
𝑧), (𝑢 +P 𝑤)〉]
~R ↔ ((𝑣 +P 𝑢) +P
(𝑥
+P 𝑤))<P ((𝑣 +P
𝑢)
+P (𝑦 +P 𝑧))) |
| 38 | 19, 20, 37 | 3bitr4g 314 |
. . . . . 6
⊢ ((𝑣 +P
𝑢) ∈ P
→ ([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ↔
[〈(𝑣
+P 𝑥), (𝑢 +P 𝑦)〉]
~R <R [〈(𝑣 +P
𝑧), (𝑢 +P 𝑤)〉]
~R )) |
| 39 | 18, 38 | syl 17 |
. . . . 5
⊢ (((𝑣 ∈ P ∧
𝑢 ∈ P)
∧ (𝑥 ∈
P ∧ 𝑦
∈ P) ∧ (𝑧 ∈ P ∧ 𝑤 ∈ P)) →
([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ↔
[〈(𝑣
+P 𝑥), (𝑢 +P 𝑦)〉]
~R <R [〈(𝑣 +P
𝑧), (𝑢 +P 𝑤)〉]
~R )) |
| 40 | | addsrpr 11115 |
. . . . . . 7
⊢ (((𝑣 ∈ P ∧
𝑢 ∈ P)
∧ (𝑥 ∈
P ∧ 𝑦
∈ P)) → ([〈𝑣, 𝑢〉] ~R
+R [〈𝑥, 𝑦〉] ~R ) =
[〈(𝑣
+P 𝑥), (𝑢 +P 𝑦)〉]
~R ) |
| 41 | 40 | 3adant3 1133 |
. . . . . 6
⊢ (((𝑣 ∈ P ∧
𝑢 ∈ P)
∧ (𝑥 ∈
P ∧ 𝑦
∈ P) ∧ (𝑧 ∈ P ∧ 𝑤 ∈ P)) →
([〈𝑣, 𝑢〉]
~R +R [〈𝑥, 𝑦〉] ~R ) =
[〈(𝑣
+P 𝑥), (𝑢 +P 𝑦)〉]
~R ) |
| 42 | | addsrpr 11115 |
. . . . . . 7
⊢ (((𝑣 ∈ P ∧
𝑢 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑣, 𝑢〉] ~R
+R [〈𝑧, 𝑤〉] ~R ) =
[〈(𝑣
+P 𝑧), (𝑢 +P 𝑤)〉]
~R ) |
| 43 | 42 | 3adant2 1132 |
. . . . . 6
⊢ (((𝑣 ∈ P ∧
𝑢 ∈ P)
∧ (𝑥 ∈
P ∧ 𝑦
∈ P) ∧ (𝑧 ∈ P ∧ 𝑤 ∈ P)) →
([〈𝑣, 𝑢〉]
~R +R [〈𝑧, 𝑤〉] ~R ) =
[〈(𝑣
+P 𝑧), (𝑢 +P 𝑤)〉]
~R ) |
| 44 | 41, 43 | breq12d 5156 |
. . . . 5
⊢ (((𝑣 ∈ P ∧
𝑢 ∈ P)
∧ (𝑥 ∈
P ∧ 𝑦
∈ P) ∧ (𝑧 ∈ P ∧ 𝑤 ∈ P)) →
(([〈𝑣, 𝑢〉]
~R +R [〈𝑥, 𝑦〉] ~R )
<R ([〈𝑣, 𝑢〉] ~R
+R [〈𝑧, 𝑤〉] ~R ) ↔
[〈(𝑣
+P 𝑥), (𝑢 +P 𝑦)〉]
~R <R [〈(𝑣 +P
𝑧), (𝑢 +P 𝑤)〉]
~R )) |
| 45 | 39, 44 | bitr4d 282 |
. . . 4
⊢ (((𝑣 ∈ P ∧
𝑢 ∈ P)
∧ (𝑥 ∈
P ∧ 𝑦
∈ P) ∧ (𝑧 ∈ P ∧ 𝑤 ∈ P)) →
([〈𝑥, 𝑦〉]
~R <R [〈𝑧, 𝑤〉] ~R ↔
([〈𝑣, 𝑢〉]
~R +R [〈𝑥, 𝑦〉] ~R )
<R ([〈𝑣, 𝑢〉] ~R
+R [〈𝑧, 𝑤〉] ~R
))) |
| 46 | 4, 8, 12, 16, 45 | 3ecoptocl 8849 |
. . 3
⊢ ((𝐶 ∈ R ∧
𝐴 ∈ R
∧ 𝐵 ∈
R) → (𝐴
<R 𝐵 ↔ (𝐶 +R 𝐴) <R
(𝐶
+R 𝐵))) |
| 47 | 46 | 3coml 1128 |
. 2
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R
∧ 𝐶 ∈
R) → (𝐴
<R 𝐵 ↔ (𝐶 +R 𝐴) <R
(𝐶
+R 𝐵))) |
| 48 | 1, 2, 3, 47 | ndmovord 7623 |
1
⊢ (𝐶 ∈ R →
(𝐴
<R 𝐵 ↔ (𝐶 +R 𝐴) <R
(𝐶
+R 𝐵))) |