Step | Hyp | Ref
| Expression |
1 | | df-nr 11053 |
. . 3
โข
R = ((P ร P) /
~R ) |
2 | | oveq1 7418 |
. . . 4
โข
([โจ๐ฅ, ๐ฆโฉ]
~R = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~R
ยทR [โจ๐ง, ๐คโฉ] ~R ) =
(๐ด
ยทR [โจ๐ง, ๐คโฉ] ~R
)) |
3 | 2 | eleq1d 2816 |
. . 3
โข
([โจ๐ฅ, ๐ฆโฉ]
~R = ๐ด โ (([โจ๐ฅ, ๐ฆโฉ] ~R
ยทR [โจ๐ง, ๐คโฉ] ~R ) โ
((P ร P) / ~R
) โ (๐ด
ยทR [โจ๐ง, ๐คโฉ] ~R ) โ
((P ร P) / ~R
))) |
4 | | oveq2 7419 |
. . . 4
โข
([โจ๐ง, ๐คโฉ]
~R = ๐ต โ (๐ด ยทR
[โจ๐ง, ๐คโฉ]
~R ) = (๐ด ยทR ๐ต)) |
5 | 4 | eleq1d 2816 |
. . 3
โข
([โจ๐ง, ๐คโฉ]
~R = ๐ต โ ((๐ด ยทR
[โจ๐ง, ๐คโฉ]
~R ) โ ((P ร P)
/ ~R ) โ (๐ด ยทR ๐ต) โ ((P
ร P) / ~R
))) |
6 | | mulsrpr 11073 |
. . . 4
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ ([โจ๐ฅ, ๐ฆโฉ] ~R
ยทR [โจ๐ง, ๐คโฉ] ~R ) =
[โจ((๐ฅ
ยทP ๐ง) +P (๐ฆ
ยทP ๐ค)), ((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง))โฉ] ~R
) |
7 | | mulclpr 11017 |
. . . . . . . 8
โข ((๐ฅ โ P โง
๐ง โ P)
โ (๐ฅ
ยทP ๐ง) โ P) |
8 | | mulclpr 11017 |
. . . . . . . 8
โข ((๐ฆ โ P โง
๐ค โ P)
โ (๐ฆ
ยทP ๐ค) โ P) |
9 | | addclpr 11015 |
. . . . . . . 8
โข (((๐ฅ
ยทP ๐ง) โ P โง (๐ฆ
ยทP ๐ค) โ P) โ ((๐ฅ
ยทP ๐ง) +P (๐ฆ
ยทP ๐ค)) โ P) |
10 | 7, 8, 9 | syl2an 594 |
. . . . . . 7
โข (((๐ฅ โ P โง
๐ง โ P)
โง (๐ฆ โ
P โง ๐ค
โ P)) โ ((๐ฅ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ค)) โ P) |
11 | 10 | an4s 656 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ ((๐ฅ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ค)) โ P) |
12 | | mulclpr 11017 |
. . . . . . . 8
โข ((๐ฅ โ P โง
๐ค โ P)
โ (๐ฅ
ยทP ๐ค) โ P) |
13 | | mulclpr 11017 |
. . . . . . . 8
โข ((๐ฆ โ P โง
๐ง โ P)
โ (๐ฆ
ยทP ๐ง) โ P) |
14 | | addclpr 11015 |
. . . . . . . 8
โข (((๐ฅ
ยทP ๐ค) โ P โง (๐ฆ
ยทP ๐ง) โ P) โ ((๐ฅ
ยทP ๐ค) +P (๐ฆ
ยทP ๐ง)) โ P) |
15 | 12, 13, 14 | syl2an 594 |
. . . . . . 7
โข (((๐ฅ โ P โง
๐ค โ P)
โง (๐ฆ โ
P โง ๐ง
โ P)) โ ((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง)) โ P) |
16 | 15 | an42s 657 |
. . . . . 6
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ ((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง)) โ P) |
17 | 11, 16 | jca 510 |
. . . . 5
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ (((๐ฅ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ค)) โ P โง ((๐ฅ
ยทP ๐ค) +P (๐ฆ
ยทP ๐ง)) โ P)) |
18 | | opelxpi 5712 |
. . . . 5
โข ((((๐ฅ
ยทP ๐ง) +P (๐ฆ
ยทP ๐ค)) โ P โง ((๐ฅ
ยทP ๐ค) +P (๐ฆ
ยทP ๐ง)) โ P) โ
โจ((๐ฅ
ยทP ๐ง) +P (๐ฆ
ยทP ๐ค)), ((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง))โฉ โ (P ร
P)) |
19 | | enrex 11064 |
. . . . . 6
โข
~R โ V |
20 | 19 | ecelqsi 8769 |
. . . . 5
โข
(โจ((๐ฅ
ยทP ๐ง) +P (๐ฆ
ยทP ๐ค)), ((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง))โฉ โ (P ร
P) โ [โจ((๐ฅ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ค)), ((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง))โฉ] ~R โ
((P ร P) / ~R
)) |
21 | 17, 18, 20 | 3syl 18 |
. . . 4
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ [โจ((๐ฅ ยทP ๐ง) +P
(๐ฆ
ยทP ๐ค)), ((๐ฅ ยทP ๐ค) +P
(๐ฆ
ยทP ๐ง))โฉ] ~R โ
((P ร P) / ~R
)) |
22 | 6, 21 | eqeltrd 2831 |
. . 3
โข (((๐ฅ โ P โง
๐ฆ โ P)
โง (๐ง โ
P โง ๐ค
โ P)) โ ([โจ๐ฅ, ๐ฆโฉ] ~R
ยทR [โจ๐ง, ๐คโฉ] ~R ) โ
((P ร P) / ~R
)) |
23 | 1, 3, 5, 22 | 2ecoptocl 8804 |
. 2
โข ((๐ด โ R โง
๐ต โ R)
โ (๐ด
ยทR ๐ต) โ ((P ร
P) / ~R )) |
24 | 23, 1 | eleqtrrdi 2842 |
1
โข ((๐ด โ R โง
๐ต โ R)
โ (๐ด
ยทR ๐ต) โ R) |