Step | Hyp | Ref
| Expression |
1 | | addclpr 10632 |
. . . . 5
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝐵
+P 𝐶) ∈ P) |
2 | | df-mp 10598 |
. . . . . 6
⊢
·P = (𝑦 ∈ P, 𝑧 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑦 ∃ℎ ∈ 𝑧 𝑓 = (𝑔 ·Q ℎ)}) |
3 | | mulclnq 10561 |
. . . . . 6
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
·Q ℎ) ∈ Q) |
4 | 2, 3 | genpelv 10614 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝐵 +P 𝐶)𝑤 = (𝑥 ·Q 𝑣))) |
5 | 1, 4 | sylan2 596 |
. . . 4
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ 𝐶 ∈
P)) → (𝑤
∈ (𝐴
·P (𝐵 +P 𝐶)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝐵 +P 𝐶)𝑤 = (𝑥 ·Q 𝑣))) |
6 | 5 | 3impb 1117 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑤
∈ (𝐴
·P (𝐵 +P 𝐶)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝐵 +P 𝐶)𝑤 = (𝑥 ·Q 𝑣))) |
7 | | df-plp 10597 |
. . . . . . . . . . 11
⊢
+P = (𝑤 ∈ P, 𝑥 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑤 ∃ℎ ∈ 𝑥 𝑓 = (𝑔 +Q ℎ)}) |
8 | | addclnq 10559 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
9 | 7, 8 | genpelv 10614 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑣 ∈ (𝐵 +P
𝐶) ↔ ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑣 = (𝑦 +Q 𝑧))) |
10 | 9 | 3adant1 1132 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑣
∈ (𝐵
+P 𝐶) ↔ ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑣 = (𝑦 +Q 𝑧))) |
11 | 10 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) → (𝑣 ∈ (𝐵 +P 𝐶) ↔ ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑣 = (𝑦 +Q 𝑧))) |
12 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) → 𝑤 = (𝑥 ·Q 𝑣)) |
13 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧)) → 𝑣 = (𝑦 +Q 𝑧)) |
14 | | oveq2 7221 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑦 +Q 𝑧) → (𝑥 ·Q 𝑣) = (𝑥 ·Q (𝑦 +Q
𝑧))) |
15 | 14 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑦 +Q 𝑧) → (𝑤 = (𝑥 ·Q 𝑣) ↔ 𝑤 = (𝑥 ·Q (𝑦 +Q
𝑧)))) |
16 | 15 | biimpac 482 |
. . . . . . . . . . . . 13
⊢ ((𝑤 = (𝑥 ·Q 𝑣) ∧ 𝑣 = (𝑦 +Q 𝑧)) → 𝑤 = (𝑥 ·Q (𝑦 +Q
𝑧))) |
17 | | distrnq 10575 |
. . . . . . . . . . . . 13
⊢ (𝑥
·Q (𝑦 +Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) |
18 | 16, 17 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ ((𝑤 = (𝑥 ·Q 𝑣) ∧ 𝑣 = (𝑦 +Q 𝑧)) → 𝑤 = ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧))) |
19 | 12, 13, 18 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → 𝑤 = ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧))) |
20 | | mulclpr 10634 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴
·P 𝐵) ∈ P) |
21 | 20 | 3adant3 1134 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐴
·P 𝐵) ∈ P) |
22 | 21 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → (𝐴 ·P 𝐵) ∈
P) |
23 | | mulclpr 10634 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (𝐴
·P 𝐶) ∈ P) |
24 | 23 | 3adant2 1133 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐴
·P 𝐶) ∈ P) |
25 | 24 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → (𝐴 ·P 𝐶) ∈
P) |
26 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧)) → 𝑦 ∈ 𝐵) |
27 | 2, 3 | genpprecl 10615 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 ·Q 𝑦) ∈ (𝐴 ·P 𝐵))) |
28 | 27 | 3adant3 1134 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 ·Q 𝑦) ∈ (𝐴 ·P 𝐵))) |
29 | 28 | impl 459 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ 𝑥
∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑥 ·Q 𝑦) ∈ (𝐴 ·P 𝐵)) |
30 | 29 | adantlrr 721 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ 𝑦 ∈ 𝐵) → (𝑥 ·Q 𝑦) ∈ (𝐴 ·P 𝐵)) |
31 | 26, 30 | sylan2 596 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → (𝑥 ·Q 𝑦) ∈ (𝐴 ·P 𝐵)) |
32 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧)) → 𝑧 ∈ 𝐶) |
33 | 2, 3 | genpprecl 10615 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶))) |
34 | 33 | 3adant2 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑥
∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶))) |
35 | 34 | impl 459 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ 𝑥
∈ 𝐴) ∧ 𝑧 ∈ 𝐶) → (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶)) |
36 | 35 | adantlrr 721 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ 𝑧 ∈ 𝐶) → (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶)) |
37 | 32, 36 | sylan2 596 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶)) |
38 | 7, 8 | genpprecl 10615 |
. . . . . . . . . . . . 13
⊢ (((𝐴
·P 𝐵) ∈ P ∧ (𝐴
·P 𝐶) ∈ P) → (((𝑥
·Q 𝑦) ∈ (𝐴 ·P 𝐵) ∧ (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶)) → ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))) |
39 | 38 | imp 410 |
. . . . . . . . . . . 12
⊢ ((((𝐴
·P 𝐵) ∈ P ∧ (𝐴
·P 𝐶) ∈ P) ∧ ((𝑥
·Q 𝑦) ∈ (𝐴 ·P 𝐵) ∧ (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶))) → ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) |
40 | 22, 25, 31, 37, 39 | syl22anc 839 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) |
41 | 19, 40 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) |
42 | 41 | exp32 424 |
. . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) → ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑣 = (𝑦 +Q 𝑧) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))))) |
43 | 42 | rexlimdvv 3212 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) → (∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑣 = (𝑦 +Q 𝑧) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))) |
44 | 11, 43 | sylbid 243 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) → (𝑣 ∈ (𝐵 +P 𝐶) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))) |
45 | 44 | exp32 424 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑥
∈ 𝐴 → (𝑤 = (𝑥 ·Q 𝑣) → (𝑣 ∈ (𝐵 +P 𝐶) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))))) |
46 | 45 | com34 91 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑥
∈ 𝐴 → (𝑣 ∈ (𝐵 +P 𝐶) → (𝑤 = (𝑥 ·Q 𝑣) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))))) |
47 | 46 | impd 414 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑥
∈ 𝐴 ∧ 𝑣 ∈ (𝐵 +P 𝐶)) → (𝑤 = (𝑥 ·Q 𝑣) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))))) |
48 | 47 | rexlimdvv 3212 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝐵 +P 𝐶)𝑤 = (𝑥 ·Q 𝑣) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))) |
49 | 6, 48 | sylbid 243 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑤
∈ (𝐴
·P (𝐵 +P 𝐶)) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))) |
50 | 49 | ssrdv 3907 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐴
·P (𝐵 +P 𝐶)) ⊆ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) |