Step | Hyp | Ref
| Expression |
1 | | ltmnqg 6378 |
. . . . . . 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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) ∧
(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 ∈ (1^{st} ‘A) ∧ y ∈
(1^{st} ‘B)) ∧ (f ∈ (1^{st} ‘A) ∧ z ∈
(1^{st} ‘𝐶)))
→ x ∈ (1^{st} ‘A)) |
5 | | prop 6450 |
. . . . . . . 8
⊢ (A ∈
P → ⟨(1^{st} ‘A), (2^{nd} ‘A)⟩ ∈
P) |
6 | | elprnql 6456 |
. . . . . . . 8
⊢
((⟨(1^{st} ‘A),
(2^{nd} ‘A)⟩ ∈ P ∧ x ∈ (1^{st} ‘A)) → x
∈ Q) |
7 | 5, 6 | sylan 267 |
. . . . . . 7
⊢
((A ∈ P ∧ x ∈ (1^{st} ‘A)) → x
∈ Q) |
8 | 3, 4, 7 | syl2an 273 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → x ∈
Q) |
9 | | simprl 483 |
. . . . . . 7
⊢
(((x ∈ (1^{st} ‘A) ∧ y ∈
(1^{st} ‘B)) ∧ (f ∈ (1^{st} ‘A) ∧ z ∈
(1^{st} ‘𝐶)))
→ f ∈ (1^{st} ‘A)) |
10 | | elprnql 6456 |
. . . . . . . 8
⊢
((⟨(1^{st} ‘A),
(2^{nd} ‘A)⟩ ∈ P ∧ f ∈ (1^{st} ‘A)) → f
∈ Q) |
11 | 5, 10 | sylan 267 |
. . . . . . 7
⊢
((A ∈ P ∧ f ∈ (1^{st} ‘A)) → f
∈ Q) |
12 | 3, 9, 11 | syl2an 273 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → f ∈
Q) |
13 | | simpl2 907 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → B ∈
P) |
14 | | simprlr 490 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → y ∈
(1^{st} ‘B)) |
15 | | prop 6450 |
. . . . . . . 8
⊢ (B ∈
P → ⟨(1^{st} ‘B), (2^{nd} ‘B)⟩ ∈
P) |
16 | | elprnql 6456 |
. . . . . . . 8
⊢
((⟨(1^{st} ‘B),
(2^{nd} ‘B)⟩ ∈ P ∧ y ∈ (1^{st} ‘B)) → y
∈ Q) |
17 | 15, 16 | sylan 267 |
. . . . . . 7
⊢
((B ∈ P ∧ y ∈ (1^{st} ‘B)) → y
∈ Q) |
18 | 13, 14, 17 | syl2anc 391 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → y ∈
Q) |
19 | | mulcomnqg 6360 |
. . . . . . 7
⊢
((w ∈ Q ∧ v ∈ Q) → (w ·_{Q} v) = (v
·_{Q} w)) |
20 | 19 | adantl 262 |
. . . . . 6
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) ∧
(w ∈
Q ∧ v ∈
Q)) → (w
·_{Q} v) =
(v ·_{Q}
w)) |
21 | 2, 8, 12, 18, 20 | caovord2d 5609 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (x <_{Q} f ↔ (x
·_{Q} y)
<_{Q} (f
·_{Q} y))) |
22 | | ltanqg 6377 |
. . . . . . 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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) ∧
(w ∈
Q ∧ v ∈
Q ∧ u ∈
Q)) → (w
<_{Q} v ↔
(u +_{Q} w) <_{Q} (u +_{Q} v))) |
24 | | mulclnq 6353 |
. . . . . . 7
⊢
((x ∈ Q ∧ y ∈ Q) → (x ·_{Q} y) ∈
Q) |
25 | 8, 18, 24 | syl2anc 391 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (x ·_{Q} y) ∈
Q) |
26 | | mulclnq 6353 |
. . . . . . 7
⊢
((f ∈ Q ∧ y ∈ Q) → (f ·_{Q} y) ∈
Q) |
27 | 12, 18, 26 | syl2anc 391 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (f ·_{Q} y) ∈
Q) |
28 | | simpl3 908 |
. . . . . . . 8
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → 𝐶 ∈
P) |
29 | | simprrr 492 |
. . . . . . . 8
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → z ∈
(1^{st} ‘𝐶)) |
30 | | prop 6450 |
. . . . . . . . 9
⊢ (𝐶 ∈ P → ⟨(1^{st}
‘𝐶), (2^{nd}
‘𝐶)⟩ ∈ P) |
31 | | elprnql 6456 |
. . . . . . . . 9
⊢
((⟨(1^{st} ‘𝐶), (2^{nd} ‘𝐶)⟩ ∈
P ∧ z ∈
(1^{st} ‘𝐶))
→ z ∈ Q) |
32 | 30, 31 | sylan 267 |
. . . . . . . 8
⊢ ((𝐶 ∈ P ∧ z ∈ (1^{st} ‘𝐶)) → z ∈
Q) |
33 | 28, 29, 32 | syl2anc 391 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → z ∈
Q) |
34 | | mulclnq 6353 |
. . . . . . 7
⊢
((f ∈ Q ∧ z ∈ Q) → (f ·_{Q} z) ∈
Q) |
35 | 12, 33, 34 | syl2anc 391 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (f ·_{Q} z) ∈
Q) |
36 | | addcomnqg 6358 |
. . . . . . 7
⊢
((w ∈ Q ∧ v ∈ Q) → (w +_{Q} v) = (v
+_{Q} w)) |
37 | 36 | adantl 262 |
. . . . . 6
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) ∧
(w ∈
Q ∧ v ∈
Q)) → (w
+_{Q} v) = (v +_{Q} w)) |
38 | 23, 25, 27, 35, 37 | caovord2d 5609 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → ((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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → A ∈
P) |
41 | | addclpr 6513 |
. . . . . . . 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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (B +_{P} 𝐶) ∈
P) |
44 | | mulclpr 6543 |
. . . . . 6
⊢
((A ∈ P ∧ (B
+_{P} 𝐶) ∈
P) → (A
·_{P} (B
+_{P} 𝐶)) ∈
P) |
45 | 40, 43, 44 | syl2anc 391 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (A ·_{P} (B +_{P} 𝐶)) ∈
P) |
46 | | distrnqg 6364 |
. . . . . . 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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (f ·_{Q} (y +_{Q} z)) = ((f
·_{Q} y)
+_{Q} (f
·_{Q} z))) |
48 | | simprrl 491 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → f ∈
(1^{st} ‘A)) |
49 | | df-iplp 6443 |
. . . . . . . . . 10
⊢
+_{P} = (u ∈ P, v ∈
P ↦ ⟨{w ∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(1^{st} ‘u) ∧ ℎ
∈ (1^{st} ‘v) ∧ w = (g
+_{Q} ℎ))}, {w
∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(2^{nd} ‘u) ∧ ℎ
∈ (2^{nd} ‘v) ∧ w = (g
+_{Q} ℎ))}⟩) |
50 | | addclnq 6352 |
. . . . . . . . . 10
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (g +_{Q} ℎ) ∈
Q) |
51 | 49, 50 | genpprecll 6489 |
. . . . . . . . 9
⊢
((B ∈ P ∧ 𝐶 ∈
P) → ((y ∈ (1^{st} ‘B) ∧ z ∈
(1^{st} ‘𝐶))
→ (y +_{Q}
z) ∈
(1^{st} ‘(B
+_{P} 𝐶)))) |
52 | 51 | imp 115 |
. . . . . . . 8
⊢
(((B ∈ P ∧ 𝐶 ∈
P) ∧ (y ∈
(1^{st} ‘B) ∧ z ∈ (1^{st} ‘𝐶))) → (y +_{Q} z) ∈
(1^{st} ‘(B
+_{P} 𝐶))) |
53 | 13, 28, 14, 29, 52 | syl22anc 1135 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (y +_{Q} z) ∈
(1^{st} ‘(B
+_{P} 𝐶))) |
54 | | df-imp 6444 |
. . . . . . . . 9
⊢
·_{P} = (u
∈ P, v ∈
P ↦ ⟨{w ∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(1^{st} ‘u) ∧ ℎ
∈ (1^{st} ‘v) ∧ w = (g
·_{Q} ℎ))}, {w
∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(2^{nd} ‘u) ∧ ℎ
∈ (2^{nd} ‘v) ∧ w = (g
·_{Q} ℎ))}⟩) |
55 | | mulclnq 6353 |
. . . . . . . . 9
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (g ·_{Q} ℎ) ∈
Q) |
56 | 54, 55 | genpprecll 6489 |
. . . . . . . 8
⊢
((A ∈ P ∧ (B
+_{P} 𝐶) ∈
P) → ((f ∈ (1^{st} ‘A) ∧ (y +_{Q} z) ∈
(1^{st} ‘(B
+_{P} 𝐶))) → (f ·_{Q} (y +_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶))))) |
57 | 56 | imp 115 |
. . . . . . 7
⊢
(((A ∈ P ∧ (B
+_{P} 𝐶) ∈
P) ∧ (f ∈
(1^{st} ‘A) ∧ (y
+_{Q} z) ∈ (1^{st} ‘(B +_{P} 𝐶)))) → (f ·_{Q} (y +_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶)))) |
58 | 40, 43, 48, 53, 57 | syl22anc 1135 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (f ·_{Q} (y +_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶)))) |
59 | 47, 58 | eqeltrrd 2112 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → ((f ·_{Q} y) +_{Q} (f ·_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶)))) |
60 | | prop 6450 |
. . . . . 6
⊢
((A
·_{P} (B
+_{P} 𝐶)) ∈
P → ⟨(1^{st} ‘(A ·_{P} (B +_{P} 𝐶))), (2^{nd} ‘(A ·_{P} (B +_{P} 𝐶)))⟩ ∈ P) |
61 | | prcdnql 6459 |
. . . . . 6
⊢
((⟨(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶))), (2^{nd} ‘(A ·_{P} (B +_{P} 𝐶)))⟩ ∈ P ∧ ((f
·_{Q} y)
+_{Q} (f
·_{Q} z))
∈ (1^{st} ‘(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))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))))) |
62 | 60, 61 | sylan 267 |
. . . . 5
⊢
(((A
·_{P} (B
+_{P} 𝐶)) ∈
P ∧ ((f ·_{Q} y) +_{Q} (f ·_{Q} z)) ∈
(1^{st} ‘(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))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))))) |
63 | 45, 59, 62 | syl2anc 391 |
. . . 4
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (((x ·_{Q} y) +_{Q} (f ·_{Q} z)) <_{Q} ((f ·_{Q} y) +_{Q} (f ·_{Q} z)) → ((x
·_{Q} y)
+_{Q} (f
·_{Q} z))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))))) |
64 | 39, 63 | sylbid 139 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (x <_{Q} f → ((x
·_{Q} y)
+_{Q} (f
·_{Q} z))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))))) |
65 | 2, 12, 8, 33, 20 | caovord2d 5609 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (f <_{Q} x ↔ (f
·_{Q} z)
<_{Q} (x
·_{Q} z))) |
66 | | mulclnq 6353 |
. . . . . . 7
⊢
((x ∈ Q ∧ z ∈ Q) → (x ·_{Q} z) ∈
Q) |
67 | 8, 33, 66 | syl2anc 391 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (x ·_{Q} z) ∈
Q) |
68 | | ltanqg 6377 |
. . . . . 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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → ((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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (f <_{Q} x ↔ ((x
·_{Q} y)
+_{Q} (f
·_{Q} z))
<_{Q} ((x
·_{Q} y)
+_{Q} (x
·_{Q} z)))) |
71 | | distrnqg 6364 |
. . . . . . 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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (x ·_{Q} (y +_{Q} z)) = ((x
·_{Q} y)
+_{Q} (x
·_{Q} z))) |
73 | | simprll 489 |
. . . . . . 7
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → x ∈
(1^{st} ‘A)) |
74 | 54, 55 | genpprecll 6489 |
. . . . . . . 8
⊢
((A ∈ P ∧ (B
+_{P} 𝐶) ∈
P) → ((x ∈ (1^{st} ‘A) ∧ (y +_{Q} z) ∈
(1^{st} ‘(B
+_{P} 𝐶))) → (x ·_{Q} (y +_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶))))) |
75 | 74 | imp 115 |
. . . . . . 7
⊢
(((A ∈ P ∧ (B
+_{P} 𝐶) ∈
P) ∧ (x ∈
(1^{st} ‘A) ∧ (y
+_{Q} z) ∈ (1^{st} ‘(B +_{P} 𝐶)))) → (x ·_{Q} (y +_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶)))) |
76 | 40, 43, 73, 53, 75 | syl22anc 1135 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (x ·_{Q} (y +_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶)))) |
77 | 72, 76 | eqeltrrd 2112 |
. . . . 5
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → ((x ·_{Q} y) +_{Q} (x ·_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶)))) |
78 | | prcdnql 6459 |
. . . . . 6
⊢
((⟨(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶))), (2^{nd} ‘(A ·_{P} (B +_{P} 𝐶)))⟩ ∈ P ∧ ((x
·_{Q} y)
+_{Q} (x
·_{Q} z))
∈ (1^{st} ‘(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))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))))) |
79 | 60, 78 | sylan 267 |
. . . . 5
⊢
(((A
·_{P} (B
+_{P} 𝐶)) ∈
P ∧ ((x ·_{Q} y) +_{Q} (x ·_{Q} z)) ∈
(1^{st} ‘(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))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))))) |
80 | 45, 77, 79 | syl2anc 391 |
. . . 4
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (((x ·_{Q} y) +_{Q} (f ·_{Q} z)) <_{Q} ((x ·_{Q} y) +_{Q} (x ·_{Q} z)) → ((x
·_{Q} y)
+_{Q} (f
·_{Q} z))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))))) |
81 | 70, 80 | sylbid 139 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (f <_{Q} x → ((x
·_{Q} y)
+_{Q} (f
·_{Q} z))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))))) |
82 | 64, 81 | jaod 636 |
. 2
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → ((x <_{Q} f ∨ f <_{Q} x) → ((x
·_{Q} y)
+_{Q} (f
·_{Q} z))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))))) |
83 | | ltsonq 6375 |
. . . . 5
⊢
<_{Q} Or Q |
84 | | nqtri3or 6373 |
. . . . 5
⊢
((x ∈ Q ∧ f ∈ Q) → (x <_{Q} f ∨ x = f ∨ f
<_{Q} x)) |
85 | 83, 84 | sotritrieq 4052 |
. . . 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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (x = f ↔
¬ (x <_{Q}
f ∨
f <_{Q} x))) |
87 | | oveq1 5459 |
. . . . . . 7
⊢ (x = f →
(x ·_{Q}
z) = (f
·_{Q} z)) |
88 | 87 | oveq2d 5468 |
. . . . . 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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) ∧
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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) ∧
x = f)
→ (x
·_{Q} (y
+_{Q} z)) ∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶)))) |
91 | 89, 90 | eqeltrrd 2112 |
. . . 4
⊢
((((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) ∧
x = f)
→ ((x
·_{Q} y)
+_{Q} (f
·_{Q} z))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶)))) |
92 | 91 | ex 108 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (x = f →
((x ·_{Q}
y) +_{Q} (f ·_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶))))) |
93 | 86, 92 | sylbird 159 |
. 2
⊢
(((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈
P) ∧ ((x ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → (¬ (x <_{Q} f ∨ f <_{Q} x) → ((x
·_{Q} y)
+_{Q} (f
·_{Q} z))
∈ (1^{st} ‘(A ·_{P} (B +_{P} 𝐶))))) |
94 | | ltdcnq 6374 |
. . . . 5
⊢
((x ∈ Q ∧ f ∈ Q) → DECID
x <_{Q} f) |
95 | | ltdcnq 6374 |
. . . . . 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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → 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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → ((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 ∈
(1^{st} ‘A) ∧ y ∈ (1^{st} ‘B)) ∧ (f ∈
(1^{st} ‘A) ∧ z ∈ (1^{st} ‘𝐶)))) → ((x ·_{Q} y) +_{Q} (f ·_{Q} z)) ∈
(1^{st} ‘(A
·_{P} (B
+_{P} 𝐶)))) |