| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mulclpr 11061 | . . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴
·P 𝐵) ∈ P) | 
| 2 | 1 | 3adant3 1132 | . . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐴
·P 𝐵) ∈ P) | 
| 3 |  | mulclpr 11061 | . . . 4
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (𝐴
·P 𝐶) ∈ P) | 
| 4 |  | df-plp 11024 | . . . . 5
⊢ 
+P = (𝑥 ∈ P, 𝑦 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑥 ∃ℎ ∈ 𝑦 𝑓 = (𝑔 +Q ℎ)}) | 
| 5 |  | addclnq 10986 | . . . . 5
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) | 
| 6 | 4, 5 | genpelv 11041 | . . . 4
⊢ (((𝐴
·P 𝐵) ∈ P ∧ (𝐴
·P 𝐶) ∈ P) → (𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)) ↔ ∃𝑣 ∈ (𝐴 ·P 𝐵)∃𝑢 ∈ (𝐴 ·P 𝐶)𝑤 = (𝑣 +Q 𝑢))) | 
| 7 | 2, 3, 6 | 3imp3i2an 1345 | . . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑤
∈ ((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)) ↔ ∃𝑣 ∈ (𝐴 ·P 𝐵)∃𝑢 ∈ (𝐴 ·P 𝐶)𝑤 = (𝑣 +Q 𝑢))) | 
| 8 |  | df-mp 11025 | . . . . . . . 8
⊢ 
·P = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑔 ∈ 𝑤 ∃ℎ ∈ 𝑣 𝑥 = (𝑔 ·Q ℎ)}) | 
| 9 |  | mulclnq 10988 | . . . . . . . 8
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
·Q ℎ) ∈ Q) | 
| 10 | 8, 9 | genpelv 11041 | . . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (𝑢 ∈ (𝐴
·P 𝐶) ↔ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧))) | 
| 11 | 10 | 3adant2 1131 | . . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑢
∈ (𝐴
·P 𝐶) ↔ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧))) | 
| 12 | 11 | anbi2d 630 | . . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑣
∈ (𝐴
·P 𝐵) ∧ 𝑢 ∈ (𝐴 ·P 𝐶)) ↔ (𝑣 ∈ (𝐴 ·P 𝐵) ∧ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧)))) | 
| 13 |  | df-mp 11025 | . . . . . . . . 9
⊢ 
·P = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑤 ∃ℎ ∈ 𝑣 𝑓 = (𝑔 ·Q ℎ)}) | 
| 14 | 13, 9 | genpelv 11041 | . . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑣 ∈ (𝐴
·P 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦))) | 
| 15 | 14 | 3adant3 1132 | . . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑣
∈ (𝐴
·P 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦))) | 
| 16 |  | distrlem4pr 11067 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))) | 
| 17 |  | oveq12 7441 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑣 +Q 𝑢) = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧))) | 
| 18 | 17 | eqeq2d 2747 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) ↔ 𝑤 = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)))) | 
| 19 |  | eleq1 2828 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = ((𝑥 ·Q 𝑦) +Q
(𝑓
·Q 𝑧)) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) | 
| 20 | 18, 19 | biimtrdi 253 | . . . . . . . . . . . . . . . 16
⊢ ((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶))))) | 
| 21 | 20 | imp 406 | . . . . . . . . . . . . . . 15
⊢ (((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) ∧ 𝑤 = (𝑣 +Q 𝑢)) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ((𝑥
·Q 𝑦) +Q (𝑓
·Q 𝑧)) ∈ (𝐴 ·P (𝐵 +P
𝐶)))) | 
| 22 | 16, 21 | syl5ibrcom 247 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶))) → (((𝑣 = (𝑥 ·Q 𝑦) ∧ 𝑢 = (𝑓 ·Q 𝑧)) ∧ 𝑤 = (𝑣 +Q 𝑢)) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))) | 
| 23 | 22 | exp4b 430 | . . . . . . . . . . . . 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 430 | . . . . . . . . . . 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 3200 | . . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑣 = (𝑥 ·Q 𝑦) → ((𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑢 = (𝑓 ·Q 𝑧) → ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑤 = (𝑣 +Q
𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶))))))) | 
| 28 | 27 | rexlimdvv 3211 | . . . . . . . 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 240 | . . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑣
∈ (𝐴
·P 𝐵) → (∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))))) | 
| 31 | 30 | impd 410 | . . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑣
∈ (𝐴
·P 𝐵) ∧ ∃𝑓 ∈ 𝐴 ∃𝑧 ∈ 𝐶 𝑢 = (𝑓 ·Q 𝑧)) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶))))) | 
| 32 | 12, 31 | sylbid 240 | . . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑣
∈ (𝐴
·P 𝐵) ∧ 𝑢 ∈ (𝐴 ·P 𝐶)) → (𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶))))) | 
| 33 | 32 | rexlimdvv 3211 | . . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑣 ∈ (𝐴 ·P 𝐵)∃𝑢 ∈ (𝐴 ·P 𝐶)𝑤 = (𝑣 +Q 𝑢) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))) | 
| 34 | 7, 33 | sylbid 240 | . 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑤
∈ ((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)) → 𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)))) | 
| 35 | 34 | ssrdv 3988 | 1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝐴
·P 𝐵) +P (𝐴
·P 𝐶)) ⊆ (𝐴 ·P (𝐵 +P
𝐶))) |