Step | Hyp | Ref
| Expression |
1 | | mulclpr 10157 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴
·P 𝐵) ∈ P) |
2 | 1 | 3adant3 1168 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐴
·P 𝐵) ∈ P) |
3 | | mulclpr 10157 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (𝐴
·P 𝐶) ∈ P) |
4 | 3 | 3adant2 1167 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐴
·P 𝐶) ∈ P) |
5 | | df-plp 10120 |
. . . . 5
⊢
+P = (𝑥 ∈ P, 𝑦 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑥 ∃ℎ ∈ 𝑦 𝑓 = (𝑔 +Q ℎ)}) |
6 | | addclnq 10082 |
. . . . 5
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
7 | 5, 6 | genpelv 10137 |
. . . 4
⊢ (((𝐴
·P 𝐵) ∈ P ∧ (𝐴
·P 𝐶) ∈ P) → (𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)) ↔ ∃𝑣 ∈ (𝐴 ·P 𝐵)∃𝑢 ∈ (𝐴 ·P 𝐶)𝑤 = (𝑣 +Q 𝑢))) |
8 | 2, 4, 7 | syl2anc 581 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑤
∈ ((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)) ↔ ∃𝑣 ∈ (𝐴 ·P 𝐵)∃𝑢 ∈ (𝐴 ·P 𝐶)𝑤 = (𝑣 +Q 𝑢))) |
9 | | df-mp 10121 |
. . . . . . . 8
⊢
·P = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑔 ∈ 𝑤 ∃ℎ ∈ 𝑣 𝑥 = (𝑔 ·Q ℎ)}) |
10 | | mulclnq 10084 |
. . . . . . . 8
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
·Q ℎ) ∈ Q) |
11 | 9, 10 | genpelv 10137 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (𝑢 ∈ (𝐴
·P 𝐶) ↔ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧))) |
12 | 11 | 3adant2 1167 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑢
∈ (𝐴
·P 𝐶) ↔ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧))) |
13 | 12 | anbi2d 624 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑣
∈ (𝐴
·P 𝐵) ∧ 𝑢 ∈ (𝐴 ·P 𝐶)) ↔ (𝑣 ∈ (𝐴 ·P 𝐵) ∧ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧)))) |
14 | | df-mp 10121 |
. . . . . . . . 9
⊢
·P = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑤 ∃ℎ ∈ 𝑣 𝑓 = (𝑔 ·Q ℎ)}) |
15 | 14, 10 | genpelv 10137 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑣 ∈ (𝐴
·P 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦))) |
16 | 15 | 3adant3 1168 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑣
∈ (𝐴
·P 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦))) |
17 | | distrlem4pr 10163 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))) |
18 | | oveq12 6914 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑣 +Q 𝑢) = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧))) |
19 | 18 | eqeq2d 2835 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) ↔ 𝑤 = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)))) |
20 | | eleq1 2894 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
21 | 19, 20 | syl6bi 245 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))))) |
22 | 21 | imp 397 |
. . . . . . . . . . . . . . 15
⊢ (((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) ∧ 𝑤 = (𝑣 +Q 𝑢)) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
23 | 17, 22 | syl5ibrcom 239 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) ∧ 𝑤 = (𝑣 +Q 𝑢)) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
24 | 23 | exp4b 423 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) |
25 | 24 | com3l 89 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) |
26 | 25 | exp4b 423 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑣 = (𝑥 ·Q 𝑦) → (𝑢 = (𝑓 ·Q 𝑧) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))))) |
27 | 26 | com23 86 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑣 = (𝑥 ·Q 𝑦) → ((𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑢 = (𝑓 ·Q 𝑧) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))))) |
28 | 27 | rexlimivv 3246 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦) → ((𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑢 = (𝑓 ·Q 𝑧) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶))))))) |
29 | 28 | rexlimdvv 3247 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦) → (∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) |
30 | 29 | com3r 87 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦) → (∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) |
31 | 16, 30 | sylbid 232 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑣
∈ (𝐴
·P 𝐵) → (∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) |
32 | 31 | impd 400 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑣
∈ (𝐴
·P 𝐵) ∧ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶))))) |
33 | 13, 32 | sylbid 232 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑣
∈ (𝐴
·P 𝐵) ∧ 𝑢 ∈ (𝐴 ·P 𝐶)) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶))))) |
34 | 33 | rexlimdvv 3247 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑣 ∈ (𝐴 ·P 𝐵)∃𝑢 ∈ (𝐴 ·P 𝐶)𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
35 | 8, 34 | sylbid 232 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑤
∈ ((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
36 | 35 | ssrdv 3833 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)) ⊆ (𝐴 ·P (𝐵 +P
𝐶))) |