Step | Hyp | Ref
| Expression |
1 | | prop 7437 |
. . . . . . 7
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
2 | | prnmaddl 7452 |
. . . . . . 7
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑣 ∈ (1st
‘𝐵)) →
∃𝑤 ∈
Q (𝑣
+Q 𝑤) ∈ (1st ‘𝐵)) |
3 | 1, 2 | sylan 281 |
. . . . . 6
⊢ ((𝐵 ∈ P ∧
𝑣 ∈ (1st
‘𝐵)) →
∃𝑤 ∈
Q (𝑣
+Q 𝑤) ∈ (1st ‘𝐵)) |
4 | 3 | 3ad2antl2 1155 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ 𝑣
∈ (1st ‘𝐵)) → ∃𝑤 ∈ Q (𝑣 +Q 𝑤) ∈ (1st
‘𝐵)) |
5 | 4 | adantlr 474 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) → ∃𝑤 ∈ Q (𝑣 +Q
𝑤) ∈ (1st
‘𝐵)) |
6 | | simprl 526 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) → 𝑤 ∈
Q) |
7 | | halfnqq 7372 |
. . . . . 6
⊢ (𝑤 ∈ Q →
∃𝑡 ∈
Q (𝑡
+Q 𝑡) = 𝑤) |
8 | 6, 7 | syl 14 |
. . . . 5
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) →
∃𝑡 ∈
Q (𝑡
+Q 𝑡) = 𝑤) |
9 | | simplll 528 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) → (𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P)) |
10 | 9 | adantr 274 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) → (𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈
P)) |
11 | 10 | simp1d 1004 |
. . . . . . . 8
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) → 𝐴 ∈ P) |
12 | | prop 7437 |
. . . . . . . 8
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
13 | 11, 12 | syl 14 |
. . . . . . 7
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) → 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
14 | | simprl 526 |
. . . . . . 7
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) → 𝑡 ∈ Q) |
15 | | prarloc2 7466 |
. . . . . . 7
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑡 ∈ Q) →
∃𝑢 ∈
(1st ‘𝐴)(𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) |
16 | 13, 14, 15 | syl2anc 409 |
. . . . . 6
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) → ∃𝑢 ∈ (1st ‘𝐴)(𝑢 +Q 𝑡) ∈ (2nd
‘𝐴)) |
17 | 9 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P)) |
18 | 17 | simp1d 1004 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝐴 ∈
P) |
19 | 17 | simp2d 1005 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝐵 ∈
P) |
20 | | addclpr 7499 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴
+P 𝐵) ∈ P) |
21 | 18, 19, 20 | syl2anc 409 |
. . . . . . . . . 10
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝐴 +P
𝐵) ∈
P) |
22 | | prop 7437 |
. . . . . . . . . 10
⊢ ((𝐴 +P
𝐵) ∈ P
→ 〈(1st ‘(𝐴 +P 𝐵)), (2nd
‘(𝐴
+P 𝐵))〉 ∈
P) |
23 | 21, 22 | syl 14 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) →
〈(1st ‘(𝐴 +P 𝐵)), (2nd
‘(𝐴
+P 𝐵))〉 ∈
P) |
24 | 18, 12 | syl 14 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
25 | | simprl 526 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑢 ∈ (1st
‘𝐴)) |
26 | | elprnql 7443 |
. . . . . . . . . . 11
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑢 ∈ (1st
‘𝐴)) → 𝑢 ∈
Q) |
27 | 24, 25, 26 | syl2anc 409 |
. . . . . . . . . 10
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑢 ∈
Q) |
28 | 19, 1 | syl 14 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
29 | | simplr 525 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) → 𝑣 ∈ (1st
‘𝐵)) |
30 | 29 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑣 ∈ (1st
‘𝐵)) |
31 | | elprnql 7443 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑣 ∈ (1st
‘𝐵)) → 𝑣 ∈
Q) |
32 | 28, 30, 31 | syl2anc 409 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑣 ∈
Q) |
33 | | simplrl 530 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) → 𝑤 ∈ Q) |
34 | 33 | adantr 274 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑤 ∈
Q) |
35 | | addclnq 7337 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→ (𝑣
+Q 𝑤) ∈ Q) |
36 | 32, 34, 35 | syl2anc 409 |
. . . . . . . . . 10
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝑣 +Q
𝑤) ∈
Q) |
37 | | addclnq 7337 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ Q ∧
(𝑣
+Q 𝑤) ∈ Q) → (𝑢 +Q
(𝑣
+Q 𝑤)) ∈ Q) |
38 | 27, 36, 37 | syl2anc 409 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝑢 +Q
(𝑣
+Q 𝑤)) ∈ Q) |
39 | | prdisj 7454 |
. . . . . . . . 9
⊢
((〈(1st ‘(𝐴 +P 𝐵)), (2nd
‘(𝐴
+P 𝐵))〉 ∈ P ∧ (𝑢 +Q
(𝑣
+Q 𝑤)) ∈ Q) → ¬
((𝑢
+Q (𝑣 +Q 𝑤)) ∈ (1st
‘(𝐴
+P 𝐵)) ∧ (𝑢 +Q (𝑣 +Q
𝑤)) ∈ (2nd
‘(𝐴
+P 𝐵)))) |
40 | 23, 38, 39 | syl2anc 409 |
. . . . . . . 8
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ¬
((𝑢
+Q (𝑣 +Q 𝑤)) ∈ (1st
‘(𝐴
+P 𝐵)) ∧ (𝑢 +Q (𝑣 +Q
𝑤)) ∈ (2nd
‘(𝐴
+P 𝐵)))) |
41 | 18 | adantr 274 |
. . . . . . . . . 10
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → 𝐴 ∈
P) |
42 | 19 | adantr 274 |
. . . . . . . . . 10
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → 𝐵 ∈
P) |
43 | | simplrl 530 |
. . . . . . . . . 10
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → 𝑢 ∈ (1st
‘𝐴)) |
44 | | simplrr 531 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) → (𝑣 +Q 𝑤) ∈ (1st
‘𝐵)) |
45 | 44 | ad2antrr 485 |
. . . . . . . . . 10
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → (𝑣 +Q
𝑤) ∈ (1st
‘𝐵)) |
46 | | df-iplp 7430 |
. . . . . . . . . . . 12
⊢
+P = (𝑟 ∈ P, 𝑠 ∈ P ↦ 〈{𝑓 ∈ Q ∣
∃𝑔 ∈
Q ∃ℎ
∈ Q (𝑔
∈ (1st ‘𝑟) ∧ ℎ ∈ (1st ‘𝑠) ∧ 𝑓 = (𝑔 +Q ℎ))}, {𝑓 ∈ Q ∣ ∃𝑔 ∈ Q
∃ℎ ∈
Q (𝑔 ∈
(2nd ‘𝑟)
∧ ℎ ∈
(2nd ‘𝑠)
∧ 𝑓 = (𝑔 +Q
ℎ))}〉) |
47 | | addclnq 7337 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
48 | 46, 47 | genpprecll 7476 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑢 ∈
(1st ‘𝐴)
∧ (𝑣
+Q 𝑤) ∈ (1st ‘𝐵)) → (𝑢 +Q (𝑣 +Q
𝑤)) ∈ (1st
‘(𝐴
+P 𝐵)))) |
49 | 48 | imp 123 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑢 ∈
(1st ‘𝐴)
∧ (𝑣
+Q 𝑤) ∈ (1st ‘𝐵))) → (𝑢 +Q (𝑣 +Q
𝑤)) ∈ (1st
‘(𝐴
+P 𝐵))) |
50 | 41, 42, 43, 45, 49 | syl22anc 1234 |
. . . . . . . . 9
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → (𝑢 +Q
(𝑣
+Q 𝑤)) ∈ (1st ‘(𝐴 +P
𝐵))) |
51 | 27 | adantr 274 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → 𝑢 ∈
Q) |
52 | 14 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → 𝑡 ∈
Q) |
53 | 32 | adantr 274 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → 𝑣 ∈
Q) |
54 | | addcomnqg 7343 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
55 | 54 | adantl 275 |
. . . . . . . . . . . . 13
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) ∧ (𝑓 ∈ Q ∧
𝑔 ∈ Q))
→ (𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
56 | | addassnqg 7344 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → ((𝑓
+Q 𝑔) +Q ℎ) = (𝑓 +Q (𝑔 +Q
ℎ))) |
57 | 56 | adantl 275 |
. . . . . . . . . . . . 13
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) ∧ (𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q)) → ((𝑓 +Q 𝑔) +Q
ℎ) = (𝑓 +Q (𝑔 +Q
ℎ))) |
58 | | addclnq 7337 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓
+Q 𝑔) ∈ Q) |
59 | 58 | adantl 275 |
. . . . . . . . . . . . 13
⊢
(((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) ∧ (𝑓 ∈ Q ∧
𝑔 ∈ Q))
→ (𝑓
+Q 𝑔) ∈ Q) |
60 | 51, 52, 53, 55, 57, 52, 59 | caov4d 6037 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → ((𝑢 +Q
𝑡)
+Q (𝑣 +Q 𝑡)) = ((𝑢 +Q 𝑣) +Q
(𝑡
+Q 𝑡))) |
61 | | simprr 527 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) → (𝑡 +Q 𝑡) = 𝑤) |
62 | 61 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → (𝑡 +Q
𝑡) = 𝑤) |
63 | 62 | oveq2d 5869 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → ((𝑢 +Q
𝑣)
+Q (𝑡 +Q 𝑡)) = ((𝑢 +Q 𝑣) +Q
𝑤)) |
64 | 33 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → 𝑤 ∈
Q) |
65 | | addassnqg 7344 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ Q ∧
𝑣 ∈ Q
∧ 𝑤 ∈
Q) → ((𝑢
+Q 𝑣) +Q 𝑤) = (𝑢 +Q (𝑣 +Q
𝑤))) |
66 | 51, 53, 64, 65 | syl3anc 1233 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → ((𝑢 +Q
𝑣)
+Q 𝑤) = (𝑢 +Q (𝑣 +Q
𝑤))) |
67 | 60, 63, 66 | 3eqtrd 2207 |
. . . . . . . . . . 11
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → ((𝑢 +Q
𝑡)
+Q (𝑣 +Q 𝑡)) = (𝑢 +Q (𝑣 +Q
𝑤))) |
68 | | simplrr 531 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → (𝑢 +Q
𝑡) ∈ (2nd
‘𝐴)) |
69 | | simpr 109 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) |
70 | 17 | simp3d 1006 |
. . . . . . . . . . . . . 14
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝐶 ∈
P) |
71 | 70 | adantr 274 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → 𝐶 ∈
P) |
72 | 46, 47 | genppreclu 7477 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (((𝑢
+Q 𝑡) ∈ (2nd ‘𝐴) ∧ (𝑣 +Q 𝑡) ∈ (2nd
‘𝐶)) → ((𝑢 +Q
𝑡)
+Q (𝑣 +Q 𝑡)) ∈ (2nd
‘(𝐴
+P 𝐶)))) |
73 | 41, 71, 72 | syl2anc 409 |
. . . . . . . . . . . 12
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → (((𝑢 +Q
𝑡) ∈ (2nd
‘𝐴) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → ((𝑢 +Q
𝑡)
+Q (𝑣 +Q 𝑡)) ∈ (2nd
‘(𝐴
+P 𝐶)))) |
74 | 68, 69, 73 | mp2and 431 |
. . . . . . . . . . 11
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → ((𝑢 +Q
𝑡)
+Q (𝑣 +Q 𝑡)) ∈ (2nd
‘(𝐴
+P 𝐶))) |
75 | 67, 74 | eqeltrrd 2248 |
. . . . . . . . . 10
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → (𝑢 +Q
(𝑣
+Q 𝑤)) ∈ (2nd ‘(𝐴 +P
𝐶))) |
76 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) |
77 | 76 | ad3antrrr 489 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) → (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) |
78 | 77 | ad2antrr 485 |
. . . . . . . . . . 11
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) |
79 | | fveq2 5496 |
. . . . . . . . . . . 12
⊢ ((𝐴 +P
𝐵) = (𝐴 +P 𝐶) → (2nd
‘(𝐴
+P 𝐵)) = (2nd ‘(𝐴 +P
𝐶))) |
80 | 79 | eleq2d 2240 |
. . . . . . . . . . 11
⊢ ((𝐴 +P
𝐵) = (𝐴 +P 𝐶) → ((𝑢 +Q (𝑣 +Q
𝑤)) ∈ (2nd
‘(𝐴
+P 𝐵)) ↔ (𝑢 +Q (𝑣 +Q
𝑤)) ∈ (2nd
‘(𝐴
+P 𝐶)))) |
81 | 78, 80 | syl 14 |
. . . . . . . . . 10
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → ((𝑢 +Q
(𝑣
+Q 𝑤)) ∈ (2nd ‘(𝐴 +P
𝐵)) ↔ (𝑢 +Q
(𝑣
+Q 𝑤)) ∈ (2nd ‘(𝐴 +P
𝐶)))) |
82 | 75, 81 | mpbird 166 |
. . . . . . . . 9
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → (𝑢 +Q
(𝑣
+Q 𝑤)) ∈ (2nd ‘(𝐴 +P
𝐵))) |
83 | 50, 82 | jca 304 |
. . . . . . . 8
⊢
((((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) ∧ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶)) → ((𝑢 +Q
(𝑣
+Q 𝑤)) ∈ (1st ‘(𝐴 +P
𝐵)) ∧ (𝑢 +Q
(𝑣
+Q 𝑤)) ∈ (2nd ‘(𝐴 +P
𝐵)))) |
84 | 40, 83 | mtand 660 |
. . . . . . 7
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → ¬
(𝑣
+Q 𝑡) ∈ (2nd ‘𝐶)) |
85 | | prop 7437 |
. . . . . . . . 9
⊢ (𝐶 ∈ P →
〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈
P) |
86 | 70, 85 | syl 14 |
. . . . . . . 8
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) →
〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈
P) |
87 | | simplrl 530 |
. . . . . . . . 9
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑡 ∈
Q) |
88 | | ltaddnq 7369 |
. . . . . . . . 9
⊢ ((𝑣 ∈ Q ∧
𝑡 ∈ Q)
→ 𝑣
<Q (𝑣 +Q 𝑡)) |
89 | 32, 87, 88 | syl2anc 409 |
. . . . . . . 8
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑣 <Q
(𝑣
+Q 𝑡)) |
90 | | prloc 7453 |
. . . . . . . 8
⊢
((〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈ P ∧ 𝑣 <Q
(𝑣
+Q 𝑡)) → (𝑣 ∈ (1st ‘𝐶) ∨ (𝑣 +Q 𝑡) ∈ (2nd
‘𝐶))) |
91 | 86, 89, 90 | syl2anc 409 |
. . . . . . 7
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → (𝑣 ∈ (1st
‘𝐶) ∨ (𝑣 +Q
𝑡) ∈ (2nd
‘𝐶))) |
92 | 84, 91 | ecased 1344 |
. . . . . 6
⊢
(((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) ∧ (𝑢 ∈ (1st ‘𝐴) ∧ (𝑢 +Q 𝑡) ∈ (2nd
‘𝐴))) → 𝑣 ∈ (1st
‘𝐶)) |
93 | 16, 92 | rexlimddv 2592 |
. . . . 5
⊢
((((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) ∧ (𝑡 ∈ Q ∧
(𝑡
+Q 𝑡) = 𝑤)) → 𝑣 ∈ (1st ‘𝐶)) |
94 | 8, 93 | rexlimddv 2592 |
. . . 4
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P
𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) ∧ (𝑤 ∈ Q ∧ (𝑣 +Q
𝑤) ∈ (1st
‘𝐵))) → 𝑣 ∈ (1st
‘𝐶)) |
95 | 5, 94 | rexlimddv 2592 |
. . 3
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) ∧ 𝑣 ∈ (1st ‘𝐵)) → 𝑣 ∈ (1st ‘𝐶)) |
96 | 95 | ex 114 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) → (𝑣 ∈ (1st ‘𝐵) → 𝑣 ∈ (1st ‘𝐶))) |
97 | 96 | ssrdv 3153 |
1
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐴
+P 𝐵) = (𝐴 +P 𝐶)) → (1st
‘𝐵) ⊆
(1st ‘𝐶)) |