Step | Hyp | Ref
| Expression |
1 | | addclpr 10961 |
. . . . 5
โข ((๐ต โ P โง
๐ถ โ P)
โ (๐ต
+P ๐ถ) โ P) |
2 | | df-mp 10927 |
. . . . . 6
โข
ยทP = (๐ฆ โ P, ๐ง โ P โฆ {๐ โฃ โ๐ โ ๐ฆ โโ โ ๐ง ๐ = (๐ ยทQ โ)}) |
3 | | mulclnq 10890 |
. . . . . 6
โข ((๐ โ Q โง
โ โ Q)
โ (๐
ยทQ โ) โ Q) |
4 | 2, 3 | genpelv 10943 |
. . . . 5
โข ((๐ด โ P โง
(๐ต
+P ๐ถ) โ P) โ (๐ค โ (๐ด ยทP (๐ต +P
๐ถ)) โ โ๐ฅ โ ๐ด โ๐ฃ โ (๐ต +P ๐ถ)๐ค = (๐ฅ ยทQ ๐ฃ))) |
5 | 1, 4 | sylan2 594 |
. . . 4
โข ((๐ด โ P โง
(๐ต โ P
โง ๐ถ โ
P)) โ (๐ค
โ (๐ด
ยทP (๐ต +P ๐ถ)) โ โ๐ฅ โ ๐ด โ๐ฃ โ (๐ต +P ๐ถ)๐ค = (๐ฅ ยทQ ๐ฃ))) |
6 | 5 | 3impb 1116 |
. . 3
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ค
โ (๐ด
ยทP (๐ต +P ๐ถ)) โ โ๐ฅ โ ๐ด โ๐ฃ โ (๐ต +P ๐ถ)๐ค = (๐ฅ ยทQ ๐ฃ))) |
7 | | df-plp 10926 |
. . . . . . . . . . 11
โข
+P = (๐ค โ P, ๐ฅ โ P โฆ {๐ โฃ โ๐ โ ๐ค โโ โ ๐ฅ ๐ = (๐ +Q โ)}) |
8 | | addclnq 10888 |
. . . . . . . . . . 11
โข ((๐ โ Q โง
โ โ Q)
โ (๐
+Q โ) โ Q) |
9 | 7, 8 | genpelv 10943 |
. . . . . . . . . 10
โข ((๐ต โ P โง
๐ถ โ P)
โ (๐ฃ โ (๐ต +P
๐ถ) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ถ ๐ฃ = (๐ฆ +Q ๐ง))) |
10 | 9 | 3adant1 1131 |
. . . . . . . . 9
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ฃ
โ (๐ต
+P ๐ถ) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ถ ๐ฃ = (๐ฆ +Q ๐ง))) |
11 | 10 | adantr 482 |
. . . . . . . 8
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โ (๐ฃ โ (๐ต +P ๐ถ) โ โ๐ฆ โ ๐ต โ๐ง โ ๐ถ ๐ฃ = (๐ฆ +Q ๐ง))) |
12 | | simprr 772 |
. . . . . . . . . . . 12
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โ ๐ค = (๐ฅ ยทQ ๐ฃ)) |
13 | | simpr 486 |
. . . . . . . . . . . 12
โข (((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โง ๐ฃ = (๐ฆ +Q ๐ง)) โ ๐ฃ = (๐ฆ +Q ๐ง)) |
14 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
โข (๐ฃ = (๐ฆ +Q ๐ง) โ (๐ฅ ยทQ ๐ฃ) = (๐ฅ ยทQ (๐ฆ +Q
๐ง))) |
15 | 14 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
โข (๐ฃ = (๐ฆ +Q ๐ง) โ (๐ค = (๐ฅ ยทQ ๐ฃ) โ ๐ค = (๐ฅ ยทQ (๐ฆ +Q
๐ง)))) |
16 | 15 | biimpac 480 |
. . . . . . . . . . . . 13
โข ((๐ค = (๐ฅ ยทQ ๐ฃ) โง ๐ฃ = (๐ฆ +Q ๐ง)) โ ๐ค = (๐ฅ ยทQ (๐ฆ +Q
๐ง))) |
17 | | distrnq 10904 |
. . . . . . . . . . . . 13
โข (๐ฅ
ยทQ (๐ฆ +Q ๐ง)) = ((๐ฅ ยทQ ๐ฆ) +Q
(๐ฅ
ยทQ ๐ง)) |
18 | 16, 17 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข ((๐ค = (๐ฅ ยทQ ๐ฃ) โง ๐ฃ = (๐ฆ +Q ๐ง)) โ ๐ค = ((๐ฅ ยทQ ๐ฆ) +Q
(๐ฅ
ยทQ ๐ง))) |
19 | 12, 13, 18 | syl2an 597 |
. . . . . . . . . . 11
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โง ((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โง ๐ฃ = (๐ฆ +Q ๐ง))) โ ๐ค = ((๐ฅ ยทQ ๐ฆ) +Q
(๐ฅ
ยทQ ๐ง))) |
20 | | mulclpr 10963 |
. . . . . . . . . . . . . 14
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ด
ยทP ๐ต) โ P) |
21 | 20 | 3adant3 1133 |
. . . . . . . . . . . . 13
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ด
ยทP ๐ต) โ P) |
22 | 21 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โง ((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โง ๐ฃ = (๐ฆ +Q ๐ง))) โ (๐ด ยทP ๐ต) โ
P) |
23 | | mulclpr 10963 |
. . . . . . . . . . . . . 14
โข ((๐ด โ P โง
๐ถ โ P)
โ (๐ด
ยทP ๐ถ) โ P) |
24 | 23 | 3adant2 1132 |
. . . . . . . . . . . . 13
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ด
ยทP ๐ถ) โ P) |
25 | 24 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โง ((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โง ๐ฃ = (๐ฆ +Q ๐ง))) โ (๐ด ยทP ๐ถ) โ
P) |
26 | | simpll 766 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โง ๐ฃ = (๐ฆ +Q ๐ง)) โ ๐ฆ โ ๐ต) |
27 | 2, 3 | genpprecl 10944 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ P โง
๐ต โ P)
โ ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ (๐ฅ ยทQ ๐ฆ) โ (๐ด ยทP ๐ต))) |
28 | 27 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โ (๐ฅ ยทQ ๐ฆ) โ (๐ด ยทP ๐ต))) |
29 | 28 | impl 457 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ๐ฅ
โ ๐ด) โง ๐ฆ โ ๐ต) โ (๐ฅ ยทQ ๐ฆ) โ (๐ด ยทP ๐ต)) |
30 | 29 | adantlrr 720 |
. . . . . . . . . . . . 13
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โง ๐ฆ โ ๐ต) โ (๐ฅ ยทQ ๐ฆ) โ (๐ด ยทP ๐ต)) |
31 | 26, 30 | sylan2 594 |
. . . . . . . . . . . 12
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โง ((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โง ๐ฃ = (๐ฆ +Q ๐ง))) โ (๐ฅ ยทQ ๐ฆ) โ (๐ด ยทP ๐ต)) |
32 | | simplr 768 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โง ๐ฃ = (๐ฆ +Q ๐ง)) โ ๐ง โ ๐ถ) |
33 | 2, 3 | genpprecl 10944 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ P โง
๐ถ โ P)
โ ((๐ฅ โ ๐ด โง ๐ง โ ๐ถ) โ (๐ฅ ยทQ ๐ง) โ (๐ด ยทP ๐ถ))) |
34 | 33 | 3adant2 1132 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ ((๐ฅ
โ ๐ด โง ๐ง โ ๐ถ) โ (๐ฅ ยทQ ๐ง) โ (๐ด ยทP ๐ถ))) |
35 | 34 | impl 457 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ๐ฅ
โ ๐ด) โง ๐ง โ ๐ถ) โ (๐ฅ ยทQ ๐ง) โ (๐ด ยทP ๐ถ)) |
36 | 35 | adantlrr 720 |
. . . . . . . . . . . . 13
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โง ๐ง โ ๐ถ) โ (๐ฅ ยทQ ๐ง) โ (๐ด ยทP ๐ถ)) |
37 | 32, 36 | sylan2 594 |
. . . . . . . . . . . 12
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โง ((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โง ๐ฃ = (๐ฆ +Q ๐ง))) โ (๐ฅ ยทQ ๐ง) โ (๐ด ยทP ๐ถ)) |
38 | 7, 8 | genpprecl 10944 |
. . . . . . . . . . . . 13
โข (((๐ด
ยทP ๐ต) โ P โง (๐ด
ยทP ๐ถ) โ P) โ (((๐ฅ
ยทQ ๐ฆ) โ (๐ด ยทP ๐ต) โง (๐ฅ ยทQ ๐ง) โ (๐ด ยทP ๐ถ)) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐ฅ
ยทQ ๐ง)) โ ((๐ด ยทP ๐ต) +P
(๐ด
ยทP ๐ถ)))) |
39 | 38 | imp 408 |
. . . . . . . . . . . 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 2838 |
. . . . . . . . . 10
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โง ((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โง ๐ฃ = (๐ฆ +Q ๐ง))) โ ๐ค โ ((๐ด ยทP ๐ต) +P
(๐ด
ยทP ๐ถ))) |
42 | 41 | exp32 422 |
. . . . . . . . 9
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โ ((๐ฆ โ ๐ต โง ๐ง โ ๐ถ) โ (๐ฃ = (๐ฆ +Q ๐ง) โ ๐ค โ ((๐ด ยทP ๐ต) +P
(๐ด
ยทP ๐ถ))))) |
43 | 42 | rexlimdvv 3205 |
. . . . . . . 8
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โ (โ๐ฆ โ ๐ต โ๐ง โ ๐ถ ๐ฃ = (๐ฆ +Q ๐ง) โ ๐ค โ ((๐ด ยทP ๐ต) +P
(๐ด
ยทP ๐ถ)))) |
44 | 11, 43 | sylbid 239 |
. . . . . . 7
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ฅ
โ ๐ด โง ๐ค = (๐ฅ ยทQ ๐ฃ))) โ (๐ฃ โ (๐ต +P ๐ถ) โ ๐ค โ ((๐ด ยทP ๐ต) +P
(๐ด
ยทP ๐ถ)))) |
45 | 44 | exp32 422 |
. . . . . 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 412 |
. . . 4
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ ((๐ฅ
โ ๐ด โง ๐ฃ โ (๐ต +P ๐ถ)) โ (๐ค = (๐ฅ ยทQ ๐ฃ) โ ๐ค โ ((๐ด ยทP ๐ต) +P
(๐ด
ยทP ๐ถ))))) |
48 | 47 | rexlimdvv 3205 |
. . 3
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (โ๐ฅ โ ๐ด โ๐ฃ โ (๐ต +P ๐ถ)๐ค = (๐ฅ ยทQ ๐ฃ) โ ๐ค โ ((๐ด ยทP ๐ต) +P
(๐ด
ยทP ๐ถ)))) |
49 | 6, 48 | sylbid 239 |
. 2
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ค
โ (๐ด
ยทP (๐ต +P ๐ถ)) โ ๐ค โ ((๐ด ยทP ๐ต) +P
(๐ด
ยทP ๐ถ)))) |
50 | 49 | ssrdv 3955 |
1
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ด
ยทP (๐ต +P ๐ถ)) โ ((๐ด ยทP ๐ต) +P
(๐ด
ยทP ๐ถ))) |