| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | addclpr 11059 | . . . . 5
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝐵
+P 𝐶) ∈ P) | 
| 2 |  | df-mp 11025 | . . . . . 6
⊢ 
·P = (𝑦 ∈ P, 𝑧 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑦 ∃ℎ ∈ 𝑧 𝑓 = (𝑔 ·Q ℎ)}) | 
| 3 |  | mulclnq 10988 | . . . . . 6
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
·Q ℎ) ∈ Q) | 
| 4 | 2, 3 | genpelv 11041 | . . . . 5
⊢ ((𝐴 ∈ P ∧
(𝐵
+P 𝐶) ∈ P) → (𝑤 ∈ (𝐴 ·P (𝐵 +P
𝐶)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝐵 +P 𝐶)𝑤 = (𝑥 ·Q 𝑣))) | 
| 5 | 1, 4 | sylan2 593 | . . . 4
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ 𝐶 ∈
P)) → (𝑤
∈ (𝐴
·P (𝐵 +P 𝐶)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝐵 +P 𝐶)𝑤 = (𝑥 ·Q 𝑣))) | 
| 6 | 5 | 3impb 1114 | . . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑤
∈ (𝐴
·P (𝐵 +P 𝐶)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝐵 +P 𝐶)𝑤 = (𝑥 ·Q 𝑣))) | 
| 7 |  | df-plp 11024 | . . . . . . . . . . 11
⊢ 
+P = (𝑤 ∈ P, 𝑥 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑤 ∃ℎ ∈ 𝑥 𝑓 = (𝑔 +Q ℎ)}) | 
| 8 |  | addclnq 10986 | . . . . . . . . . . 11
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) | 
| 9 | 7, 8 | genpelv 11041 | . . . . . . . . . 10
⊢ ((𝐵 ∈ P ∧
𝐶 ∈ P)
→ (𝑣 ∈ (𝐵 +P
𝐶) ↔ ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑣 = (𝑦 +Q 𝑧))) | 
| 10 | 9 | 3adant1 1130 | . . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑣
∈ (𝐵
+P 𝐶) ↔ ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑣 = (𝑦 +Q 𝑧))) | 
| 11 | 10 | adantr 480 | . . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) → (𝑣 ∈ (𝐵 +P 𝐶) ↔ ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑣 = (𝑦 +Q 𝑧))) | 
| 12 |  | simprr 772 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) → 𝑤 = (𝑥 ·Q 𝑣)) | 
| 13 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧)) → 𝑣 = (𝑦 +Q 𝑧)) | 
| 14 |  | oveq2 7440 | . . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑦 +Q 𝑧) → (𝑥 ·Q 𝑣) = (𝑥 ·Q (𝑦 +Q
𝑧))) | 
| 15 | 14 | eqeq2d 2747 | . . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑦 +Q 𝑧) → (𝑤 = (𝑥 ·Q 𝑣) ↔ 𝑤 = (𝑥 ·Q (𝑦 +Q
𝑧)))) | 
| 16 | 15 | biimpac 478 | . . . . . . . . . . . . 13
⊢ ((𝑤 = (𝑥 ·Q 𝑣) ∧ 𝑣 = (𝑦 +Q 𝑧)) → 𝑤 = (𝑥 ·Q (𝑦 +Q
𝑧))) | 
| 17 |  | distrnq 11002 | . . . . . . . . . . . . 13
⊢ (𝑥
·Q (𝑦 +Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) | 
| 18 | 16, 17 | eqtrdi 2792 | . . . . . . . . . . . 12
⊢ ((𝑤 = (𝑥 ·Q 𝑣) ∧ 𝑣 = (𝑦 +Q 𝑧)) → 𝑤 = ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧))) | 
| 19 | 12, 13, 18 | syl2an 596 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → 𝑤 = ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧))) | 
| 20 |  | mulclpr 11061 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴
·P 𝐵) ∈ P) | 
| 21 | 20 | 3adant3 1132 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐴
·P 𝐵) ∈ P) | 
| 22 | 21 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → (𝐴 ·P 𝐵) ∈
P) | 
| 23 |  | mulclpr 11061 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (𝐴
·P 𝐶) ∈ P) | 
| 24 | 23 | 3adant2 1131 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐴
·P 𝐶) ∈ P) | 
| 25 | 24 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → (𝐴 ·P 𝐶) ∈
P) | 
| 26 |  | simpll 766 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧)) → 𝑦 ∈ 𝐵) | 
| 27 | 2, 3 | genpprecl 11042 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 ·Q 𝑦) ∈ (𝐴 ·P 𝐵))) | 
| 28 | 27 | 3adant3 1132 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑥
∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 ·Q 𝑦) ∈ (𝐴 ·P 𝐵))) | 
| 29 | 28 | impl 455 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ 𝑥
∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑥 ·Q 𝑦) ∈ (𝐴 ·P 𝐵)) | 
| 30 | 29 | adantlrr 721 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ 𝑦 ∈ 𝐵) → (𝑥 ·Q 𝑦) ∈ (𝐴 ·P 𝐵)) | 
| 31 | 26, 30 | sylan2 593 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → (𝑥 ·Q 𝑦) ∈ (𝐴 ·P 𝐵)) | 
| 32 |  | simplr 768 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧)) → 𝑧 ∈ 𝐶) | 
| 33 | 2, 3 | genpprecl 11042 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶))) | 
| 34 | 33 | 3adant2 1131 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑥
∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶))) | 
| 35 | 34 | impl 455 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ 𝑥
∈ 𝐴) ∧ 𝑧 ∈ 𝐶) → (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶)) | 
| 36 | 35 | adantlrr 721 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ 𝑧 ∈ 𝐶) → (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶)) | 
| 37 | 32, 36 | sylan2 593 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶)) | 
| 38 | 7, 8 | genpprecl 11042 | . . . . . . . . . . . . 13
⊢ (((𝐴
·P 𝐵) ∈ P ∧ (𝐴
·P 𝐶) ∈ P) → (((𝑥
·Q 𝑦) ∈ (𝐴 ·P 𝐵) ∧ (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶)) → ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))) | 
| 39 | 38 | imp 406 | . . . . . . . . . . . 12
⊢ ((((𝐴
·P 𝐵) ∈ P ∧ (𝐴
·P 𝐶) ∈ P) ∧ ((𝑥
·Q 𝑦) ∈ (𝐴 ·P 𝐵) ∧ (𝑥 ·Q 𝑧) ∈ (𝐴 ·P 𝐶))) → ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) | 
| 40 | 22, 25, 31, 37, 39 | syl22anc 838 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → ((𝑥 ·Q 𝑦) +Q
(𝑥
·Q 𝑧)) ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) | 
| 41 | 19, 40 | eqeltrd 2840 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) ∧ 𝑣 = (𝑦 +Q 𝑧))) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) | 
| 42 | 41 | exp32 420 | . . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) → ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑣 = (𝑦 +Q 𝑧) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))))) | 
| 43 | 42 | rexlimdvv 3211 | . . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) → (∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑣 = (𝑦 +Q 𝑧) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))) | 
| 44 | 11, 43 | sylbid 240 | . . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝑥
∈ 𝐴 ∧ 𝑤 = (𝑥 ·Q 𝑣))) → (𝑣 ∈ (𝐵 +P 𝐶) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))) | 
| 45 | 44 | exp32 420 | . . . . . 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 410 | . . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝑥
∈ 𝐴 ∧ 𝑣 ∈ (𝐵 +P 𝐶)) → (𝑤 = (𝑥 ·Q 𝑣) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))))) | 
| 48 | 47 | rexlimdvv 3211 | . . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (∃𝑥 ∈ 𝐴 ∃𝑣 ∈ (𝐵 +P 𝐶)𝑤 = (𝑥 ·Q 𝑣) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))) | 
| 49 | 6, 48 | sylbid 240 | . 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝑤
∈ (𝐴
·P (𝐵 +P 𝐶)) → 𝑤 ∈ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶)))) | 
| 50 | 49 | ssrdv 3988 | 1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → (𝐴
·P (𝐵 +P 𝐶)) ⊆ ((𝐴 ·P 𝐵) +P
(𝐴
·P 𝐶))) |