| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | addclprlem1 11056 | . . . . 5
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) ∈ 𝐴)) | 
| 2 | 1 | adantlr 715 | . . . 4
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) ∈ 𝐴)) | 
| 3 |  | addclprlem1 11056 | . . . . . 6
⊢ (((𝐵 ∈ P ∧
ℎ ∈ 𝐵) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(ℎ
+Q 𝑔) → ((𝑥 ·Q
(*Q‘(ℎ +Q 𝑔)))
·Q ℎ) ∈ 𝐵)) | 
| 4 |  | addcomnq 10991 | . . . . . . 7
⊢ (𝑔 +Q
ℎ) = (ℎ +Q 𝑔) | 
| 5 | 4 | breq2i 5151 | . . . . . 6
⊢ (𝑥 <Q
(𝑔
+Q ℎ) ↔ 𝑥 <Q (ℎ +Q
𝑔)) | 
| 6 | 4 | fveq2i 6909 | . . . . . . . . 9
⊢
(*Q‘(𝑔 +Q ℎ)) =
(*Q‘(ℎ +Q 𝑔)) | 
| 7 | 6 | oveq2i 7442 | . . . . . . . 8
⊢ (𝑥
·Q (*Q‘(𝑔 +Q
ℎ))) = (𝑥 ·Q
(*Q‘(ℎ +Q 𝑔))) | 
| 8 | 7 | oveq1i 7441 | . . . . . . 7
⊢ ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ) = ((𝑥 ·Q
(*Q‘(ℎ +Q 𝑔)))
·Q ℎ) | 
| 9 | 8 | eleq1i 2832 | . . . . . 6
⊢ (((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ) ∈ 𝐵 ↔ ((𝑥 ·Q
(*Q‘(ℎ +Q 𝑔)))
·Q ℎ) ∈ 𝐵) | 
| 10 | 3, 5, 9 | 3imtr4g 296 | . . . . 5
⊢ (((𝐵 ∈ P ∧
ℎ ∈ 𝐵) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q ℎ) ∈ 𝐵)) | 
| 11 | 10 | adantll 714 | . . . 4
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q ℎ) ∈ 𝐵)) | 
| 12 | 2, 11 | jcad 512 | . . 3
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → (((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) ∈ 𝐴 ∧ ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q ℎ) ∈ 𝐵))) | 
| 13 |  | simpl 482 | . . . 4
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → ((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵))) | 
| 14 |  | simpl 482 | . . . . 5
⊢ ((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) → 𝐴 ∈ P) | 
| 15 |  | simpl 482 | . . . . 5
⊢ ((𝐵 ∈ P ∧
ℎ ∈ 𝐵) → 𝐵 ∈ P) | 
| 16 | 14, 15 | anim12i 613 | . . . 4
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝐴 ∈ P ∧ 𝐵 ∈
P)) | 
| 17 |  | df-plp 11023 | . . . . 5
⊢ 
+P = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦 +Q 𝑧)}) | 
| 18 |  | addclnq 10985 | . . . . 5
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
+Q 𝑧) ∈ Q) | 
| 19 | 17, 18 | genpprecl 11041 | . . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q 𝑔) ∈ 𝐴 ∧ ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q ℎ) ∈ 𝐵) → (((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) ∈ (𝐴 +P 𝐵))) | 
| 20 | 13, 16, 19 | 3syl 18 | . . 3
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → ((((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q 𝑔) ∈ 𝐴 ∧ ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q ℎ) ∈ 𝐵) → (((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) ∈ (𝐴 +P 𝐵))) | 
| 21 | 12, 20 | syld 47 | . 2
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → (((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) ∈ (𝐴 +P 𝐵))) | 
| 22 |  | distrnq 11001 | . . . . 5
⊢ ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q (𝑔 +Q ℎ)) = (((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) | 
| 23 |  | mulassnq 10999 | . . . . 5
⊢ ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q (𝑔 +Q ℎ)) = (𝑥 ·Q
((*Q‘(𝑔 +Q ℎ))
·Q (𝑔 +Q ℎ))) | 
| 24 | 22, 23 | eqtr3i 2767 | . . . 4
⊢ (((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) = (𝑥 ·Q
((*Q‘(𝑔 +Q ℎ))
·Q (𝑔 +Q ℎ))) | 
| 25 |  | mulcomnq 10993 | . . . . . . 7
⊢
((*Q‘(𝑔 +Q ℎ))
·Q (𝑔 +Q ℎ)) = ((𝑔 +Q ℎ)
·Q (*Q‘(𝑔 +Q
ℎ))) | 
| 26 |  | elprnq 11031 | . . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) → 𝑔 ∈ Q) | 
| 27 |  | elprnq 11031 | . . . . . . . . 9
⊢ ((𝐵 ∈ P ∧
ℎ ∈ 𝐵) → ℎ ∈ Q) | 
| 28 | 26, 27 | anim12i 613 | . . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝑔 ∈ Q ∧ ℎ ∈
Q)) | 
| 29 |  | addclnq 10985 | . . . . . . . 8
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) | 
| 30 |  | recidnq 11005 | . . . . . . . 8
⊢ ((𝑔 +Q
ℎ) ∈ Q
→ ((𝑔
+Q ℎ) ·Q
(*Q‘(𝑔 +Q ℎ))) =
1Q) | 
| 31 | 28, 29, 30 | 3syl 18 | . . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → ((𝑔 +Q ℎ)
·Q (*Q‘(𝑔 +Q
ℎ))) =
1Q) | 
| 32 | 25, 31 | eqtrid 2789 | . . . . . 6
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) →
((*Q‘(𝑔 +Q ℎ))
·Q (𝑔 +Q ℎ)) =
1Q) | 
| 33 | 32 | oveq2d 7447 | . . . . 5
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝑥 ·Q
((*Q‘(𝑔 +Q ℎ))
·Q (𝑔 +Q ℎ))) = (𝑥 ·Q
1Q)) | 
| 34 |  | mulidnq 11003 | . . . . 5
⊢ (𝑥 ∈ Q →
(𝑥
·Q 1Q) = 𝑥) | 
| 35 | 33, 34 | sylan9eq 2797 | . . . 4
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥
·Q ((*Q‘(𝑔 +Q
ℎ))
·Q (𝑔 +Q ℎ))) = 𝑥) | 
| 36 | 24, 35 | eqtrid 2789 | . . 3
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) = 𝑥) | 
| 37 | 36 | eleq1d 2826 | . 2
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → ((((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) ∈ (𝐴 +P 𝐵) ↔ 𝑥 ∈ (𝐴 +P 𝐵))) | 
| 38 | 21, 37 | sylibd 239 | 1
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → 𝑥 ∈ (𝐴 +P 𝐵))) |