Step | Hyp | Ref
| Expression |
1 | | ltmnqg 6385 |
. . . . . . 7
⊢
((w ∈ Q ∧ v ∈ Q ∧ u ∈ Q) → (w <Q v ↔ (u
·Q w)
<Q (u
·Q v))) |
2 | 1 | adantl 262 |
. . . . . 6
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) ∧
(w ∈
Q ∧ v ∈
Q ∧ u ∈
Q)) → (w
<Q v ↔
(u ·Q
w) <Q (u ·Q v))) |
3 | | simp1 903 |
. . . . . . 7
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → A ∈ P) |
4 | | simpll 481 |
. . . . . . 7
⊢
(((x ∈ (1st ‘A) ∧ y ∈
(1st ‘B)) ∧ (f ∈ (1st ‘A) ∧ z ∈
(1st ‘𝐶)))
→ x ∈ (1st ‘A)) |
5 | | prop 6458 |
. . . . . . . 8
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
6 | | elprnql 6464 |
. . . . . . . 8
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ x ∈ (1st ‘A)) → x
∈ Q) |
7 | 5, 6 | sylan 267 |
. . . . . . 7
⊢
((A ∈ P ∧ x ∈ (1st ‘A)) → x
∈ Q) |
8 | 3, 4, 7 | syl2an 273 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → x ∈
Q) |
9 | | simprl 483 |
. . . . . . 7
⊢
(((x ∈ (1st ‘A) ∧ y ∈
(1st ‘B)) ∧ (f ∈ (1st ‘A) ∧ z ∈
(1st ‘𝐶)))
→ f ∈ (1st ‘A)) |
10 | | elprnql 6464 |
. . . . . . . 8
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ f ∈ (1st ‘A)) → f
∈ Q) |
11 | 5, 10 | sylan 267 |
. . . . . . 7
⊢
((A ∈ P ∧ f ∈ (1st ‘A)) → f
∈ Q) |
12 | 3, 9, 11 | syl2an 273 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → f ∈
Q) |
13 | | simpl2 907 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → B ∈
P) |
14 | | simprlr 490 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → y ∈
(1st ‘B)) |
15 | | prop 6458 |
. . . . . . . 8
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
16 | | elprnql 6464 |
. . . . . . . 8
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ y ∈ (1st ‘B)) → y
∈ Q) |
17 | 15, 16 | sylan 267 |
. . . . . . 7
⊢
((B ∈ P ∧ y ∈ (1st ‘B)) → y
∈ Q) |
18 | 13, 14, 17 | syl2anc 391 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → y ∈
Q) |
19 | | mulcomnqg 6367 |
. . . . . . 7
⊢
((w ∈ Q ∧ v ∈ Q) → (w ·Q v) = (v
·Q w)) |
20 | 19 | adantl 262 |
. . . . . 6
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) ∧
(w ∈
Q ∧ v ∈
Q)) → (w
·Q v) =
(v ·Q
w)) |
21 | 2, 8, 12, 18, 20 | caovord2d 5612 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (x <Q f ↔ (x
·Q y)
<Q (f
·Q y))) |
22 | | ltanqg 6384 |
. . . . . . 7
⊢
((w ∈ Q ∧ v ∈ Q ∧ u ∈ Q) → (w <Q v ↔ (u
+Q w)
<Q (u
+Q v))) |
23 | 22 | adantl 262 |
. . . . . 6
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) ∧
(w ∈
Q ∧ v ∈
Q ∧ u ∈
Q)) → (w
<Q v ↔
(u +Q w) <Q (u +Q v))) |
24 | | mulclnq 6360 |
. . . . . . 7
⊢
((x ∈ Q ∧ y ∈ Q) → (x ·Q y) ∈
Q) |
25 | 8, 18, 24 | syl2anc 391 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (x ·Q y) ∈
Q) |
26 | | mulclnq 6360 |
. . . . . . 7
⊢
((f ∈ Q ∧ y ∈ Q) → (f ·Q y) ∈
Q) |
27 | 12, 18, 26 | syl2anc 391 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (f ·Q y) ∈
Q) |
28 | | simpl3 908 |
. . . . . . . 8
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → 𝐶 ∈
P) |
29 | | simprrr 492 |
. . . . . . . 8
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → z ∈
(1st ‘𝐶)) |
30 | | prop 6458 |
. . . . . . . . 9
⊢ (𝐶 ∈ P → 〈(1st
‘𝐶), (2nd
‘𝐶)〉 ∈ P) |
31 | | elprnql 6464 |
. . . . . . . . 9
⊢
((〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈
P ∧ z ∈
(1st ‘𝐶))
→ z ∈ Q) |
32 | 30, 31 | sylan 267 |
. . . . . . . 8
⊢ ((𝐶 ∈ P ∧ z ∈ (1st ‘𝐶)) → z ∈
Q) |
33 | 28, 29, 32 | syl2anc 391 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → z ∈
Q) |
34 | | mulclnq 6360 |
. . . . . . 7
⊢
((f ∈ Q ∧ z ∈ Q) → (f ·Q z) ∈
Q) |
35 | 12, 33, 34 | syl2anc 391 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (f ·Q z) ∈
Q) |
36 | | addcomnqg 6365 |
. . . . . . 7
⊢
((w ∈ Q ∧ v ∈ Q) → (w +Q v) = (v
+Q w)) |
37 | 36 | adantl 262 |
. . . . . 6
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) ∧
(w ∈
Q ∧ v ∈
Q)) → (w
+Q v) = (v +Q w)) |
38 | 23, 25, 27, 35, 37 | caovord2d 5612 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → ((x ·Q y) <Q (f ·Q y) ↔ ((x
·Q y)
+Q (f
·Q z))
<Q ((f
·Q y)
+Q (f
·Q z)))) |
39 | 21, 38 | bitrd 177 |
. . . 4
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (x <Q f ↔ ((x
·Q y)
+Q (f
·Q z))
<Q ((f
·Q y)
+Q (f
·Q z)))) |
40 | | simpl1 906 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → A ∈
P) |
41 | | addclpr 6520 |
. . . . . . . 8
⊢
((B ∈ P ∧ 𝐶 ∈
P) → (B
+P 𝐶) ∈
P) |
42 | 41 | 3adant1 921 |
. . . . . . 7
⊢
((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) → (B
+P 𝐶) ∈
P) |
43 | 42 | adantr 261 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (B +P 𝐶) ∈
P) |
44 | | mulclpr 6553 |
. . . . . 6
⊢
((A ∈ P ∧ (B
+P 𝐶) ∈
P) → (A
·P (B
+P 𝐶)) ∈
P) |
45 | 40, 43, 44 | syl2anc 391 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (A ·P (B +P 𝐶)) ∈
P) |
46 | | distrnqg 6371 |
. . . . . . 7
⊢
((f ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → (f ·Q (y +Q z)) = ((f
·Q y)
+Q (f
·Q z))) |
47 | 12, 18, 33, 46 | syl3anc 1134 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (f ·Q (y +Q z)) = ((f
·Q y)
+Q (f
·Q z))) |
48 | | simprrl 491 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → f ∈
(1st ‘A)) |
49 | | df-iplp 6451 |
. . . . . . . . . 10
⊢
+P = (u ∈ P, v ∈
P ↦ 〈{w ∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(1st ‘u) ∧ ℎ
∈ (1st ‘v) ∧ w = (g
+Q ℎ))}, {w
∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(2nd ‘u) ∧ ℎ
∈ (2nd ‘v) ∧ w = (g
+Q ℎ))}〉) |
50 | | addclnq 6359 |
. . . . . . . . . 10
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (g +Q ℎ) ∈
Q) |
51 | 49, 50 | genpprecll 6497 |
. . . . . . . . 9
⊢
((B ∈ P ∧ 𝐶 ∈
P) → ((y ∈ (1st ‘B) ∧ z ∈
(1st ‘𝐶))
→ (y +Q
z) ∈
(1st ‘(B
+P 𝐶)))) |
52 | 51 | imp 115 |
. . . . . . . 8
⊢
(((B ∈ P ∧ 𝐶 ∈
P) ∧ (y ∈
(1st ‘B) ∧ z ∈ (1st ‘𝐶))) → (y +Q z) ∈
(1st ‘(B
+P 𝐶))) |
53 | 13, 28, 14, 29, 52 | syl22anc 1135 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (y +Q z) ∈
(1st ‘(B
+P 𝐶))) |
54 | | df-imp 6452 |
. . . . . . . . 9
⊢
·P = (u
∈ P, v ∈
P ↦ 〈{w ∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(1st ‘u) ∧ ℎ
∈ (1st ‘v) ∧ w = (g
·Q ℎ))}, {w
∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(2nd ‘u) ∧ ℎ
∈ (2nd ‘v) ∧ w = (g
·Q ℎ))}〉) |
55 | | mulclnq 6360 |
. . . . . . . . 9
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (g ·Q ℎ) ∈
Q) |
56 | 54, 55 | genpprecll 6497 |
. . . . . . . 8
⊢
((A ∈ P ∧ (B
+P 𝐶) ∈
P) → ((f ∈ (1st ‘A) ∧ (y +Q z) ∈
(1st ‘(B
+P 𝐶))) → (f ·Q (y +Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶))))) |
57 | 56 | imp 115 |
. . . . . . 7
⊢
(((A ∈ P ∧ (B
+P 𝐶) ∈
P) ∧ (f ∈
(1st ‘A) ∧ (y
+Q z) ∈ (1st ‘(B +P 𝐶)))) → (f ·Q (y +Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶)))) |
58 | 40, 43, 48, 53, 57 | syl22anc 1135 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (f ·Q (y +Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶)))) |
59 | 47, 58 | eqeltrrd 2112 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → ((f ·Q y) +Q (f ·Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶)))) |
60 | | prop 6458 |
. . . . . 6
⊢
((A
·P (B
+P 𝐶)) ∈
P → 〈(1st ‘(A ·P (B +P 𝐶))), (2nd ‘(A ·P (B +P 𝐶)))〉 ∈ P) |
61 | | prcdnql 6467 |
. . . . . 6
⊢
((〈(1st ‘(A
·P (B
+P 𝐶))), (2nd ‘(A ·P (B +P 𝐶)))〉 ∈ P ∧ ((f
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶)))) → (((x ·Q y) +Q (f ·Q z)) <Q ((f ·Q y) +Q (f ·Q z)) → ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶))))) |
62 | 60, 61 | sylan 267 |
. . . . 5
⊢
(((A
·P (B
+P 𝐶)) ∈
P ∧ ((f ·Q y) +Q (f ·Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶)))) → (((x ·Q y) +Q (f ·Q z)) <Q ((f ·Q y) +Q (f ·Q z)) → ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶))))) |
63 | 45, 59, 62 | syl2anc 391 |
. . . 4
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (((x ·Q y) +Q (f ·Q z)) <Q ((f ·Q y) +Q (f ·Q z)) → ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶))))) |
64 | 39, 63 | sylbid 139 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (x <Q f → ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶))))) |
65 | 2, 12, 8, 33, 20 | caovord2d 5612 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (f <Q x ↔ (f
·Q z)
<Q (x
·Q z))) |
66 | | mulclnq 6360 |
. . . . . . 7
⊢
((x ∈ Q ∧ z ∈ Q) → (x ·Q z) ∈
Q) |
67 | 8, 33, 66 | syl2anc 391 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (x ·Q z) ∈
Q) |
68 | | ltanqg 6384 |
. . . . . 6
⊢
(((f
·Q z) ∈ Q ∧ (x
·Q z) ∈ Q ∧ (x
·Q y) ∈ Q) → ((f ·Q z) <Q (x ·Q z) ↔ ((x
·Q y)
+Q (f
·Q z))
<Q ((x
·Q y)
+Q (x
·Q z)))) |
69 | 35, 67, 25, 68 | syl3anc 1134 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → ((f ·Q z) <Q (x ·Q z) ↔ ((x
·Q y)
+Q (f
·Q z))
<Q ((x
·Q y)
+Q (x
·Q z)))) |
70 | 65, 69 | bitrd 177 |
. . . 4
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (f <Q x ↔ ((x
·Q y)
+Q (f
·Q z))
<Q ((x
·Q y)
+Q (x
·Q z)))) |
71 | | distrnqg 6371 |
. . . . . . 7
⊢
((x ∈ Q ∧ y ∈ Q ∧ z ∈ Q) → (x ·Q (y +Q z)) = ((x
·Q y)
+Q (x
·Q z))) |
72 | 8, 18, 33, 71 | syl3anc 1134 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (x ·Q (y +Q z)) = ((x
·Q y)
+Q (x
·Q z))) |
73 | | simprll 489 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → x ∈
(1st ‘A)) |
74 | 54, 55 | genpprecll 6497 |
. . . . . . . 8
⊢
((A ∈ P ∧ (B
+P 𝐶) ∈
P) → ((x ∈ (1st ‘A) ∧ (y +Q z) ∈
(1st ‘(B
+P 𝐶))) → (x ·Q (y +Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶))))) |
75 | 74 | imp 115 |
. . . . . . 7
⊢
(((A ∈ P ∧ (B
+P 𝐶) ∈
P) ∧ (x ∈
(1st ‘A) ∧ (y
+Q z) ∈ (1st ‘(B +P 𝐶)))) → (x ·Q (y +Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶)))) |
76 | 40, 43, 73, 53, 75 | syl22anc 1135 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (x ·Q (y +Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶)))) |
77 | 72, 76 | eqeltrrd 2112 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → ((x ·Q y) +Q (x ·Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶)))) |
78 | | prcdnql 6467 |
. . . . . 6
⊢
((〈(1st ‘(A
·P (B
+P 𝐶))), (2nd ‘(A ·P (B +P 𝐶)))〉 ∈ P ∧ ((x
·Q y)
+Q (x
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶)))) → (((x ·Q y) +Q (f ·Q z)) <Q ((x ·Q y) +Q (x ·Q z)) → ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶))))) |
79 | 60, 78 | sylan 267 |
. . . . 5
⊢
(((A
·P (B
+P 𝐶)) ∈
P ∧ ((x ·Q y) +Q (x ·Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶)))) → (((x ·Q y) +Q (f ·Q z)) <Q ((x ·Q y) +Q (x ·Q z)) → ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶))))) |
80 | 45, 77, 79 | syl2anc 391 |
. . . 4
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (((x ·Q y) +Q (f ·Q z)) <Q ((x ·Q y) +Q (x ·Q z)) → ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶))))) |
81 | 70, 80 | sylbid 139 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (f <Q x → ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶))))) |
82 | 64, 81 | jaod 636 |
. 2
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → ((x <Q f ∨ f <Q x) → ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶))))) |
83 | | ltsonq 6382 |
. . . . 5
⊢
<Q Or Q |
84 | | nqtri3or 6380 |
. . . . 5
⊢
((x ∈ Q ∧ f ∈ Q) → (x <Q f ∨ x = f ∨ f
<Q x)) |
85 | 83, 84 | sotritrieq 4053 |
. . . 4
⊢
((x ∈ Q ∧ f ∈ Q) → (x = f ↔
¬ (x <Q
f ∨
f <Q x))) |
86 | 8, 12, 85 | syl2anc 391 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (x = f ↔
¬ (x <Q
f ∨
f <Q x))) |
87 | | oveq1 5462 |
. . . . . . 7
⊢ (x = f →
(x ·Q
z) = (f
·Q z)) |
88 | 87 | oveq2d 5471 |
. . . . . 6
⊢ (x = f →
((x ·Q
y) +Q (x ·Q z)) = ((x
·Q y)
+Q (f
·Q z))) |
89 | 72, 88 | sylan9eq 2089 |
. . . . 5
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) ∧
x = f)
→ (x
·Q (y
+Q z)) =
((x ·Q
y) +Q (f ·Q z))) |
90 | 76 | adantr 261 |
. . . . 5
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) ∧
x = f)
→ (x
·Q (y
+Q z)) ∈ (1st ‘(A ·P (B +P 𝐶)))) |
91 | 89, 90 | eqeltrrd 2112 |
. . . 4
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) ∧
x = f)
→ ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶)))) |
92 | 91 | ex 108 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (x = f →
((x ·Q
y) +Q (f ·Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶))))) |
93 | 86, 92 | sylbird 159 |
. 2
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → (¬ (x <Q f ∨ f <Q x) → ((x
·Q y)
+Q (f
·Q z))
∈ (1st ‘(A ·P (B +P 𝐶))))) |
94 | | ltdcnq 6381 |
. . . . 5
⊢
((x ∈ Q ∧ f ∈ Q) → DECID
x <Q f) |
95 | | ltdcnq 6381 |
. . . . . 6
⊢
((f ∈ Q ∧ x ∈ Q) → DECID
f <Q x) |
96 | 95 | ancoms 255 |
. . . . 5
⊢
((x ∈ Q ∧ f ∈ Q) → DECID
f <Q x) |
97 | | dcor 842 |
. . . . 5
⊢
(DECID x
<Q f →
(DECID f
<Q x →
DECID (x
<Q f ∨ f
<Q x))) |
98 | 94, 96, 97 | sylc 56 |
. . . 4
⊢
((x ∈ Q ∧ f ∈ Q) → DECID
(x <Q f ∨ f <Q x)) |
99 | 8, 12, 98 | syl2anc 391 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → DECID (x <Q f ∨ f <Q x)) |
100 | | df-dc 742 |
. . 3
⊢
(DECID (x
<Q f ∨ f
<Q x) ↔
((x <Q f ∨ f <Q x) ∨ ¬
(x <Q f ∨ f <Q x))) |
101 | 99, 100 | sylib 127 |
. 2
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → ((x <Q f ∨ f <Q x) ∨ ¬
(x <Q f ∨ f <Q x))) |
102 | 82, 93, 101 | mpjaod 637 |
1
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1st ‘A) ∧ y ∈ (1st ‘B)) ∧ (f ∈
(1st ‘A) ∧ z ∈ (1st ‘𝐶)))) → ((x ·Q y) +Q (f ·Q z)) ∈
(1st ‘(A
·P (B
+P 𝐶)))) |