Step | Hyp | Ref
| Expression |
1 | | ltmnqg 7352 |
. . . . . . 7
⊢ ((𝑤 ∈ Q ∧
𝑣 ∈ Q
∧ 𝑢 ∈
Q) → (𝑤
<Q 𝑣 ↔ (𝑢 ·Q 𝑤) <Q
(𝑢
·Q 𝑣))) |
2 | 1 | adantl 275 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q ∧
𝑢 ∈ Q))
→ (𝑤
<Q 𝑣 ↔ (𝑢 ·Q 𝑤) <Q
(𝑢
·Q 𝑣))) |
3 | | simp1 992 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → 𝐴
∈ P) |
4 | | simpll 524 |
. . . . . . 7
⊢ (((𝑥 ∈ (2nd
‘𝐴) ∧ 𝑦 ∈ (2nd
‘𝐵)) ∧ (𝑓 ∈ (2nd
‘𝐴) ∧ 𝑧 ∈ (2nd
‘𝐶))) → 𝑥 ∈ (2nd
‘𝐴)) |
5 | | prop 7426 |
. . . . . . . 8
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
6 | | elprnqu 7433 |
. . . . . . . 8
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑥 ∈ (2nd
‘𝐴)) → 𝑥 ∈
Q) |
7 | 5, 6 | sylan 281 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ (2nd
‘𝐴)) → 𝑥 ∈
Q) |
8 | 3, 4, 7 | syl2an 287 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝑥 ∈ Q) |
9 | | simprl 526 |
. . . . . . 7
⊢ (((𝑥 ∈ (2nd
‘𝐴) ∧ 𝑦 ∈ (2nd
‘𝐵)) ∧ (𝑓 ∈ (2nd
‘𝐴) ∧ 𝑧 ∈ (2nd
‘𝐶))) → 𝑓 ∈ (2nd
‘𝐴)) |
10 | | elprnqu 7433 |
. . . . . . . 8
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑓 ∈ (2nd
‘𝐴)) → 𝑓 ∈
Q) |
11 | 5, 10 | sylan 281 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ (2nd
‘𝐴)) → 𝑓 ∈
Q) |
12 | 3, 9, 11 | syl2an 287 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝑓 ∈ Q) |
13 | | simpl3 997 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝐶 ∈ P) |
14 | | simprrr 535 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝑧 ∈ (2nd ‘𝐶)) |
15 | | prop 7426 |
. . . . . . . 8
⊢ (𝐶 ∈ P →
〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈
P) |
16 | | elprnqu 7433 |
. . . . . . . 8
⊢
((〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈ P ∧ 𝑧 ∈ (2nd
‘𝐶)) → 𝑧 ∈
Q) |
17 | 15, 16 | sylan 281 |
. . . . . . 7
⊢ ((𝐶 ∈ P ∧
𝑧 ∈ (2nd
‘𝐶)) → 𝑧 ∈
Q) |
18 | 13, 14, 17 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝑧 ∈ Q) |
19 | | mulcomnqg 7334 |
. . . . . . 7
⊢ ((𝑤 ∈ Q ∧
𝑣 ∈ Q)
→ (𝑤
·Q 𝑣) = (𝑣 ·Q 𝑤)) |
20 | 19 | adantl 275 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q)) →
(𝑤
·Q 𝑣) = (𝑣 ·Q 𝑤)) |
21 | 2, 8, 12, 18, 20 | caovord2d 6020 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑥 <Q 𝑓 ↔ (𝑥 ·Q 𝑧) <Q
(𝑓
·Q 𝑧))) |
22 | | mulclnq 7327 |
. . . . . . 7
⊢ ((𝑥 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑥
·Q 𝑧) ∈ Q) |
23 | 8, 18, 22 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑥 ·Q 𝑧) ∈
Q) |
24 | | mulclnq 7327 |
. . . . . . 7
⊢ ((𝑓 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑓
·Q 𝑧) ∈ Q) |
25 | 12, 18, 24 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑓 ·Q 𝑧) ∈
Q) |
26 | | simpl2 996 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝐵 ∈ P) |
27 | | simprlr 533 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝑦 ∈ (2nd ‘𝐵)) |
28 | | prop 7426 |
. . . . . . . . 9
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
29 | | elprnqu 7433 |
. . . . . . . . 9
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑦 ∈ (2nd
‘𝐵)) → 𝑦 ∈
Q) |
30 | 28, 29 | sylan 281 |
. . . . . . . 8
⊢ ((𝐵 ∈ P ∧
𝑦 ∈ (2nd
‘𝐵)) → 𝑦 ∈
Q) |
31 | 26, 27, 30 | syl2anc 409 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝑦 ∈ Q) |
32 | | mulclnq 7327 |
. . . . . . 7
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
·Q 𝑦) ∈ Q) |
33 | 8, 31, 32 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑥 ·Q 𝑦) ∈
Q) |
34 | | ltanqg 7351 |
. . . . . 6
⊢ (((𝑥
·Q 𝑧) ∈ Q ∧ (𝑓
·Q 𝑧) ∈ Q ∧ (𝑥
·Q 𝑦) ∈ Q) → ((𝑥
·Q 𝑧) <Q (𝑓
·Q 𝑧) ↔ ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)))) |
35 | 23, 25, 33, 34 | syl3anc 1233 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → ((𝑥 ·Q 𝑧) <Q
(𝑓
·Q 𝑧) ↔ ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)))) |
36 | 21, 35 | bitrd 187 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑥 <Q 𝑓 ↔ ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)))) |
37 | | simpl1 995 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝐴 ∈ P) |
38 | | addclpr 7488 |
. . . . . . . 8
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝐵
+P 𝐶) ∈ P) |
39 | 38 | 3adant1 1010 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐵
+P 𝐶) ∈ P) |
40 | 39 | adantr 274 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝐵 +P 𝐶) ∈
P) |
41 | | mulclpr 7523 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) → (𝐴
·P (𝐵 +P 𝐶)) ∈
P) |
42 | 37, 40, 41 | syl2anc 409 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝐴 ·P (𝐵 +P
𝐶)) ∈
P) |
43 | | distrnqg 7338 |
. . . . . . 7
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
·Q (𝑦 +Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧))) |
44 | 8, 31, 18, 43 | syl3anc 1233 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑥 ·Q (𝑦 +Q
𝑧)) = ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧))) |
45 | | simprll 532 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝑥 ∈ (2nd ‘𝐴)) |
46 | | df-iplp 7419 |
. . . . . . . . . 10
⊢
+P = (𝑢 ∈ P, 𝑣 ∈ P ↦ 〈{𝑤 ∈ Q ∣
∃𝑔 ∈
Q ∃ℎ
∈ Q (𝑔
∈ (1st ‘𝑢) ∧ ℎ ∈ (1st ‘𝑣) ∧ 𝑤 = (𝑔 +Q ℎ))}, {𝑤 ∈ Q ∣ ∃𝑔 ∈ Q
∃ℎ ∈
Q (𝑔 ∈
(2nd ‘𝑢)
∧ ℎ ∈
(2nd ‘𝑣)
∧ 𝑤 = (𝑔 +Q
ℎ))}〉) |
47 | | addclnq 7326 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
48 | 46, 47 | genppreclu 7466 |
. . . . . . . . 9
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ ((𝑦 ∈
(2nd ‘𝐵)
∧ 𝑧 ∈
(2nd ‘𝐶))
→ (𝑦
+Q 𝑧) ∈ (2nd ‘(𝐵 +P
𝐶)))) |
49 | 48 | imp 123 |
. . . . . . . 8
⊢ (((𝐵 ∈ P ∧
𝐶 ∈ P)
∧ (𝑦 ∈
(2nd ‘𝐵)
∧ 𝑧 ∈
(2nd ‘𝐶)))
→ (𝑦
+Q 𝑧) ∈ (2nd ‘(𝐵 +P
𝐶))) |
50 | 26, 13, 27, 14, 49 | syl22anc 1234 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑦 +Q 𝑧) ∈ (2nd
‘(𝐵
+P 𝐶))) |
51 | | df-imp 7420 |
. . . . . . . . 9
⊢
·P = (𝑢 ∈ P, 𝑣 ∈ P ↦ 〈{𝑤 ∈ Q ∣
∃𝑔 ∈
Q ∃ℎ
∈ Q (𝑔
∈ (1st ‘𝑢) ∧ ℎ ∈ (1st ‘𝑣) ∧ 𝑤 = (𝑔 ·Q ℎ))}, {𝑤 ∈ Q ∣ ∃𝑔 ∈ Q
∃ℎ ∈
Q (𝑔 ∈
(2nd ‘𝑢)
∧ ℎ ∈
(2nd ‘𝑣)
∧ 𝑤 = (𝑔
·Q ℎ))}〉) |
52 | | mulclnq 7327 |
. . . . . . . . 9
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
·Q ℎ) ∈ Q) |
53 | 51, 52 | genppreclu 7466 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) → ((𝑥 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑧) ∈ (2nd
‘(𝐵
+P 𝐶))) → (𝑥 ·Q (𝑦 +Q
𝑧)) ∈ (2nd
‘(𝐴
·P (𝐵 +P 𝐶))))) |
54 | 53 | imp 123 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑧) ∈ (2nd
‘(𝐵
+P 𝐶)))) → (𝑥 ·Q (𝑦 +Q
𝑧)) ∈ (2nd
‘(𝐴
·P (𝐵 +P 𝐶)))) |
55 | 37, 40, 45, 50, 54 | syl22anc 1234 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑥 ·Q (𝑦 +Q
𝑧)) ∈ (2nd
‘(𝐴
·P (𝐵 +P 𝐶)))) |
56 | 44, 55 | eqeltrrd 2248 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶)))) |
57 | | prop 7426 |
. . . . . 6
⊢ ((𝐴
·P (𝐵 +P 𝐶)) ∈ P →
〈(1st ‘(𝐴 ·P (𝐵 +P
𝐶))), (2nd
‘(𝐴
·P (𝐵 +P 𝐶)))〉 ∈
P) |
58 | | prcunqu 7436 |
. . . . . 6
⊢
((〈(1st ‘(𝐴 ·P (𝐵 +P
𝐶))), (2nd
‘(𝐴
·P (𝐵 +P 𝐶)))〉 ∈ P
∧ ((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶)))) → (((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
59 | 57, 58 | sylan 281 |
. . . . 5
⊢ (((𝐴
·P (𝐵 +P 𝐶)) ∈ P ∧
((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶)))) → (((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
60 | 42, 56, 59 | syl2anc 409 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
61 | 36, 60 | sylbid 149 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑥 <Q 𝑓 → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
62 | 2, 12, 8, 31, 20 | caovord2d 6020 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑓 <Q 𝑥 ↔ (𝑓 ·Q 𝑦) <Q
(𝑥
·Q 𝑦))) |
63 | | ltanqg 7351 |
. . . . . . 7
⊢ ((𝑤 ∈ Q ∧
𝑣 ∈ Q
∧ 𝑢 ∈
Q) → (𝑤
<Q 𝑣 ↔ (𝑢 +Q 𝑤) <Q
(𝑢
+Q 𝑣))) |
64 | 63 | adantl 275 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q ∧
𝑢 ∈ Q))
→ (𝑤
<Q 𝑣 ↔ (𝑢 +Q 𝑤) <Q
(𝑢
+Q 𝑣))) |
65 | | mulclnq 7327 |
. . . . . . 7
⊢ ((𝑓 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑓
·Q 𝑦) ∈ Q) |
66 | 12, 31, 65 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑓 ·Q 𝑦) ∈
Q) |
67 | | addcomnqg 7332 |
. . . . . . 7
⊢ ((𝑤 ∈ Q ∧
𝑣 ∈ Q)
→ (𝑤
+Q 𝑣) = (𝑣 +Q 𝑤)) |
68 | 67 | adantl 275 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q)) →
(𝑤
+Q 𝑣) = (𝑣 +Q 𝑤)) |
69 | 64, 66, 33, 25, 68 | caovord2d 6020 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → ((𝑓 ·Q 𝑦) <Q
(𝑥
·Q 𝑦) ↔ ((𝑓 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)))) |
70 | 62, 69 | bitrd 187 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑓 <Q 𝑥 ↔ ((𝑓 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)))) |
71 | | distrnqg 7338 |
. . . . . . 7
⊢ ((𝑓 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑓
·Q (𝑦 +Q 𝑧)) = ((𝑓 ·Q 𝑦) +Q
(𝑓
·Q 𝑧))) |
72 | 12, 31, 18, 71 | syl3anc 1233 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑓 ·Q (𝑦 +Q
𝑧)) = ((𝑓 ·Q 𝑦) +Q
(𝑓
·Q 𝑧))) |
73 | | simprrl 534 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → 𝑓 ∈ (2nd ‘𝐴)) |
74 | 51, 52 | genppreclu 7466 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) → ((𝑓 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑧) ∈ (2nd
‘(𝐵
+P 𝐶))) → (𝑓 ·Q (𝑦 +Q
𝑧)) ∈ (2nd
‘(𝐴
·P (𝐵 +P 𝐶))))) |
75 | 74 | imp 123 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) ∧ (𝑓 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑧) ∈ (2nd
‘(𝐵
+P 𝐶)))) → (𝑓 ·Q (𝑦 +Q
𝑧)) ∈ (2nd
‘(𝐴
·P (𝐵 +P 𝐶)))) |
76 | 37, 40, 73, 50, 75 | syl22anc 1234 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑓 ·Q (𝑦 +Q
𝑧)) ∈ (2nd
‘(𝐴
·P (𝐵 +P 𝐶)))) |
77 | 72, 76 | eqeltrrd 2248 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → ((𝑓 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶)))) |
78 | | prcunqu 7436 |
. . . . . 6
⊢
((〈(1st ‘(𝐴 ·P (𝐵 +P
𝐶))), (2nd
‘(𝐴
·P (𝐵 +P 𝐶)))〉 ∈ P
∧ ((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶)))) → (((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
79 | 57, 78 | sylan 281 |
. . . . 5
⊢ (((𝐴
·P (𝐵 +P 𝐶)) ∈ P ∧
((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶)))) → (((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
80 | 42, 77, 79 | syl2anc 409 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
81 | 70, 80 | sylbid 149 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑓 <Q 𝑥 → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
82 | 61, 81 | jaod 712 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → ((𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
83 | | ltsonq 7349 |
. . . . 5
⊢
<Q Or Q |
84 | | nqtri3or 7347 |
. . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑥
<Q 𝑓 ∨ 𝑥 = 𝑓 ∨ 𝑓 <Q 𝑥)) |
85 | 83, 84 | sotritrieq 4308 |
. . . 4
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑥 = 𝑓 ↔ ¬ (𝑥 <Q
𝑓 ∨ 𝑓 <Q 𝑥))) |
86 | 8, 12, 85 | syl2anc 409 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑥 = 𝑓 ↔ ¬ (𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥))) |
87 | | oveq1 5858 |
. . . . . . 7
⊢ (𝑥 = 𝑓 → (𝑥 ·Q 𝑧) = (𝑓 ·Q 𝑧)) |
88 | 87 | oveq2d 5867 |
. . . . . 6
⊢ (𝑥 = 𝑓 → ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧))) |
89 | 44, 88 | sylan9eq 2223 |
. . . . 5
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) ∧ 𝑥 = 𝑓) → (𝑥 ·Q (𝑦 +Q
𝑧)) = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧))) |
90 | 55 | adantr 274 |
. . . . 5
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) ∧ 𝑥 = 𝑓) → (𝑥 ·Q (𝑦 +Q
𝑧)) ∈ (2nd
‘(𝐴
·P (𝐵 +P 𝐶)))) |
91 | 89, 90 | eqeltrrd 2248 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) ∧ 𝑥 = 𝑓) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶)))) |
92 | 91 | ex 114 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (𝑥 = 𝑓 → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
93 | 86, 92 | sylbird 169 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → (¬ (𝑥 <Q
𝑓 ∨ 𝑓 <Q 𝑥) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶))))) |
94 | | ltdcnq 7348 |
. . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ DECID 𝑥 <Q 𝑓) |
95 | | ltdcnq 7348 |
. . . . . 6
⊢ ((𝑓 ∈ Q ∧
𝑥 ∈ Q)
→ DECID 𝑓 <Q 𝑥) |
96 | 95 | ancoms 266 |
. . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ DECID 𝑓 <Q 𝑥) |
97 | | dcor 930 |
. . . . 5
⊢
(DECID 𝑥 <Q 𝑓 → (DECID
𝑓
<Q 𝑥 → DECID (𝑥 <Q
𝑓 ∨ 𝑓 <Q 𝑥))) |
98 | 94, 96, 97 | sylc 62 |
. . . 4
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ DECID (𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥)) |
99 | 8, 12, 98 | syl2anc 409 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → DECID
(𝑥
<Q 𝑓 ∨ 𝑓 <Q 𝑥)) |
100 | | df-dc 830 |
. . 3
⊢
(DECID (𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥) ↔ ((𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥) ∨ ¬ (𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥))) |
101 | 99, 100 | sylib 121 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → ((𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥) ∨ ¬ (𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥))) |
102 | 82, 93, 101 | mpjaod 713 |
1
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐵)) ∧ (𝑓 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐶)))) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (2nd ‘(𝐴
·P (𝐵 +P 𝐶)))) |