Step | Hyp | Ref
| Expression |
1 | | addclprlem1 10760 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) ∈ 𝐴)) |
2 | 1 | adantlr 712 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) ∈ 𝐴)) |
3 | | addclprlem1 10760 |
. . . . . 6
⊢ (((𝐵 ∈ P ∧
ℎ ∈ 𝐵) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(ℎ
+Q 𝑔) → ((𝑥 ·Q
(*Q‘(ℎ +Q 𝑔)))
·Q ℎ) ∈ 𝐵)) |
4 | | addcomnq 10695 |
. . . . . . 7
⊢ (𝑔 +Q
ℎ) = (ℎ +Q 𝑔) |
5 | 4 | breq2i 5082 |
. . . . . 6
⊢ (𝑥 <Q
(𝑔
+Q ℎ) ↔ 𝑥 <Q (ℎ +Q
𝑔)) |
6 | 4 | fveq2i 6770 |
. . . . . . . . 9
⊢
(*Q‘(𝑔 +Q ℎ)) =
(*Q‘(ℎ +Q 𝑔)) |
7 | 6 | oveq2i 7279 |
. . . . . . . 8
⊢ (𝑥
·Q (*Q‘(𝑔 +Q
ℎ))) = (𝑥 ·Q
(*Q‘(ℎ +Q 𝑔))) |
8 | 7 | oveq1i 7278 |
. . . . . . 7
⊢ ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ) = ((𝑥 ·Q
(*Q‘(ℎ +Q 𝑔)))
·Q ℎ) |
9 | 8 | eleq1i 2829 |
. . . . . 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 711 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q ℎ) ∈ 𝐵)) |
12 | 2, 11 | jcad 513 |
. . 3
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → (((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) ∈ 𝐴 ∧ ((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q ℎ) ∈ 𝐵))) |
13 | | simpl 483 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → ((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵))) |
14 | | simpl 483 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) → 𝐴 ∈ P) |
15 | | simpl 483 |
. . . . 5
⊢ ((𝐵 ∈ P ∧
ℎ ∈ 𝐵) → 𝐵 ∈ P) |
16 | 14, 15 | anim12i 613 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
17 | | df-plp 10727 |
. . . . 5
⊢
+P = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦 +Q 𝑧)}) |
18 | | addclnq 10689 |
. . . . 5
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
+Q 𝑧) ∈ Q) |
19 | 17, 18 | genpprecl 10745 |
. . . 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 10705 |
. . . . 5
⊢ ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q (𝑔 +Q ℎ)) = (((𝑥 ·Q
(*Q‘(𝑔 +Q ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) |
23 | | mulassnq 10703 |
. . . . 5
⊢ ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q (𝑔 +Q ℎ)) = (𝑥 ·Q
((*Q‘(𝑔 +Q ℎ))
·Q (𝑔 +Q ℎ))) |
24 | 22, 23 | eqtr3i 2768 |
. . . 4
⊢ (((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) = (𝑥 ·Q
((*Q‘(𝑔 +Q ℎ))
·Q (𝑔 +Q ℎ))) |
25 | | mulcomnq 10697 |
. . . . . . 7
⊢
((*Q‘(𝑔 +Q ℎ))
·Q (𝑔 +Q ℎ)) = ((𝑔 +Q ℎ)
·Q (*Q‘(𝑔 +Q
ℎ))) |
26 | | elprnq 10735 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) → 𝑔 ∈ Q) |
27 | | elprnq 10735 |
. . . . . . . . 9
⊢ ((𝐵 ∈ P ∧
ℎ ∈ 𝐵) → ℎ ∈ Q) |
28 | 26, 27 | anim12i 613 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝑔 ∈ Q ∧ ℎ ∈
Q)) |
29 | | addclnq 10689 |
. . . . . . . 8
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
30 | | recidnq 10709 |
. . . . . . . 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 2790 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) →
((*Q‘(𝑔 +Q ℎ))
·Q (𝑔 +Q ℎ)) =
1Q) |
33 | 32 | oveq2d 7284 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝑥 ·Q
((*Q‘(𝑔 +Q ℎ))
·Q (𝑔 +Q ℎ))) = (𝑥 ·Q
1Q)) |
34 | | mulidnq 10707 |
. . . . 5
⊢ (𝑥 ∈ Q →
(𝑥
·Q 1Q) = 𝑥) |
35 | 33, 34 | sylan9eq 2798 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥
·Q ((*Q‘(𝑔 +Q
ℎ))
·Q (𝑔 +Q ℎ))) = 𝑥) |
36 | 24, 35 | eqtrid 2790 |
. . 3
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) = 𝑥) |
37 | 36 | eleq1d 2823 |
. 2
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → ((((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q 𝑔) +Q ((𝑥
·Q (*Q‘(𝑔 +Q
ℎ)))
·Q ℎ)) ∈ (𝐴 +P 𝐵) ↔ 𝑥 ∈ (𝐴 +P 𝐵))) |
38 | 21, 37 | sylibd 238 |
1
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
+Q ℎ) → 𝑥 ∈ (𝐴 +P 𝐵))) |