Step |
Hyp |
Ref |
Expression |
1 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝐵 ∈ P ) |
2 |
|
simprlr |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝑦 ∈ 𝐵 ) |
3 |
|
elprnq |
⊢ ( ( 𝐵 ∈ P ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ Q ) |
4 |
1 2 3
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝑦 ∈ Q ) |
5 |
|
simp1 |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → 𝐴 ∈ P ) |
6 |
|
simprl |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑓 ∈ 𝐴 ) |
7 |
|
elprnq |
⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ Q ) |
8 |
5 6 7
|
syl2an |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝑓 ∈ Q ) |
9 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝐶 ∈ P ) |
10 |
|
simprrr |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝑧 ∈ 𝐶 ) |
11 |
|
elprnq |
⊢ ( ( 𝐶 ∈ P ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ Q ) |
12 |
9 10 11
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝑧 ∈ Q ) |
13 |
|
vex |
⊢ 𝑥 ∈ V |
14 |
|
vex |
⊢ 𝑓 ∈ V |
15 |
|
ltmnq |
⊢ ( 𝑢 ∈ Q → ( 𝑤 <Q 𝑣 ↔ ( 𝑢 ·Q 𝑤 ) <Q ( 𝑢 ·Q 𝑣 ) ) ) |
16 |
|
vex |
⊢ 𝑦 ∈ V |
17 |
|
mulcomnq |
⊢ ( 𝑤 ·Q 𝑣 ) = ( 𝑣 ·Q 𝑤 ) |
18 |
13 14 15 16 17
|
caovord2 |
⊢ ( 𝑦 ∈ Q → ( 𝑥 <Q 𝑓 ↔ ( 𝑥 ·Q 𝑦 ) <Q ( 𝑓 ·Q 𝑦 ) ) ) |
19 |
|
mulclnq |
⊢ ( ( 𝑓 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑓 ·Q 𝑧 ) ∈ Q ) |
20 |
|
ovex |
⊢ ( 𝑥 ·Q 𝑦 ) ∈ V |
21 |
|
ovex |
⊢ ( 𝑓 ·Q 𝑦 ) ∈ V |
22 |
|
ltanq |
⊢ ( 𝑢 ∈ Q → ( 𝑤 <Q 𝑣 ↔ ( 𝑢 +Q 𝑤 ) <Q ( 𝑢 +Q 𝑣 ) ) ) |
23 |
|
ovex |
⊢ ( 𝑓 ·Q 𝑧 ) ∈ V |
24 |
|
addcomnq |
⊢ ( 𝑤 +Q 𝑣 ) = ( 𝑣 +Q 𝑤 ) |
25 |
20 21 22 23 24
|
caovord2 |
⊢ ( ( 𝑓 ·Q 𝑧 ) ∈ Q → ( ( 𝑥 ·Q 𝑦 ) <Q ( 𝑓 ·Q 𝑦 ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) ) |
26 |
19 25
|
syl |
⊢ ( ( 𝑓 ∈ Q ∧ 𝑧 ∈ Q ) → ( ( 𝑥 ·Q 𝑦 ) <Q ( 𝑓 ·Q 𝑦 ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) ) |
27 |
18 26
|
sylan9bb |
⊢ ( ( 𝑦 ∈ Q ∧ ( 𝑓 ∈ Q ∧ 𝑧 ∈ Q ) ) → ( 𝑥 <Q 𝑓 ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) ) |
28 |
4 8 12 27
|
syl12anc |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝑥 <Q 𝑓 ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) ) |
29 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝐴 ∈ P ) |
30 |
|
addclpr |
⊢ ( ( 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐵 +P 𝐶 ) ∈ P ) |
31 |
30
|
3adant1 |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐵 +P 𝐶 ) ∈ P ) |
32 |
31
|
adantr |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝐵 +P 𝐶 ) ∈ P ) |
33 |
|
mulclpr |
⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) → ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ∈ P ) |
34 |
29 32 33
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ∈ P ) |
35 |
|
distrnq |
⊢ ( 𝑓 ·Q ( 𝑦 +Q 𝑧 ) ) = ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) |
36 |
|
simprrl |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝑓 ∈ 𝐴 ) |
37 |
|
df-plp |
⊢ +P = ( 𝑢 ∈ P , 𝑣 ∈ P ↦ { 𝑤 ∣ ∃ 𝑔 ∈ 𝑢 ∃ ℎ ∈ 𝑣 𝑤 = ( 𝑔 +Q ℎ ) } ) |
38 |
|
addclnq |
⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑔 +Q ℎ ) ∈ Q ) |
39 |
37 38
|
genpprecl |
⊢ ( ( 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) ) |
40 |
39
|
imp |
⊢ ( ( ( 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) |
41 |
1 9 2 10 40
|
syl22anc |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) |
42 |
|
df-mp |
⊢ ·P = ( 𝑢 ∈ P , 𝑣 ∈ P ↦ { 𝑤 ∣ ∃ 𝑔 ∈ 𝑢 ∃ ℎ ∈ 𝑣 𝑤 = ( 𝑔 ·Q ℎ ) } ) |
43 |
|
mulclnq |
⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑔 ·Q ℎ ) ∈ Q ) |
44 |
42 43
|
genpprecl |
⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) → ( ( 𝑓 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) → ( 𝑓 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) |
45 |
44
|
imp |
⊢ ( ( ( 𝐴 ∈ P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) ∧ ( 𝑓 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) ) → ( 𝑓 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) |
46 |
29 32 36 41 45
|
syl22anc |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝑓 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) |
47 |
35 46
|
eqeltrrid |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) |
48 |
|
prcdnq |
⊢ ( ( ( 𝐴 ·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 |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) |
50 |
28 49
|
sylbid |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝑥 <Q 𝑓 → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) |
51 |
|
simpll |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑥 ∈ 𝐴 ) |
52 |
|
elprnq |
⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ Q ) |
53 |
5 51 52
|
syl2an |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝑥 ∈ Q ) |
54 |
|
vex |
⊢ 𝑧 ∈ V |
55 |
14 13 15 54 17
|
caovord2 |
⊢ ( 𝑧 ∈ Q → ( 𝑓 <Q 𝑥 ↔ ( 𝑓 ·Q 𝑧 ) <Q ( 𝑥 ·Q 𝑧 ) ) ) |
56 |
|
mulclnq |
⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 ·Q 𝑦 ) ∈ Q ) |
57 |
|
ltanq |
⊢ ( ( 𝑥 ·Q 𝑦 ) ∈ Q → ( ( 𝑓 ·Q 𝑧 ) <Q ( 𝑥 ·Q 𝑧 ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ) ) |
58 |
56 57
|
syl |
⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ( ( 𝑓 ·Q 𝑧 ) <Q ( 𝑥 ·Q 𝑧 ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ) ) |
59 |
55 58
|
sylan9bbr |
⊢ ( ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑧 ∈ Q ) → ( 𝑓 <Q 𝑥 ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ) ) |
60 |
53 4 12 59
|
syl21anc |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝑓 <Q 𝑥 ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ) ) |
61 |
|
distrnq |
⊢ ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) |
62 |
|
simprll |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → 𝑥 ∈ 𝐴 ) |
63 |
42 43
|
genpprecl |
⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) → ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) → ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) |
64 |
63
|
imp |
⊢ ( ( ( 𝐴 ∈ P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) ) → ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) |
65 |
29 32 62 41 64
|
syl22anc |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) |
66 |
61 65
|
eqeltrrid |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) |
67 |
|
prcdnq |
⊢ ( ( ( 𝐴 ·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 |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) |
69 |
60 68
|
sylbid |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝑓 <Q 𝑥 → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) |
70 |
|
ltsonq |
⊢ <Q Or Q |
71 |
|
sotrieq |
⊢ ( ( <Q Or Q ∧ ( 𝑥 ∈ Q ∧ 𝑓 ∈ Q ) ) → ( 𝑥 = 𝑓 ↔ ¬ ( 𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥 ) ) ) |
72 |
70 71
|
mpan |
⊢ ( ( 𝑥 ∈ Q ∧ 𝑓 ∈ Q ) → ( 𝑥 = 𝑓 ↔ ¬ ( 𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥 ) ) ) |
73 |
53 8 72
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝑥 = 𝑓 ↔ ¬ ( 𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥 ) ) ) |
74 |
|
oveq1 |
⊢ ( 𝑥 = 𝑓 → ( 𝑥 ·Q 𝑧 ) = ( 𝑓 ·Q 𝑧 ) ) |
75 |
74
|
oveq2d |
⊢ ( 𝑥 = 𝑓 → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) |
76 |
61 75
|
eqtrid |
⊢ ( 𝑥 = 𝑓 → ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) |
77 |
76
|
eleq1d |
⊢ ( 𝑥 = 𝑓 → ( ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) |
78 |
65 77
|
syl5ibcom |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( 𝑥 = 𝑓 → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) |
79 |
73 78
|
sylbird |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( ¬ ( 𝑥 <Q 𝑓 ∨ 𝑓 <Q 𝑥 ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) |
80 |
50 69 79
|
ecase3d |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) |