Step | Hyp | Ref
| Expression |
1 | | mulclpr 10765 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴
·P 𝐵) ∈ P) |
2 | 1 | 3adant3 1131 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐴
·P 𝐵) ∈ P) |
3 | | mulclpr 10765 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (𝐴
·P 𝐶) ∈ P) |
4 | | df-plp 10728 |
. . . . 5
⊢
+P = (𝑥 ∈ P, 𝑦 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑥 ∃ℎ ∈ 𝑦 𝑓 = (𝑔 +Q ℎ)}) |
5 | | addclnq 10690 |
. . . . 5
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
6 | 4, 5 | genpelv 10745 |
. . . 4
⊢ (((𝐴
·P 𝐵) ∈ P ∧ (𝐴
·P 𝐶) ∈ P) → (𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)) ↔ ∃𝑣 ∈ (𝐴 ·P 𝐵)∃𝑢 ∈ (𝐴 ·P 𝐶)𝑤 = (𝑣 +Q 𝑢))) |
7 | 2, 3, 6 | 3imp3i2an 1344 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑤
∈ ((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)) ↔ ∃𝑣 ∈ (𝐴 ·P 𝐵)∃𝑢 ∈ (𝐴 ·P 𝐶)𝑤 = (𝑣 +Q 𝑢))) |
8 | | df-mp 10729 |
. . . . . . . 8
⊢
·P = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑔 ∈ 𝑤 ∃ℎ ∈ 𝑣 𝑥 = (𝑔 ·Q ℎ)}) |
9 | | mulclnq 10692 |
. . . . . . . 8
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
·Q ℎ) ∈ Q) |
10 | 8, 9 | genpelv 10745 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (𝑢 ∈ (𝐴
·P 𝐶) ↔ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧))) |
11 | 10 | 3adant2 1130 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑢
∈ (𝐴
·P 𝐶) ↔ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧))) |
12 | 11 | anbi2d 629 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑣
∈ (𝐴
·P 𝐵) ∧ 𝑢 ∈ (𝐴 ·P 𝐶)) ↔ (𝑣 ∈ (𝐴 ·P 𝐵) ∧ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧)))) |
13 | | df-mp 10729 |
. . . . . . . . 9
⊢
·P = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑤 ∃ℎ ∈ 𝑣 𝑓 = (𝑔 ·Q ℎ)}) |
14 | 13, 9 | genpelv 10745 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑣 ∈ (𝐴
·P 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦))) |
15 | 14 | 3adant3 1131 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑣
∈ (𝐴
·P 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦))) |
16 | | distrlem4pr 10771 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))) |
17 | | oveq12 7278 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑣 +Q 𝑢) = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧))) |
18 | 17 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) ↔ 𝑤 = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)))) |
19 | | eleq1 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
20 | 18, 19 | syl6bi 252 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))))) |
21 | 20 | imp 407 |
. . . . . . . . . . . . . . 15
⊢ (((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) ∧ 𝑤 = (𝑣 +Q 𝑢)) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
22 | 16, 21 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) ∧ 𝑤 = (𝑣 +Q 𝑢)) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
23 | 22 | exp4b 431 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) |
24 | 23 | com3l 89 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) |
25 | 24 | exp4b 431 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑣 = (𝑥 ·Q 𝑦) → (𝑢 = (𝑓 ·Q 𝑧) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))))) |
26 | 25 | com23 86 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑣 = (𝑥 ·Q 𝑦) → ((𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑢 = (𝑓 ·Q 𝑧) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))))) |
27 | 26 | rexlimivv 3220 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦) → ((𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑢 = (𝑓 ·Q 𝑧) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶))))))) |
28 | 27 | rexlimdvv 3221 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦) → (∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) |
29 | 28 | com3r 87 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦) → (∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) |
30 | 15, 29 | sylbid 239 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑣
∈ (𝐴
·P 𝐵) → (∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) |
31 | 30 | impd 411 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑣
∈ (𝐴
·P 𝐵) ∧ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶))))) |
32 | 12, 31 | sylbid 239 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑣
∈ (𝐴
·P 𝐵) ∧ 𝑢 ∈ (𝐴 ·P 𝐶)) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶))))) |
33 | 32 | rexlimdvv 3221 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑣 ∈ (𝐴 ·P 𝐵)∃𝑢 ∈ (𝐴 ·P 𝐶)𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
34 | 7, 33 | sylbid 239 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑤
∈ ((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))) |
35 | 34 | ssrdv 3928 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)) ⊆ (𝐴 ·P (𝐵 +P
𝐶))) |