| Step | Hyp | Ref
| Expression |
| 1 | | simpl2 1193 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝐵 ∈ P) |
| 2 | | simprlr 780 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝑦 ∈ 𝐵) |
| 3 | | elprnq 11031 |
. . . . 5
⊢ ((𝐵 ∈ P ∧
𝑦 ∈ 𝐵) → 𝑦 ∈ Q) |
| 4 | 1, 2, 3 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝑦 ∈ Q) |
| 5 | | simp1 1137 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → 𝐴
∈ P) |
| 6 | | simprl 771 |
. . . . 5
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑓 ∈ 𝐴) |
| 7 | | elprnq 11031 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → 𝑓 ∈ Q) |
| 8 | 5, 6, 7 | syl2an 596 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝑓 ∈ Q) |
| 9 | | simpl3 1194 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝐶 ∈ P) |
| 10 | | simprrr 782 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝑧 ∈ 𝐶) |
| 11 | | elprnq 11031 |
. . . . 5
⊢ ((𝐶 ∈ P ∧
𝑧 ∈ 𝐶) → 𝑧 ∈ Q) |
| 12 | 9, 10, 11 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝑧 ∈ Q) |
| 13 | | vex 3484 |
. . . . . 6
⊢ 𝑥 ∈ V |
| 14 | | vex 3484 |
. . . . . 6
⊢ 𝑓 ∈ V |
| 15 | | ltmnq 11012 |
. . . . . 6
⊢ (𝑢 ∈ Q →
(𝑤
<Q 𝑣 ↔ (𝑢 ·Q 𝑤) <Q
(𝑢
·Q 𝑣))) |
| 16 | | vex 3484 |
. . . . . 6
⊢ 𝑦 ∈ V |
| 17 | | mulcomnq 10993 |
. . . . . 6
⊢ (𝑤
·Q 𝑣) = (𝑣 ·Q 𝑤) |
| 18 | 13, 14, 15, 16, 17 | caovord2 7645 |
. . . . 5
⊢ (𝑦 ∈ Q →
(𝑥
<Q 𝑓 ↔ (𝑥 ·Q 𝑦) <Q
(𝑓
·Q 𝑦))) |
| 19 | | mulclnq 10987 |
. . . . . 6
⊢ ((𝑓 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑓
·Q 𝑧) ∈ Q) |
| 20 | | ovex 7464 |
. . . . . . 7
⊢ (𝑥
·Q 𝑦) ∈ V |
| 21 | | ovex 7464 |
. . . . . . 7
⊢ (𝑓
·Q 𝑦) ∈ V |
| 22 | | ltanq 11011 |
. . . . . . 7
⊢ (𝑢 ∈ Q →
(𝑤
<Q 𝑣 ↔ (𝑢 +Q 𝑤) <Q
(𝑢
+Q 𝑣))) |
| 23 | | ovex 7464 |
. . . . . . 7
⊢ (𝑓
·Q 𝑧) ∈ V |
| 24 | | addcomnq 10991 |
. . . . . . 7
⊢ (𝑤 +Q
𝑣) = (𝑣 +Q 𝑤) |
| 25 | 20, 21, 22, 23, 24 | caovord2 7645 |
. . . . . 6
⊢ ((𝑓
·Q 𝑧) ∈ Q → ((𝑥
·Q 𝑦) <Q (𝑓
·Q 𝑦) ↔ ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)))) |
| 26 | 19, 25 | syl 17 |
. . . . 5
⊢ ((𝑓 ∈ Q ∧
𝑧 ∈ Q)
→ ((𝑥
·Q 𝑦) <Q (𝑓
·Q 𝑦) ↔ ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)))) |
| 27 | 18, 26 | sylan9bb 509 |
. . . 4
⊢ ((𝑦 ∈ Q ∧
(𝑓 ∈ Q
∧ 𝑧 ∈
Q)) → (𝑥
<Q 𝑓 ↔ ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)))) |
| 28 | 4, 8, 12, 27 | syl12anc 837 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝑥 <Q 𝑓 ↔ ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)))) |
| 29 | | simpl1 1192 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝐴 ∈ P) |
| 30 | | addclpr 11058 |
. . . . . . 7
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝐵
+P 𝐶) ∈ P) |
| 31 | 30 | 3adant1 1131 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐵
+P 𝐶) ∈ P) |
| 32 | 31 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝐵 +P 𝐶) ∈
P) |
| 33 | | mulclpr 11060 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) → (𝐴
·P (𝐵 +P 𝐶)) ∈
P) |
| 34 | 29, 32, 33 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝐴 ·P (𝐵 +P
𝐶)) ∈
P) |
| 35 | | distrnq 11001 |
. . . . 5
⊢ (𝑓
·Q (𝑦 +Q 𝑧)) = ((𝑓 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) |
| 36 | | simprrl 781 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝑓 ∈ 𝐴) |
| 37 | | df-plp 11023 |
. . . . . . . . 9
⊢
+P = (𝑢 ∈ P, 𝑣 ∈ P ↦ {𝑤 ∣ ∃𝑔 ∈ 𝑢 ∃ℎ ∈ 𝑣 𝑤 = (𝑔 +Q ℎ)}) |
| 38 | | addclnq 10985 |
. . . . . . . . 9
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
| 39 | 37, 38 | genpprecl 11041 |
. . . . . . . 8
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑦 +Q 𝑧) ∈ (𝐵 +P 𝐶))) |
| 40 | 39 | imp 406 |
. . . . . . 7
⊢ (((𝐵 ∈ P ∧
𝐶 ∈ P)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → (𝑦 +Q 𝑧) ∈ (𝐵 +P 𝐶)) |
| 41 | 1, 9, 2, 10, 40 | syl22anc 839 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝑦 +Q 𝑧) ∈ (𝐵 +P 𝐶)) |
| 42 | | df-mp 11024 |
. . . . . . . 8
⊢
·P = (𝑢 ∈ P, 𝑣 ∈ P ↦ {𝑤 ∣ ∃𝑔 ∈ 𝑢 ∃ℎ ∈ 𝑣 𝑤 = (𝑔 ·Q ℎ)}) |
| 43 | | mulclnq 10987 |
. . . . . . . 8
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
·Q ℎ) ∈ Q) |
| 44 | 42, 43 | genpprecl 11041 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) → ((𝑓 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ (𝐵 +P 𝐶)) → (𝑓 ·Q (𝑦 +Q
𝑧)) ∈ (𝐴
·P (𝐵 +P 𝐶)))) |
| 45 | 44 | imp 406 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) ∧ (𝑓 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ (𝐵 +P 𝐶))) → (𝑓 ·Q (𝑦 +Q
𝑧)) ∈ (𝐴
·P (𝐵 +P 𝐶))) |
| 46 | 29, 32, 36, 41, 45 | syl22anc 839 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝑓 ·Q (𝑦 +Q
𝑧)) ∈ (𝐴
·P (𝐵 +P 𝐶))) |
| 47 | 35, 46 | eqeltrrid 2846 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → ((𝑓 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))) |
| 48 | | prcdnq 11033 |
. . . 4
⊢ (((𝐴
·P (𝐵 +P 𝐶)) ∈ P ∧
((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))) → (((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) <Q ((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
| 49 | 34, 47, 48 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑓
·Q 𝑦) +Q (𝑓
·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
| 50 | 28, 49 | sylbid 240 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝑥 <Q 𝑓 → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
| 51 | | simpll 767 |
. . . . 5
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑥 ∈ 𝐴) |
| 52 | | elprnq 11031 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ 𝐴) → 𝑥 ∈ Q) |
| 53 | 5, 51, 52 | syl2an 596 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝑥 ∈ Q) |
| 54 | | vex 3484 |
. . . . . 6
⊢ 𝑧 ∈ V |
| 55 | 14, 13, 15, 54, 17 | caovord2 7645 |
. . . . 5
⊢ (𝑧 ∈ Q →
(𝑓
<Q 𝑥 ↔ (𝑓 ·Q 𝑧) <Q
(𝑥
·Q 𝑧))) |
| 56 | | mulclnq 10987 |
. . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
·Q 𝑦) ∈ Q) |
| 57 | | ltanq 11011 |
. . . . . 6
⊢ ((𝑥
·Q 𝑦) ∈ Q → ((𝑓
·Q 𝑧) <Q (𝑥
·Q 𝑧) ↔ ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)))) |
| 58 | 56, 57 | syl 17 |
. . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ((𝑓
·Q 𝑧) <Q (𝑥
·Q 𝑧) ↔ ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)))) |
| 59 | 55, 58 | sylan9bbr 510 |
. . . 4
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑧 ∈
Q) → (𝑓
<Q 𝑥 ↔ ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)))) |
| 60 | 53, 4, 12, 59 | syl21anc 838 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝑓 <Q 𝑥 ↔ ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)))) |
| 61 | | distrnq 11001 |
. . . . 5
⊢ (𝑥
·Q (𝑦 +Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) |
| 62 | | simprll 779 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → 𝑥 ∈ 𝐴) |
| 63 | 42, 43 | genpprecl 11041 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) → ((𝑥 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ (𝐵 +P 𝐶)) → (𝑥 ·Q (𝑦 +Q
𝑧)) ∈ (𝐴
·P (𝐵 +P 𝐶)))) |
| 64 | 63 | imp 406 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) ∧ (𝑥 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ (𝐵 +P 𝐶))) → (𝑥 ·Q (𝑦 +Q
𝑧)) ∈ (𝐴
·P (𝐵 +P 𝐶))) |
| 65 | 29, 32, 62, 41, 64 | syl22anc 839 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝑥 ·Q (𝑦 +Q
𝑧)) ∈ (𝐴
·P (𝐵 +P 𝐶))) |
| 66 | 61, 65 | eqeltrrid 2846 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))) |
| 67 | | prcdnq 11033 |
. . . 4
⊢ (((𝐴
·P (𝐵 +P 𝐶)) ∈ P ∧
((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))) → (((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
| 68 | 34, 66, 67 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) <Q ((𝑥
·Q 𝑦) +Q (𝑥
·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
| 69 | 60, 68 | sylbid 240 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝑓 <Q 𝑥 → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
| 70 | | ltsonq 11009 |
. . . . 5
⊢
<Q Or Q |
| 71 | | sotrieq 5623 |
. . . . 5
⊢ ((
<Q Or Q ∧ (𝑥 ∈ Q ∧ 𝑓 ∈ Q)) →
(𝑥 = 𝑓 ↔ ¬ (𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥))) |
| 72 | 70, 71 | mpan 690 |
. . . 4
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑥 = 𝑓 ↔ ¬ (𝑥 <Q
𝑓 ∨ 𝑓 <Q 𝑥))) |
| 73 | 53, 8, 72 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝑥 = 𝑓 ↔ ¬ (𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥))) |
| 74 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝑓 → (𝑥 ·Q 𝑧) = (𝑓 ·Q 𝑧)) |
| 75 | 74 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 = 𝑓 → ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧))) |
| 76 | 61, 75 | eqtrid 2789 |
. . . . 5
⊢ (𝑥 = 𝑓 → (𝑥 ·Q (𝑦 +Q
𝑧)) = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧))) |
| 77 | 76 | eleq1d 2826 |
. . . 4
⊢ (𝑥 = 𝑓 → ((𝑥 ·Q (𝑦 +Q
𝑧)) ∈ (𝐴
·P (𝐵 +P 𝐶)) ↔ ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
| 78 | 65, 77 | syl5ibcom 245 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (𝑥 = 𝑓 → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
| 79 | 73, 78 | sylbird 260 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (¬ (𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
| 80 | 50, 69, 79 | ecase3d 1035 |
1
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))) |