Metamath Proof Explorer

Theorem distrlem4pr

Description: Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996) (Revised by Mario Carneiro, 14-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion distrlem4pr ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )

Proof

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 𝐶 ) ) )