Step | Hyp | Ref
| Expression |
1 | | mulclpr 10963 |
. . . . 5
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ด
ยทP ๐ต) โ P) |
2 | 1 | 3adant3 1133 |
. . . 4
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ด
ยทP ๐ต) โ P) |
3 | | mulclpr 10963 |
. . . 4
โข ((๐ด โ P โง
๐ถ โ P)
โ (๐ด
ยทP ๐ถ) โ P) |
4 | | df-plp 10926 |
. . . . 5
โข
+P = (๐ฅ โ P, ๐ฆ โ P โฆ {๐ โฃ โ๐ โ ๐ฅ โโ โ ๐ฆ ๐ = (๐ +Q โ)}) |
5 | | addclnq 10888 |
. . . . 5
โข ((๐ โ Q โง
โ โ Q)
โ (๐
+Q โ) โ Q) |
6 | 4, 5 | genpelv 10943 |
. . . 4
โข (((๐ด
ยทP ๐ต) โ P โง (๐ด
ยทP ๐ถ) โ P) โ (๐ค โ ((๐ด ยทP ๐ต) +P
(๐ด
ยทP ๐ถ)) โ โ๐ฃ โ (๐ด ยทP ๐ต)โ๐ข โ (๐ด ยทP ๐ถ)๐ค = (๐ฃ +Q ๐ข))) |
7 | 2, 3, 6 | 3imp3i2an 1346 |
. . 3
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ค
โ ((๐ด
ยทP ๐ต) +P (๐ด
ยทP ๐ถ)) โ โ๐ฃ โ (๐ด ยทP ๐ต)โ๐ข โ (๐ด ยทP ๐ถ)๐ค = (๐ฃ +Q ๐ข))) |
8 | | df-mp 10927 |
. . . . . . . 8
โข
ยทP = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ โ ๐ค โโ โ ๐ฃ ๐ฅ = (๐ ยทQ โ)}) |
9 | | mulclnq 10890 |
. . . . . . . 8
โข ((๐ โ Q โง
โ โ Q)
โ (๐
ยทQ โ) โ Q) |
10 | 8, 9 | genpelv 10943 |
. . . . . . 7
โข ((๐ด โ P โง
๐ถ โ P)
โ (๐ข โ (๐ด
ยทP ๐ถ) โ โ๐ โ ๐ด โ๐ง โ ๐ถ ๐ข = (๐ ยทQ ๐ง))) |
11 | 10 | 3adant2 1132 |
. . . . . 6
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ข
โ (๐ด
ยทP ๐ถ) โ โ๐ โ ๐ด โ๐ง โ ๐ถ ๐ข = (๐ ยทQ ๐ง))) |
12 | 11 | anbi2d 630 |
. . . . 5
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ ((๐ฃ
โ (๐ด
ยทP ๐ต) โง ๐ข โ (๐ด ยทP ๐ถ)) โ (๐ฃ โ (๐ด ยทP ๐ต) โง โ๐ โ ๐ด โ๐ง โ ๐ถ ๐ข = (๐ ยทQ ๐ง)))) |
13 | | df-mp 10927 |
. . . . . . . . 9
โข
ยทP = (๐ค โ P, ๐ฃ โ P โฆ {๐ โฃ โ๐ โ ๐ค โโ โ ๐ฃ ๐ = (๐ ยทQ โ)}) |
14 | 13, 9 | genpelv 10943 |
. . . . . . . 8
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ฃ โ (๐ด
ยทP ๐ต) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฃ = (๐ฅ ยทQ ๐ฆ))) |
15 | 14 | 3adant3 1133 |
. . . . . . 7
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ฃ
โ (๐ด
ยทP ๐ต) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฃ = (๐ฅ ยทQ ๐ฆ))) |
16 | | distrlem4pr 10969 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ))) |
17 | | oveq12 7371 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฃ = (๐ฅ ยทQ ๐ฆ) โง ๐ข = (๐ ยทQ ๐ง)) โ (๐ฃ +Q ๐ข) = ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง))) |
18 | 17 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฃ = (๐ฅ ยทQ ๐ฆ) โง ๐ข = (๐ ยทQ ๐ง)) โ (๐ค = (๐ฃ +Q ๐ข) โ ๐ค = ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)))) |
19 | | eleq1 2826 |
. . . . . . . . . . . . . . . . 17
โข (๐ค = ((๐ฅ ยทQ ๐ฆ) +Q
(๐
ยทQ ๐ง)) โ (๐ค โ (๐ด ยทP (๐ต +P
๐ถ)) โ ((๐ฅ
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
20 | 18, 19 | syl6bi 253 |
. . . . . . . . . . . . . . . 16
โข ((๐ฃ = (๐ฅ ยทQ ๐ฆ) โง ๐ข = (๐ ยทQ ๐ง)) โ (๐ค = (๐ฃ +Q ๐ข) โ (๐ค โ (๐ด ยทP (๐ต +P
๐ถ)) โ ((๐ฅ
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ))))) |
21 | 20 | imp 408 |
. . . . . . . . . . . . . . 15
โข (((๐ฃ = (๐ฅ ยทQ ๐ฆ) โง ๐ข = (๐ ยทQ ๐ง)) โง ๐ค = (๐ฃ +Q ๐ข)) โ (๐ค โ (๐ด ยทP (๐ต +P
๐ถ)) โ ((๐ฅ
ยทQ ๐ฆ) +Q (๐
ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P
๐ถ)))) |
22 | 16, 21 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง ((๐ฅ
โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ (((๐ฃ = (๐ฅ ยทQ ๐ฆ) โง ๐ข = (๐ ยทQ ๐ง)) โง ๐ค = (๐ฃ +Q ๐ข)) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ)))) |
23 | 22 | exp4b 432 |
. . . . . . . . . . . . 13
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ)) โ ((๐ฃ = (๐ฅ ยทQ ๐ฆ) โง ๐ข = (๐ ยทQ ๐ง)) โ (๐ค = (๐ฃ +Q ๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ)))))) |
24 | 23 | com3l 89 |
. . . . . . . . . . . 12
โข (((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ)) โ ((๐ฃ = (๐ฅ ยทQ ๐ฆ) โง ๐ข = (๐ ยทQ ๐ง)) โ ((๐ด โ P โง ๐ต โ P โง
๐ถ โ P)
โ (๐ค = (๐ฃ +Q
๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ)))))) |
25 | 24 | exp4b 432 |
. . . . . . . . . . 11
โข ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ((๐ โ ๐ด โง ๐ง โ ๐ถ) โ (๐ฃ = (๐ฅ ยทQ ๐ฆ) โ (๐ข = (๐ ยทQ ๐ง) โ ((๐ด โ P โง ๐ต โ P โง
๐ถ โ P)
โ (๐ค = (๐ฃ +Q
๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ)))))))) |
26 | 25 | com23 86 |
. . . . . . . . . 10
โข ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ (๐ฃ = (๐ฅ ยทQ ๐ฆ) โ ((๐ โ ๐ด โง ๐ง โ ๐ถ) โ (๐ข = (๐ ยทQ ๐ง) โ ((๐ด โ P โง ๐ต โ P โง
๐ถ โ P)
โ (๐ค = (๐ฃ +Q
๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ)))))))) |
27 | 26 | rexlimivv 3197 |
. . . . . . . . 9
โข
(โ๐ฅ โ
๐ด โ๐ฆ โ ๐ต ๐ฃ = (๐ฅ ยทQ ๐ฆ) โ ((๐ โ ๐ด โง ๐ง โ ๐ถ) โ (๐ข = (๐ ยทQ ๐ง) โ ((๐ด โ P โง ๐ต โ P โง
๐ถ โ P)
โ (๐ค = (๐ฃ +Q
๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ))))))) |
28 | 27 | rexlimdvv 3205 |
. . . . . . . 8
โข
(โ๐ฅ โ
๐ด โ๐ฆ โ ๐ต ๐ฃ = (๐ฅ ยทQ ๐ฆ) โ (โ๐ โ ๐ด โ๐ง โ ๐ถ ๐ข = (๐ ยทQ ๐ง) โ ((๐ด โ P โง ๐ต โ P โง
๐ถ โ P)
โ (๐ค = (๐ฃ +Q
๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ)))))) |
29 | 28 | com3r 87 |
. . . . . . 7
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฃ = (๐ฅ ยทQ ๐ฆ) โ (โ๐ โ ๐ด โ๐ง โ ๐ถ ๐ข = (๐ ยทQ ๐ง) โ (๐ค = (๐ฃ +Q ๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ)))))) |
30 | 15, 29 | sylbid 239 |
. . . . . 6
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ฃ
โ (๐ด
ยทP ๐ต) โ (โ๐ โ ๐ด โ๐ง โ ๐ถ ๐ข = (๐ ยทQ ๐ง) โ (๐ค = (๐ฃ +Q ๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ)))))) |
31 | 30 | impd 412 |
. . . . 5
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ ((๐ฃ
โ (๐ด
ยทP ๐ต) โง โ๐ โ ๐ด โ๐ง โ ๐ถ ๐ข = (๐ ยทQ ๐ง)) โ (๐ค = (๐ฃ +Q ๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ))))) |
32 | 12, 31 | sylbid 239 |
. . . 4
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ ((๐ฃ
โ (๐ด
ยทP ๐ต) โง ๐ข โ (๐ด ยทP ๐ถ)) โ (๐ค = (๐ฃ +Q ๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ))))) |
33 | 32 | rexlimdvv 3205 |
. . 3
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (โ๐ฃ โ (๐ด ยทP ๐ต)โ๐ข โ (๐ด ยทP ๐ถ)๐ค = (๐ฃ +Q ๐ข) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ)))) |
34 | 7, 33 | sylbid 239 |
. 2
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ (๐ค
โ ((๐ด
ยทP ๐ต) +P (๐ด
ยทP ๐ถ)) โ ๐ค โ (๐ด ยทP (๐ต +P
๐ถ)))) |
35 | 34 | ssrdv 3955 |
1
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ ((๐ด
ยทP ๐ต) +P (๐ด
ยทP ๐ถ)) โ (๐ด ยทP (๐ต +P
๐ถ))) |