| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ltrelsr |
⊢ <R ⊆ ( R × R ) |
| 2 |
1
|
brel |
⊢ ( 0R <R 𝐴 → ( 0R ∈ R ∧ 𝐴 ∈ R ) ) |
| 3 |
2
|
simprd |
⊢ ( 0R <R 𝐴 → 𝐴 ∈ R ) |
| 4 |
1
|
brel |
⊢ ( 0R <R 𝐵 → ( 0R ∈ R ∧ 𝐵 ∈ R ) ) |
| 5 |
4
|
simprd |
⊢ ( 0R <R 𝐵 → 𝐵 ∈ R ) |
| 6 |
3 5
|
anim12i |
⊢ ( ( 0R <R 𝐴 ∧ 0R <R 𝐵 ) → ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ) |
| 7 |
|
df-nr |
⊢ R = ( ( P × P ) / ~R ) |
| 8 |
|
breq2 |
⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( 0R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ↔ 0R <R 𝐴 ) ) |
| 9 |
8
|
anbi1d |
⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( ( 0R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ∧ 0R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ ( 0R <R 𝐴 ∧ 0R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ) |
| 10 |
|
oveq1 |
⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = ( 𝐴 ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) |
| 11 |
10
|
breq2d |
⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( 0R <R ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ 0R <R ( 𝐴 ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ) |
| 12 |
9 11
|
imbi12d |
⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( ( ( 0R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ∧ 0R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) → 0R <R ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ↔ ( ( 0R <R 𝐴 ∧ 0R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) → 0R <R ( 𝐴 ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ) ) |
| 13 |
|
breq2 |
⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( 0R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ 0R <R 𝐵 ) ) |
| 14 |
13
|
anbi2d |
⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( ( 0R <R 𝐴 ∧ 0R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ ( 0R <R 𝐴 ∧ 0R <R 𝐵 ) ) ) |
| 15 |
|
oveq2 |
⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( 𝐴 ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = ( 𝐴 ·R 𝐵 ) ) |
| 16 |
15
|
breq2d |
⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( 0R <R ( 𝐴 ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ 0R <R ( 𝐴 ·R 𝐵 ) ) ) |
| 17 |
14 16
|
imbi12d |
⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( ( ( 0R <R 𝐴 ∧ 0R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) → 0R <R ( 𝐴 ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ↔ ( ( 0R <R 𝐴 ∧ 0R <R 𝐵 ) → 0R <R ( 𝐴 ·R 𝐵 ) ) ) ) |
| 18 |
|
gt0srpr |
⊢ ( 0R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ↔ 𝑦 <P 𝑥 ) |
| 19 |
|
gt0srpr |
⊢ ( 0R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ↔ 𝑤 <P 𝑧 ) |
| 20 |
18 19
|
anbi12i |
⊢ ( ( 0R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ∧ 0R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ ( 𝑦 <P 𝑥 ∧ 𝑤 <P 𝑧 ) ) |
| 21 |
|
simprr |
⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → 𝑤 ∈ P ) |
| 22 |
|
mulclpr |
⊢ ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑥 ·P 𝑧 ) ∈ P ) |
| 23 |
|
mulclpr |
⊢ ( ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑦 ·P 𝑤 ) ∈ P ) |
| 24 |
|
addclpr |
⊢ ( ( ( 𝑥 ·P 𝑧 ) ∈ P ∧ ( 𝑦 ·P 𝑤 ) ∈ P ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) |
| 25 |
22 23 24
|
syl2an |
⊢ ( ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) |
| 26 |
25
|
an4s |
⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) |
| 27 |
|
ltexpri |
⊢ ( 𝑦 <P 𝑥 → ∃ 𝑣 ∈ P ( 𝑦 +P 𝑣 ) = 𝑥 ) |
| 28 |
|
ltexpri |
⊢ ( 𝑤 <P 𝑧 → ∃ 𝑢 ∈ P ( 𝑤 +P 𝑢 ) = 𝑧 ) |
| 29 |
|
mulclpr |
⊢ ( ( 𝑣 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑣 ·P 𝑤 ) ∈ P ) |
| 30 |
|
oveq12 |
⊢ ( ( ( 𝑦 +P 𝑣 ) = 𝑥 ∧ ( 𝑤 +P 𝑢 ) = 𝑧 ) → ( ( 𝑦 +P 𝑣 ) ·P ( 𝑤 +P 𝑢 ) ) = ( 𝑥 ·P 𝑧 ) ) |
| 31 |
30
|
oveq1d |
⊢ ( ( ( 𝑦 +P 𝑣 ) = 𝑥 ∧ ( 𝑤 +P 𝑢 ) = 𝑧 ) → ( ( ( 𝑦 +P 𝑣 ) ·P ( 𝑤 +P 𝑢 ) ) +P ( ( 𝑦 ·P 𝑤 ) +P ( 𝑣 ·P 𝑤 ) ) ) = ( ( 𝑥 ·P 𝑧 ) +P ( ( 𝑦 ·P 𝑤 ) +P ( 𝑣 ·P 𝑤 ) ) ) ) |
| 32 |
|
distrpr |
⊢ ( 𝑦 ·P ( 𝑤 +P 𝑢 ) ) = ( ( 𝑦 ·P 𝑤 ) +P ( 𝑦 ·P 𝑢 ) ) |
| 33 |
|
oveq2 |
⊢ ( ( 𝑤 +P 𝑢 ) = 𝑧 → ( 𝑦 ·P ( 𝑤 +P 𝑢 ) ) = ( 𝑦 ·P 𝑧 ) ) |
| 34 |
32 33
|
eqtr3id |
⊢ ( ( 𝑤 +P 𝑢 ) = 𝑧 → ( ( 𝑦 ·P 𝑤 ) +P ( 𝑦 ·P 𝑢 ) ) = ( 𝑦 ·P 𝑧 ) ) |
| 35 |
34
|
oveq1d |
⊢ ( ( 𝑤 +P 𝑢 ) = 𝑧 → ( ( ( 𝑦 ·P 𝑤 ) +P ( 𝑦 ·P 𝑢 ) ) +P ( ( 𝑣 ·P 𝑤 ) +P ( 𝑣 ·P 𝑢 ) ) ) = ( ( 𝑦 ·P 𝑧 ) +P ( ( 𝑣 ·P 𝑤 ) +P ( 𝑣 ·P 𝑢 ) ) ) ) |
| 36 |
|
vex |
⊢ 𝑦 ∈ V |
| 37 |
|
vex |
⊢ 𝑣 ∈ V |
| 38 |
|
vex |
⊢ 𝑤 ∈ V |
| 39 |
|
mulcompr |
⊢ ( 𝑓 ·P 𝑔 ) = ( 𝑔 ·P 𝑓 ) |
| 40 |
|
distrpr |
⊢ ( 𝑓 ·P ( 𝑔 +P ℎ ) ) = ( ( 𝑓 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) ) |
| 41 |
36 37 38 39 40
|
caovdir |
⊢ ( ( 𝑦 +P 𝑣 ) ·P 𝑤 ) = ( ( 𝑦 ·P 𝑤 ) +P ( 𝑣 ·P 𝑤 ) ) |
| 42 |
|
vex |
⊢ 𝑢 ∈ V |
| 43 |
36 37 42 39 40
|
caovdir |
⊢ ( ( 𝑦 +P 𝑣 ) ·P 𝑢 ) = ( ( 𝑦 ·P 𝑢 ) +P ( 𝑣 ·P 𝑢 ) ) |
| 44 |
41 43
|
oveq12i |
⊢ ( ( ( 𝑦 +P 𝑣 ) ·P 𝑤 ) +P ( ( 𝑦 +P 𝑣 ) ·P 𝑢 ) ) = ( ( ( 𝑦 ·P 𝑤 ) +P ( 𝑣 ·P 𝑤 ) ) +P ( ( 𝑦 ·P 𝑢 ) +P ( 𝑣 ·P 𝑢 ) ) ) |
| 45 |
|
distrpr |
⊢ ( ( 𝑦 +P 𝑣 ) ·P ( 𝑤 +P 𝑢 ) ) = ( ( ( 𝑦 +P 𝑣 ) ·P 𝑤 ) +P ( ( 𝑦 +P 𝑣 ) ·P 𝑢 ) ) |
| 46 |
|
ovex |
⊢ ( 𝑦 ·P 𝑤 ) ∈ V |
| 47 |
|
ovex |
⊢ ( 𝑦 ·P 𝑢 ) ∈ V |
| 48 |
|
ovex |
⊢ ( 𝑣 ·P 𝑤 ) ∈ V |
| 49 |
|
addcompr |
⊢ ( 𝑓 +P 𝑔 ) = ( 𝑔 +P 𝑓 ) |
| 50 |
|
addasspr |
⊢ ( ( 𝑓 +P 𝑔 ) +P ℎ ) = ( 𝑓 +P ( 𝑔 +P ℎ ) ) |
| 51 |
|
ovex |
⊢ ( 𝑣 ·P 𝑢 ) ∈ V |
| 52 |
46 47 48 49 50 51
|
caov4 |
⊢ ( ( ( 𝑦 ·P 𝑤 ) +P ( 𝑦 ·P 𝑢 ) ) +P ( ( 𝑣 ·P 𝑤 ) +P ( 𝑣 ·P 𝑢 ) ) ) = ( ( ( 𝑦 ·P 𝑤 ) +P ( 𝑣 ·P 𝑤 ) ) +P ( ( 𝑦 ·P 𝑢 ) +P ( 𝑣 ·P 𝑢 ) ) ) |
| 53 |
44 45 52
|
3eqtr4i |
⊢ ( ( 𝑦 +P 𝑣 ) ·P ( 𝑤 +P 𝑢 ) ) = ( ( ( 𝑦 ·P 𝑤 ) +P ( 𝑦 ·P 𝑢 ) ) +P ( ( 𝑣 ·P 𝑤 ) +P ( 𝑣 ·P 𝑢 ) ) ) |
| 54 |
|
ovex |
⊢ ( 𝑦 ·P 𝑧 ) ∈ V |
| 55 |
48 54 51 49 50
|
caov12 |
⊢ ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) = ( ( 𝑦 ·P 𝑧 ) +P ( ( 𝑣 ·P 𝑤 ) +P ( 𝑣 ·P 𝑢 ) ) ) |
| 56 |
35 53 55
|
3eqtr4g |
⊢ ( ( 𝑤 +P 𝑢 ) = 𝑧 → ( ( 𝑦 +P 𝑣 ) ·P ( 𝑤 +P 𝑢 ) ) = ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) ) |
| 57 |
|
oveq1 |
⊢ ( ( 𝑦 +P 𝑣 ) = 𝑥 → ( ( 𝑦 +P 𝑣 ) ·P 𝑤 ) = ( 𝑥 ·P 𝑤 ) ) |
| 58 |
41 57
|
eqtr3id |
⊢ ( ( 𝑦 +P 𝑣 ) = 𝑥 → ( ( 𝑦 ·P 𝑤 ) +P ( 𝑣 ·P 𝑤 ) ) = ( 𝑥 ·P 𝑤 ) ) |
| 59 |
56 58
|
oveqan12rd |
⊢ ( ( ( 𝑦 +P 𝑣 ) = 𝑥 ∧ ( 𝑤 +P 𝑢 ) = 𝑧 ) → ( ( ( 𝑦 +P 𝑣 ) ·P ( 𝑤 +P 𝑢 ) ) +P ( ( 𝑦 ·P 𝑤 ) +P ( 𝑣 ·P 𝑤 ) ) ) = ( ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) +P ( 𝑥 ·P 𝑤 ) ) ) |
| 60 |
31 59
|
eqtr3d |
⊢ ( ( ( 𝑦 +P 𝑣 ) = 𝑥 ∧ ( 𝑤 +P 𝑢 ) = 𝑧 ) → ( ( 𝑥 ·P 𝑧 ) +P ( ( 𝑦 ·P 𝑤 ) +P ( 𝑣 ·P 𝑤 ) ) ) = ( ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) +P ( 𝑥 ·P 𝑤 ) ) ) |
| 61 |
|
addasspr |
⊢ ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) +P ( 𝑣 ·P 𝑤 ) ) = ( ( 𝑥 ·P 𝑧 ) +P ( ( 𝑦 ·P 𝑤 ) +P ( 𝑣 ·P 𝑤 ) ) ) |
| 62 |
|
addcompr |
⊢ ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) +P ( 𝑣 ·P 𝑤 ) ) = ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) |
| 63 |
61 62
|
eqtr3i |
⊢ ( ( 𝑥 ·P 𝑧 ) +P ( ( 𝑦 ·P 𝑤 ) +P ( 𝑣 ·P 𝑤 ) ) ) = ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) |
| 64 |
|
addasspr |
⊢ ( ( ( 𝑣 ·P 𝑤 ) +P ( 𝑥 ·P 𝑤 ) ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) = ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑥 ·P 𝑤 ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) ) |
| 65 |
|
ovex |
⊢ ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ∈ V |
| 66 |
|
ovex |
⊢ ( 𝑥 ·P 𝑤 ) ∈ V |
| 67 |
48 65 66 49 50
|
caov32 |
⊢ ( ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) +P ( 𝑥 ·P 𝑤 ) ) = ( ( ( 𝑣 ·P 𝑤 ) +P ( 𝑥 ·P 𝑤 ) ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) |
| 68 |
|
addasspr |
⊢ ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) = ( ( 𝑥 ·P 𝑤 ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) |
| 69 |
68
|
oveq2i |
⊢ ( ( 𝑣 ·P 𝑤 ) +P ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) ) = ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑥 ·P 𝑤 ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) ) |
| 70 |
64 67 69
|
3eqtr4i |
⊢ ( ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑦 ·P 𝑧 ) +P ( 𝑣 ·P 𝑢 ) ) ) +P ( 𝑥 ·P 𝑤 ) ) = ( ( 𝑣 ·P 𝑤 ) +P ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) ) |
| 71 |
60 63 70
|
3eqtr3g |
⊢ ( ( ( 𝑦 +P 𝑣 ) = 𝑥 ∧ ( 𝑤 +P 𝑢 ) = 𝑧 ) → ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) = ( ( 𝑣 ·P 𝑤 ) +P ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) ) ) |
| 72 |
|
addcanpr |
⊢ ( ( ( 𝑣 ·P 𝑤 ) ∈ P ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ( ( 𝑣 ·P 𝑤 ) +P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) = ( ( 𝑣 ·P 𝑤 ) +P ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) = ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) ) ) |
| 73 |
71 72
|
syl5 |
⊢ ( ( ( 𝑣 ·P 𝑤 ) ∈ P ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ( ( 𝑦 +P 𝑣 ) = 𝑥 ∧ ( 𝑤 +P 𝑢 ) = 𝑧 ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) = ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) ) ) |
| 74 |
|
eqcom |
⊢ ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) = ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) ↔ ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) = ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) |
| 75 |
|
ltaddpr2 |
⊢ ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P → ( ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) = ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) |
| 76 |
74 75
|
biimtrid |
⊢ ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P → ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) = ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) |
| 77 |
76
|
adantl |
⊢ ( ( ( 𝑣 ·P 𝑤 ) ∈ P ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) = ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) +P ( 𝑣 ·P 𝑢 ) ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) |
| 78 |
73 77
|
syld |
⊢ ( ( ( 𝑣 ·P 𝑤 ) ∈ P ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ( ( 𝑦 +P 𝑣 ) = 𝑥 ∧ ( 𝑤 +P 𝑢 ) = 𝑧 ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) |
| 79 |
29 78
|
sylan |
⊢ ( ( ( 𝑣 ∈ P ∧ 𝑤 ∈ P ) ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ( ( 𝑦 +P 𝑣 ) = 𝑥 ∧ ( 𝑤 +P 𝑢 ) = 𝑧 ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) |
| 80 |
79
|
a1d |
⊢ ( ( ( 𝑣 ∈ P ∧ 𝑤 ∈ P ) ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( 𝑢 ∈ P → ( ( ( 𝑦 +P 𝑣 ) = 𝑥 ∧ ( 𝑤 +P 𝑢 ) = 𝑧 ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) ) |
| 81 |
80
|
exp4a |
⊢ ( ( ( 𝑣 ∈ P ∧ 𝑤 ∈ P ) ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( 𝑢 ∈ P → ( ( 𝑦 +P 𝑣 ) = 𝑥 → ( ( 𝑤 +P 𝑢 ) = 𝑧 → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) ) ) |
| 82 |
81
|
com34 |
⊢ ( ( ( 𝑣 ∈ P ∧ 𝑤 ∈ P ) ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( 𝑢 ∈ P → ( ( 𝑤 +P 𝑢 ) = 𝑧 → ( ( 𝑦 +P 𝑣 ) = 𝑥 → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) ) ) |
| 83 |
82
|
rexlimdv |
⊢ ( ( ( 𝑣 ∈ P ∧ 𝑤 ∈ P ) ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ∃ 𝑢 ∈ P ( 𝑤 +P 𝑢 ) = 𝑧 → ( ( 𝑦 +P 𝑣 ) = 𝑥 → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) ) |
| 84 |
83
|
expl |
⊢ ( 𝑣 ∈ P → ( ( 𝑤 ∈ P ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ∃ 𝑢 ∈ P ( 𝑤 +P 𝑢 ) = 𝑧 → ( ( 𝑦 +P 𝑣 ) = 𝑥 → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) ) ) |
| 85 |
84
|
com24 |
⊢ ( 𝑣 ∈ P → ( ( 𝑦 +P 𝑣 ) = 𝑥 → ( ∃ 𝑢 ∈ P ( 𝑤 +P 𝑢 ) = 𝑧 → ( ( 𝑤 ∈ P ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) ) ) |
| 86 |
85
|
rexlimiv |
⊢ ( ∃ 𝑣 ∈ P ( 𝑦 +P 𝑣 ) = 𝑥 → ( ∃ 𝑢 ∈ P ( 𝑤 +P 𝑢 ) = 𝑧 → ( ( 𝑤 ∈ P ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) ) |
| 87 |
27 28 86
|
syl2im |
⊢ ( 𝑦 <P 𝑥 → ( 𝑤 <P 𝑧 → ( ( 𝑤 ∈ P ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) ) |
| 88 |
87
|
imp |
⊢ ( ( 𝑦 <P 𝑥 ∧ 𝑤 <P 𝑧 ) → ( ( 𝑤 ∈ P ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) |
| 89 |
88
|
com12 |
⊢ ( ( 𝑤 ∈ P ∧ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ) → ( ( 𝑦 <P 𝑥 ∧ 𝑤 <P 𝑧 ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) |
| 90 |
21 26 89
|
syl2anc |
⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑦 <P 𝑥 ∧ 𝑤 <P 𝑧 ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) |
| 91 |
|
mulsrpr |
⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R ) |
| 92 |
91
|
breq2d |
⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( 0R <R ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ 0R <R [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R ) ) |
| 93 |
|
gt0srpr |
⊢ ( 0R <R [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R ↔ ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) |
| 94 |
92 93
|
bitrdi |
⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( 0R <R ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ↔ ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) <P ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ) ) |
| 95 |
90 94
|
sylibrd |
⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑦 <P 𝑥 ∧ 𝑤 <P 𝑧 ) → 0R <R ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ) |
| 96 |
20 95
|
biimtrid |
⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 0R <R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ∧ 0R <R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) → 0R <R ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ) ) |
| 97 |
7 12 17 96
|
2ecoptocl |
⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ( 0R <R 𝐴 ∧ 0R <R 𝐵 ) → 0R <R ( 𝐴 ·R 𝐵 ) ) ) |
| 98 |
6 97
|
mpcom |
⊢ ( ( 0R <R 𝐴 ∧ 0R <R 𝐵 ) → 0R <R ( 𝐴 ·R 𝐵 ) ) |