Step | Hyp | Ref
| Expression |
1 | | prop 6458 |
. . . 4
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
2 | | prml 6460 |
. . . 4
⊢
(〈(1st ‘B),
(2nd ‘B)〉 ∈ P → ∃𝑝 ∈
Q 𝑝 ∈ (1st ‘B)) |
3 | 1, 2 | syl 14 |
. . 3
⊢ (B ∈
P → ∃𝑝 ∈
Q 𝑝 ∈ (1st ‘B)) |
4 | 3 | adantl 262 |
. 2
⊢
((A ∈ P ∧ B ∈ P) → ∃𝑝 ∈
Q 𝑝 ∈ (1st ‘B)) |
5 | | prop 6458 |
. . . . 5
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
6 | | prarloc 6486 |
. . . . 5
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ 𝑝
∈ Q) → ∃𝑟 ∈
(1st ‘A)∃𝑞 ∈
(2nd ‘A)𝑞 <Q (𝑟 +Q 𝑝)) |
7 | 5, 6 | sylan 267 |
. . . 4
⊢
((A ∈ P ∧ 𝑝
∈ Q) → ∃𝑟 ∈
(1st ‘A)∃𝑞 ∈
(2nd ‘A)𝑞 <Q (𝑟 +Q 𝑝)) |
8 | 7 | ad2ant2r 478 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) → ∃𝑟 ∈
(1st ‘A)∃𝑞 ∈
(2nd ‘A)𝑞 <Q (𝑟 +Q 𝑝)) |
9 | | elprnqu 6465 |
. . . . . . . . . . 11
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ 𝑞
∈ (2nd ‘A)) → 𝑞 ∈
Q) |
10 | 5, 9 | sylan 267 |
. . . . . . . . . 10
⊢
((A ∈ P ∧ 𝑞
∈ (2nd ‘A)) → 𝑞 ∈
Q) |
11 | 10 | adantlr 446 |
. . . . . . . . 9
⊢
(((A ∈ P ∧ B ∈ P) ∧ 𝑞
∈ (2nd ‘A)) → 𝑞 ∈
Q) |
12 | 11 | ad2ant2rl 480 |
. . . . . . . 8
⊢
((((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A))) → 𝑞 ∈
Q) |
13 | 12 | adantr 261 |
. . . . . . 7
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A))) ∧ 𝑞 <Q
(𝑟 +Q
𝑝)) → 𝑞 ∈
Q) |
14 | | simplrr 488 |
. . . . . . 7
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A))) ∧ 𝑞 <Q
(𝑟 +Q
𝑝)) → 𝑞 ∈
(2nd ‘A)) |
15 | | simprl 483 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ Q ∧ 𝑝
∈ (1st ‘B)) ∧ (𝑟 ∈ (1st ‘A) ∧ 𝑞 ∈ (2nd ‘A))) → 𝑟 ∈
(1st ‘A)) |
16 | | simplr 482 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ Q ∧ 𝑝
∈ (1st ‘B)) ∧ (𝑟 ∈ (1st ‘A) ∧ 𝑞 ∈ (2nd ‘A))) → 𝑝 ∈
(1st ‘B)) |
17 | 15, 16 | jca 290 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ Q ∧ 𝑝
∈ (1st ‘B)) ∧ (𝑟 ∈ (1st ‘A) ∧ 𝑞 ∈ (2nd ‘A))) → (𝑟 ∈
(1st ‘A) ∧ 𝑝
∈ (1st ‘B))) |
18 | | df-iplp 6451 |
. . . . . . . . . . . . 13
⊢
+P = (x ∈ P, y ∈
P ↦ 〈{f ∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(1st ‘x) ∧ ℎ
∈ (1st ‘y) ∧ f = (g
+Q ℎ))}, {f
∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(2nd ‘x) ∧ ℎ
∈ (2nd ‘y) ∧ f = (g
+Q ℎ))}〉) |
19 | | addclnq 6359 |
. . . . . . . . . . . . 13
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (g +Q ℎ) ∈
Q) |
20 | 18, 19 | genpprecll 6497 |
. . . . . . . . . . . 12
⊢
((A ∈ P ∧ B ∈ P) → ((𝑟 ∈
(1st ‘A) ∧ 𝑝
∈ (1st ‘B)) → (𝑟 +Q 𝑝) ∈
(1st ‘(A
+P B)))) |
21 | 17, 20 | syl5 28 |
. . . . . . . . . . 11
⊢
((A ∈ P ∧ B ∈ P) → (((𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B)) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A))) → (𝑟 +Q 𝑝) ∈
(1st ‘(A
+P B)))) |
22 | 21 | imdistani 419 |
. . . . . . . . . 10
⊢
(((A ∈ P ∧ B ∈ P) ∧ ((𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B)) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A)))) → ((A
∈ P ∧ B ∈ P) ∧ (𝑟 +Q 𝑝) ∈
(1st ‘(A
+P B)))) |
23 | | addclpr 6520 |
. . . . . . . . . . 11
⊢
((A ∈ P ∧ B ∈ P) → (A +P B) ∈
P) |
24 | | prop 6458 |
. . . . . . . . . . . 12
⊢
((A +P
B) ∈
P → 〈(1st ‘(A +P B)), (2nd ‘(A +P B))〉 ∈
P) |
25 | | prcdnql 6467 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘(A
+P B)),
(2nd ‘(A
+P B))〉 ∈ P ∧ (𝑟 +Q 𝑝) ∈
(1st ‘(A
+P B))) →
(𝑞
<Q (𝑟 +Q 𝑝) → 𝑞 ∈
(1st ‘(A
+P B)))) |
26 | 24, 25 | sylan 267 |
. . . . . . . . . . 11
⊢
(((A +P
B) ∈
P ∧ (𝑟 +Q 𝑝) ∈
(1st ‘(A
+P B))) →
(𝑞
<Q (𝑟 +Q 𝑝) → 𝑞 ∈
(1st ‘(A
+P B)))) |
27 | 23, 26 | sylan 267 |
. . . . . . . . . 10
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝑟 +Q 𝑝) ∈
(1st ‘(A
+P B))) →
(𝑞
<Q (𝑟 +Q 𝑝) → 𝑞 ∈
(1st ‘(A
+P B)))) |
28 | 22, 27 | syl 14 |
. . . . . . . . 9
⊢
(((A ∈ P ∧ B ∈ P) ∧ ((𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B)) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A)))) → (𝑞 <Q (𝑟 +Q 𝑝) → 𝑞 ∈
(1st ‘(A
+P B)))) |
29 | 28 | anassrs 380 |
. . . . . . . 8
⊢
((((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A))) → (𝑞 <Q (𝑟 +Q 𝑝) → 𝑞 ∈
(1st ‘(A
+P B)))) |
30 | 29 | imp 115 |
. . . . . . 7
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A))) ∧ 𝑞 <Q
(𝑟 +Q
𝑝)) → 𝑞 ∈
(1st ‘(A
+P B))) |
31 | | rspe 2364 |
. . . . . . 7
⊢ ((𝑞 ∈ Q ∧ (𝑞 ∈
(2nd ‘A) ∧ 𝑞
∈ (1st ‘(A +P B)))) → ∃𝑞 ∈
Q (𝑞 ∈ (2nd ‘A) ∧ 𝑞 ∈ (1st ‘(A +P B)))) |
32 | 13, 14, 30, 31 | syl12anc 1132 |
. . . . . 6
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A))) ∧ 𝑞 <Q
(𝑟 +Q
𝑝)) → ∃𝑞 ∈
Q (𝑞 ∈ (2nd ‘A) ∧ 𝑞 ∈ (1st ‘(A +P B)))) |
33 | | ltdfpr 6489 |
. . . . . . . 8
⊢
((A ∈ P ∧ (A
+P B) ∈ P) → (A<P (A +P B) ↔ ∃𝑞 ∈ Q (𝑞 ∈
(2nd ‘A) ∧ 𝑞
∈ (1st ‘(A +P B))))) |
34 | 23, 33 | syldan 266 |
. . . . . . 7
⊢
((A ∈ P ∧ B ∈ P) → (A<P (A +P B) ↔ ∃𝑞 ∈ Q (𝑞 ∈
(2nd ‘A) ∧ 𝑞
∈ (1st ‘(A +P B))))) |
35 | 34 | ad3antrrr 461 |
. . . . . 6
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A))) ∧ 𝑞 <Q
(𝑟 +Q
𝑝)) → (A<P (A +P B) ↔ ∃𝑞 ∈ Q (𝑞 ∈
(2nd ‘A) ∧ 𝑞
∈ (1st ‘(A +P B))))) |
36 | 32, 35 | mpbird 156 |
. . . . 5
⊢
(((((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A))) ∧ 𝑞 <Q
(𝑟 +Q
𝑝)) → A<P (A +P B)) |
37 | 36 | ex 108 |
. . . 4
⊢
((((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) ∧ (𝑟 ∈
(1st ‘A) ∧ 𝑞
∈ (2nd ‘A))) → (𝑞 <Q (𝑟 +Q 𝑝) → A<P (A +P B))) |
38 | 37 | rexlimdvva 2434 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) → (∃𝑟 ∈
(1st ‘A)∃𝑞 ∈
(2nd ‘A)𝑞 <Q (𝑟 +Q 𝑝) → A<P (A +P B))) |
39 | 8, 38 | mpd 13 |
. 2
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝑝 ∈
Q ∧ 𝑝 ∈
(1st ‘B))) → A<P (A +P B)) |
40 | 4, 39 | rexlimddv 2431 |
1
⊢
((A ∈ P ∧ B ∈ P) → A<P (A +P B)) |