Step | Hyp | Ref
| Expression |
1 | | ltrelsr 10513 |
. . . . 5
⊢
<R ⊆ (R ×
R) |
2 | 1 | brel 5579 |
. . . 4
⊢
(0R <R 𝐴 →
(0R ∈ R ∧ 𝐴 ∈ R)) |
3 | 2 | simprd 500 |
. . 3
⊢
(0R <R 𝐴 → 𝐴 ∈ R) |
4 | 1 | brel 5579 |
. . . 4
⊢
(0R <R 𝐵 →
(0R ∈ R ∧ 𝐵 ∈ R)) |
5 | 4 | simprd 500 |
. . 3
⊢
(0R <R 𝐵 → 𝐵 ∈ R) |
6 | 3, 5 | anim12i 616 |
. 2
⊢
((0R <R 𝐴 ∧
0R <R 𝐵) → (𝐴 ∈ R ∧ 𝐵 ∈
R)) |
7 | | df-nr 10501 |
. . 3
⊢
R = ((P × P) /
~R ) |
8 | | breq2 5029 |
. . . . 5
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → (0R
<R [〈𝑥, 𝑦〉] ~R ↔
0R <R 𝐴)) |
9 | 8 | anbi1d 633 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → ((0R
<R [〈𝑥, 𝑦〉] ~R ∧
0R <R [〈𝑧, 𝑤〉] ~R ) ↔
(0R <R 𝐴 ∧ 0R
<R [〈𝑧, 𝑤〉] ~R
))) |
10 | | oveq1 7150 |
. . . . 5
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → ([〈𝑥, 𝑦〉] ~R
·R [〈𝑧, 𝑤〉] ~R ) =
(𝐴
·R [〈𝑧, 𝑤〉] ~R
)) |
11 | 10 | breq2d 5037 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → (0R
<R ([〈𝑥, 𝑦〉] ~R
·R [〈𝑧, 𝑤〉] ~R ) ↔
0R <R (𝐴 ·R
[〈𝑧, 𝑤〉]
~R ))) |
12 | 9, 11 | imbi12d 349 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → (((0R
<R [〈𝑥, 𝑦〉] ~R ∧
0R <R [〈𝑧, 𝑤〉] ~R ) →
0R <R ([〈𝑥, 𝑦〉] ~R
·R [〈𝑧, 𝑤〉] ~R )) ↔
((0R <R 𝐴 ∧ 0R
<R [〈𝑧, 𝑤〉] ~R ) →
0R <R (𝐴 ·R
[〈𝑧, 𝑤〉]
~R )))) |
13 | | breq2 5029 |
. . . . 5
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → (0R
<R [〈𝑧, 𝑤〉] ~R ↔
0R <R 𝐵)) |
14 | 13 | anbi2d 632 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → ((0R
<R 𝐴 ∧ 0R
<R [〈𝑧, 𝑤〉] ~R ) ↔
(0R <R 𝐴 ∧ 0R
<R 𝐵))) |
15 | | oveq2 7151 |
. . . . 5
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → (𝐴 ·R
[〈𝑧, 𝑤〉]
~R ) = (𝐴 ·R 𝐵)) |
16 | 15 | breq2d 5037 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → (0R
<R (𝐴 ·R
[〈𝑧, 𝑤〉]
~R ) ↔ 0R
<R (𝐴 ·R 𝐵))) |
17 | 14, 16 | imbi12d 349 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~R = 𝐵 → (((0R
<R 𝐴 ∧ 0R
<R [〈𝑧, 𝑤〉] ~R ) →
0R <R (𝐴 ·R
[〈𝑧, 𝑤〉]
~R )) ↔ ((0R
<R 𝐴 ∧ 0R
<R 𝐵) → 0R
<R (𝐴 ·R 𝐵)))) |
18 | | gt0srpr 10523 |
. . . . 5
⊢
(0R <R [〈𝑥, 𝑦〉] ~R ↔
𝑦<P 𝑥) |
19 | | gt0srpr 10523 |
. . . . 5
⊢
(0R <R [〈𝑧, 𝑤〉] ~R ↔
𝑤<P 𝑧) |
20 | 18, 19 | anbi12i 630 |
. . . 4
⊢
((0R <R
[〈𝑥, 𝑦〉]
~R ∧ 0R
<R [〈𝑧, 𝑤〉] ~R ) ↔
(𝑦<P 𝑥 ∧ 𝑤<P 𝑧)) |
21 | | simprr 773 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → 𝑤 ∈ P) |
22 | | mulclpr 10465 |
. . . . . . . 8
⊢ ((𝑥 ∈ P ∧
𝑧 ∈ P)
→ (𝑥
·P 𝑧) ∈ P) |
23 | | mulclpr 10465 |
. . . . . . . 8
⊢ ((𝑦 ∈ P ∧
𝑤 ∈ P)
→ (𝑦
·P 𝑤) ∈ P) |
24 | | addclpr 10463 |
. . . . . . . 8
⊢ (((𝑥
·P 𝑧) ∈ P ∧ (𝑦
·P 𝑤) ∈ P) → ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) |
25 | 22, 23, 24 | syl2an 599 |
. . . . . . 7
⊢ (((𝑥 ∈ P ∧
𝑧 ∈ P)
∧ (𝑦 ∈
P ∧ 𝑤
∈ P)) → ((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) ∈ P) |
26 | 25 | an4s 660 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) ∈ P) |
27 | | ltexpri 10488 |
. . . . . . . . 9
⊢ (𝑦<P
𝑥 → ∃𝑣 ∈ P (𝑦 +P
𝑣) = 𝑥) |
28 | | ltexpri 10488 |
. . . . . . . . 9
⊢ (𝑤<P
𝑧 → ∃𝑢 ∈ P (𝑤 +P
𝑢) = 𝑧) |
29 | | mulclpr 10465 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ P ∧
𝑤 ∈ P)
→ (𝑣
·P 𝑤) ∈ P) |
30 | | oveq12 7152 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 +P
𝑣) = 𝑥 ∧ (𝑤 +P 𝑢) = 𝑧) → ((𝑦 +P 𝑣)
·P (𝑤 +P 𝑢)) = (𝑥 ·P 𝑧)) |
31 | 30 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 +P
𝑣) = 𝑥 ∧ (𝑤 +P 𝑢) = 𝑧) → (((𝑦 +P 𝑣)
·P (𝑤 +P 𝑢)) +P
((𝑦
·P 𝑤) +P (𝑣
·P 𝑤))) = ((𝑥 ·P 𝑧) +P
((𝑦
·P 𝑤) +P (𝑣
·P 𝑤)))) |
32 | | distrpr 10473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦
·P (𝑤 +P 𝑢)) = ((𝑦 ·P 𝑤) +P
(𝑦
·P 𝑢)) |
33 | | oveq2 7151 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑤 +P
𝑢) = 𝑧 → (𝑦 ·P (𝑤 +P
𝑢)) = (𝑦 ·P 𝑧)) |
34 | 32, 33 | syl5eqr 2808 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑤 +P
𝑢) = 𝑧 → ((𝑦 ·P 𝑤) +P
(𝑦
·P 𝑢)) = (𝑦 ·P 𝑧)) |
35 | 34 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 +P
𝑢) = 𝑧 → (((𝑦 ·P 𝑤) +P
(𝑦
·P 𝑢)) +P ((𝑣
·P 𝑤) +P (𝑣
·P 𝑢))) = ((𝑦 ·P 𝑧) +P
((𝑣
·P 𝑤) +P (𝑣
·P 𝑢)))) |
36 | | vex 3411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑦 ∈ V |
37 | | vex 3411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑣 ∈ V |
38 | | vex 3411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑤 ∈ V |
39 | | mulcompr 10468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓
·P 𝑔) = (𝑔 ·P 𝑓) |
40 | | distrpr 10473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓
·P (𝑔 +P ℎ)) = ((𝑓 ·P 𝑔) +P
(𝑓
·P ℎ)) |
41 | 36, 37, 38, 39, 40 | caovdir 7371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 +P
𝑣)
·P 𝑤) = ((𝑦 ·P 𝑤) +P
(𝑣
·P 𝑤)) |
42 | | vex 3411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑢 ∈ V |
43 | 36, 37, 42, 39, 40 | caovdir 7371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 +P
𝑣)
·P 𝑢) = ((𝑦 ·P 𝑢) +P
(𝑣
·P 𝑢)) |
44 | 41, 43 | oveq12i 7155 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 +P
𝑣)
·P 𝑤) +P ((𝑦 +P
𝑣)
·P 𝑢)) = (((𝑦 ·P 𝑤) +P
(𝑣
·P 𝑤)) +P ((𝑦
·P 𝑢) +P (𝑣
·P 𝑢))) |
45 | | distrpr 10473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 +P
𝑣)
·P (𝑤 +P 𝑢)) = (((𝑦 +P 𝑣)
·P 𝑤) +P ((𝑦 +P
𝑣)
·P 𝑢)) |
46 | | ovex 7176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦
·P 𝑤) ∈ V |
47 | | ovex 7176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦
·P 𝑢) ∈ V |
48 | | ovex 7176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣
·P 𝑤) ∈ V |
49 | | addcompr 10466 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 +P
𝑔) = (𝑔 +P 𝑓) |
50 | | addasspr 10467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓 +P
𝑔)
+P ℎ) = (𝑓 +P (𝑔 +P
ℎ)) |
51 | | ovex 7176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣
·P 𝑢) ∈ V |
52 | 46, 47, 48, 49, 50, 51 | caov4 7368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦
·P 𝑤) +P (𝑦
·P 𝑢)) +P ((𝑣
·P 𝑤) +P (𝑣
·P 𝑢))) = (((𝑦 ·P 𝑤) +P
(𝑣
·P 𝑤)) +P ((𝑦
·P 𝑢) +P (𝑣
·P 𝑢))) |
53 | 44, 45, 52 | 3eqtr4i 2792 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 +P
𝑣)
·P (𝑤 +P 𝑢)) = (((𝑦 ·P 𝑤) +P
(𝑦
·P 𝑢)) +P ((𝑣
·P 𝑤) +P (𝑣
·P 𝑢))) |
54 | | ovex 7176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦
·P 𝑧) ∈ V |
55 | 48, 54, 51, 49, 50 | caov12 7365 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑣
·P 𝑤) +P ((𝑦
·P 𝑧) +P (𝑣
·P 𝑢))) = ((𝑦 ·P 𝑧) +P
((𝑣
·P 𝑤) +P (𝑣
·P 𝑢))) |
56 | 35, 53, 55 | 3eqtr4g 2819 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 +P
𝑢) = 𝑧 → ((𝑦 +P 𝑣)
·P (𝑤 +P 𝑢)) = ((𝑣 ·P 𝑤) +P
((𝑦
·P 𝑧) +P (𝑣
·P 𝑢)))) |
57 | | oveq1 7150 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 +P
𝑣) = 𝑥 → ((𝑦 +P 𝑣)
·P 𝑤) = (𝑥 ·P 𝑤)) |
58 | 41, 57 | syl5eqr 2808 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 +P
𝑣) = 𝑥 → ((𝑦 ·P 𝑤) +P
(𝑣
·P 𝑤)) = (𝑥 ·P 𝑤)) |
59 | 56, 58 | oveqan12rd 7163 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 +P
𝑣) = 𝑥 ∧ (𝑤 +P 𝑢) = 𝑧) → (((𝑦 +P 𝑣)
·P (𝑤 +P 𝑢)) +P
((𝑦
·P 𝑤) +P (𝑣
·P 𝑤))) = (((𝑣 ·P 𝑤) +P
((𝑦
·P 𝑧) +P (𝑣
·P 𝑢))) +P (𝑥
·P 𝑤))) |
60 | 31, 59 | eqtr3d 2796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 +P
𝑣) = 𝑥 ∧ (𝑤 +P 𝑢) = 𝑧) → ((𝑥 ·P 𝑧) +P
((𝑦
·P 𝑤) +P (𝑣
·P 𝑤))) = (((𝑣 ·P 𝑤) +P
((𝑦
·P 𝑧) +P (𝑣
·P 𝑢))) +P (𝑥
·P 𝑤))) |
61 | | addasspr 10467 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) +P (𝑣
·P 𝑤)) = ((𝑥 ·P 𝑧) +P
((𝑦
·P 𝑤) +P (𝑣
·P 𝑤))) |
62 | | addcompr 10466 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) +P (𝑣
·P 𝑤)) = ((𝑣 ·P 𝑤) +P
((𝑥
·P 𝑧) +P (𝑦
·P 𝑤))) |
63 | 61, 62 | eqtr3i 2784 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥
·P 𝑧) +P ((𝑦
·P 𝑤) +P (𝑣
·P 𝑤))) = ((𝑣 ·P 𝑤) +P
((𝑥
·P 𝑧) +P (𝑦
·P 𝑤))) |
64 | | addasspr 10467 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑣
·P 𝑤) +P (𝑥
·P 𝑤)) +P ((𝑦
·P 𝑧) +P (𝑣
·P 𝑢))) = ((𝑣 ·P 𝑤) +P
((𝑥
·P 𝑤) +P ((𝑦
·P 𝑧) +P (𝑣
·P 𝑢)))) |
65 | | ovex 7176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦
·P 𝑧) +P (𝑣
·P 𝑢)) ∈ V |
66 | | ovex 7176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥
·P 𝑤) ∈ V |
67 | 48, 65, 66, 49, 50 | caov32 7364 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑣
·P 𝑤) +P ((𝑦
·P 𝑧) +P (𝑣
·P 𝑢))) +P (𝑥
·P 𝑤)) = (((𝑣 ·P 𝑤) +P
(𝑥
·P 𝑤)) +P ((𝑦
·P 𝑧) +P (𝑣
·P 𝑢))) |
68 | | addasspr 10467 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥
·P 𝑤) +P (𝑦
·P 𝑧)) +P (𝑣
·P 𝑢)) = ((𝑥 ·P 𝑤) +P
((𝑦
·P 𝑧) +P (𝑣
·P 𝑢))) |
69 | 68 | oveq2i 7154 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑣
·P 𝑤) +P (((𝑥
·P 𝑤) +P (𝑦
·P 𝑧)) +P (𝑣
·P 𝑢))) = ((𝑣 ·P 𝑤) +P
((𝑥
·P 𝑤) +P ((𝑦
·P 𝑧) +P (𝑣
·P 𝑢)))) |
70 | 64, 67, 69 | 3eqtr4i 2792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑣
·P 𝑤) +P ((𝑦
·P 𝑧) +P (𝑣
·P 𝑢))) +P (𝑥
·P 𝑤)) = ((𝑣 ·P 𝑤) +P
(((𝑥
·P 𝑤) +P (𝑦
·P 𝑧)) +P (𝑣
·P 𝑢))) |
71 | 60, 63, 70 | 3eqtr3g 2817 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 +P
𝑣) = 𝑥 ∧ (𝑤 +P 𝑢) = 𝑧) → ((𝑣 ·P 𝑤) +P
((𝑥
·P 𝑧) +P (𝑦
·P 𝑤))) = ((𝑣 ·P 𝑤) +P
(((𝑥
·P 𝑤) +P (𝑦
·P 𝑧)) +P (𝑣
·P 𝑢)))) |
72 | | addcanpr 10491 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑣
·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 34 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑣
·P 𝑤) ∈ P ∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → (((𝑦 +P
𝑣) = 𝑥 ∧ (𝑤 +P 𝑢) = 𝑧) → ((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) = (((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧)) +P (𝑣
·P 𝑢)))) |
74 | | eqcom 2766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) = (((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧)) +P (𝑣
·P 𝑢)) ↔ (((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧)) +P (𝑣
·P 𝑢)) = ((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤))) |
75 | | ltaddpr2 10480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P → ((((𝑥
·P 𝑤) +P (𝑦
·P 𝑧)) +P (𝑣
·P 𝑢)) = ((𝑥 ·P 𝑧) +P
(𝑦
·P 𝑤)) → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))) |
76 | 74, 75 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P → (((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) = (((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧)) +P (𝑣
·P 𝑢)) → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))) |
77 | 76 | adantl 486 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑣
·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 47 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑣
·P 𝑤) ∈ P ∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → (((𝑦 +P
𝑣) = 𝑥 ∧ (𝑤 +P 𝑢) = 𝑧) → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))) |
79 | 29, 78 | sylan 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑣 ∈ P ∧
𝑤 ∈ P)
∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → (((𝑦 +P
𝑣) = 𝑥 ∧ (𝑤 +P 𝑢) = 𝑧) → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))) |
80 | 79 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ (((𝑣 ∈ P ∧
𝑤 ∈ P)
∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → (𝑢 ∈ P →
(((𝑦
+P 𝑣) = 𝑥 ∧ (𝑤 +P 𝑢) = 𝑧) → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤))))) |
81 | 80 | exp4a 436 |
. . . . . . . . . . . . . 14
⊢ (((𝑣 ∈ P ∧
𝑤 ∈ P)
∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → (𝑢 ∈ P →
((𝑦
+P 𝑣) = 𝑥 → ((𝑤 +P 𝑢) = 𝑧 → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))))) |
82 | 81 | com34 91 |
. . . . . . . . . . . . 13
⊢ (((𝑣 ∈ P ∧
𝑤 ∈ P)
∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → (𝑢 ∈ P →
((𝑤
+P 𝑢) = 𝑧 → ((𝑦 +P 𝑣) = 𝑥 → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))))) |
83 | 82 | rexlimdv 3205 |
. . . . . . . . . . . 12
⊢ (((𝑣 ∈ P ∧
𝑤 ∈ P)
∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) →
(∃𝑢 ∈
P (𝑤
+P 𝑢) = 𝑧 → ((𝑦 +P 𝑣) = 𝑥 → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤))))) |
84 | 83 | expl 462 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ P →
((𝑤 ∈ P
∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) →
(∃𝑢 ∈
P (𝑤
+P 𝑢) = 𝑧 → ((𝑦 +P 𝑣) = 𝑥 → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))))) |
85 | 84 | com24 95 |
. . . . . . . . . 10
⊢ (𝑣 ∈ P →
((𝑦
+P 𝑣) = 𝑥 → (∃𝑢 ∈ P (𝑤 +P 𝑢) = 𝑧 → ((𝑤 ∈ P ∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → ((𝑥
·P 𝑤) +P (𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))))) |
86 | 85 | rexlimiv 3202 |
. . . . . . . . 9
⊢
(∃𝑣 ∈
P (𝑦
+P 𝑣) = 𝑥 → (∃𝑢 ∈ P (𝑤 +P 𝑢) = 𝑧 → ((𝑤 ∈ P ∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → ((𝑥
·P 𝑤) +P (𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤))))) |
87 | 27, 28, 86 | syl2im 40 |
. . . . . . . 8
⊢ (𝑦<P
𝑥 → (𝑤<P
𝑧 → ((𝑤 ∈ P ∧
((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → ((𝑥
·P 𝑤) +P (𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤))))) |
88 | 87 | imp 411 |
. . . . . . 7
⊢ ((𝑦<P
𝑥 ∧ 𝑤<P 𝑧) → ((𝑤 ∈ P ∧ ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → ((𝑥
·P 𝑤) +P (𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))) |
89 | 88 | com12 32 |
. . . . . 6
⊢ ((𝑤 ∈ P ∧
((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)) ∈ P) → ((𝑦<P
𝑥 ∧ 𝑤<P 𝑧) → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))) |
90 | 21, 26, 89 | syl2anc 588 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑦<P 𝑥 ∧ 𝑤<P 𝑧) → ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))) |
91 | | mulsrpr 10521 |
. . . . . . 7
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ([〈𝑥, 𝑦〉] ~R
·R [〈𝑧, 𝑤〉] ~R ) =
[〈((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)), ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))〉] ~R
) |
92 | 91 | breq2d 5037 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (0R
<R ([〈𝑥, 𝑦〉] ~R
·R [〈𝑧, 𝑤〉] ~R ) ↔
0R <R [〈((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)), ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))〉] ~R
)) |
93 | | gt0srpr 10523 |
. . . . . 6
⊢
(0R <R
[〈((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)), ((𝑥 ·P 𝑤) +P
(𝑦
·P 𝑧))〉] ~R ↔
((𝑥
·P 𝑤) +P (𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤))) |
94 | 92, 93 | bitrdi 290 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (0R
<R ([〈𝑥, 𝑦〉] ~R
·R [〈𝑧, 𝑤〉] ~R ) ↔
((𝑥
·P 𝑤) +P (𝑦
·P 𝑧))<P ((𝑥
·P 𝑧) +P (𝑦
·P 𝑤)))) |
95 | 90, 94 | sylibrd 262 |
. . . 4
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((𝑦<P 𝑥 ∧ 𝑤<P 𝑧) →
0R <R ([〈𝑥, 𝑦〉] ~R
·R [〈𝑧, 𝑤〉] ~R
))) |
96 | 20, 95 | syl5bi 245 |
. . 3
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → ((0R
<R [〈𝑥, 𝑦〉] ~R ∧
0R <R [〈𝑧, 𝑤〉] ~R ) →
0R <R ([〈𝑥, 𝑦〉] ~R
·R [〈𝑧, 𝑤〉] ~R
))) |
97 | 7, 12, 17, 96 | 2ecoptocl 8391 |
. 2
⊢ ((𝐴 ∈ R ∧
𝐵 ∈ R)
→ ((0R <R 𝐴 ∧
0R <R 𝐵) → 0R
<R (𝐴 ·R 𝐵))) |
98 | 6, 97 | mpcom 38 |
1
⊢
((0R <R 𝐴 ∧
0R <R 𝐵) → 0R
<R (𝐴 ·R 𝐵)) |