Step | Hyp | Ref
| Expression |
1 | | ax-hilex 29649 |
. . . 4
โข โ
โ V |
2 | 1 | elpw2 5289 |
. . 3
โข (๐ป โ ๐ซ โ โ
๐ป โ
โ) |
3 | | 3anass 1094 |
. . 3
โข
((0โ โ ๐ป โง ( +โ โ (๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป) โ (0โ โ ๐ป โง (( +โ
โ (๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป))) |
4 | 2, 3 | anbi12i 627 |
. 2
โข ((๐ป โ ๐ซ โ โง
(0โ โ ๐ป โง ( +โ โ (๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป)) โ (๐ป โ โ โง (0โ
โ ๐ป โง ((
+โ โ (๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป)))) |
5 | | eleq2 2825 |
. . . 4
โข (โ = ๐ป โ (0โ โ โ โ 0โ
โ ๐ป)) |
6 | | id 22 |
. . . . . . 7
โข (โ = ๐ป โ โ = ๐ป) |
7 | 6 | sqxpeqd 5652 |
. . . . . 6
โข (โ = ๐ป โ (โ ร โ) = (๐ป ร ๐ป)) |
8 | 7 | imaeq2d 5999 |
. . . . 5
โข (โ = ๐ป โ ( +โ โ
(โ ร โ)) = ( +โ
โ (๐ป ร ๐ป))) |
9 | 8, 6 | sseq12d 3965 |
. . . 4
โข (โ = ๐ป โ (( +โ โ
(โ ร โ)) โ โ โ ( +โ โ (๐ป ร ๐ป)) โ ๐ป)) |
10 | | xpeq2 5641 |
. . . . . 6
โข (โ = ๐ป โ (โ ร โ) = (โ ร ๐ป)) |
11 | 10 | imaeq2d 5999 |
. . . . 5
โข (โ = ๐ป โ ( ยทโ
โ (โ ร โ))
= ( ยทโ โ (โ ร ๐ป))) |
12 | 11, 6 | sseq12d 3965 |
. . . 4
โข (โ = ๐ป โ ((
ยทโ โ (โ ร โ)) โ โ โ ( ยทโ
โ (โ ร ๐ป)) โ ๐ป)) |
13 | 5, 9, 12 | 3anbi123d 1435 |
. . 3
โข (โ = ๐ป โ ((0โ โ โ โง ( +โ
โ (โ ร โ)) โ โ โง ( ยทโ
โ (โ ร โ))
โ โ) โ
(0โ โ ๐ป โง ( +โ โ (๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป))) |
14 | | df-sh 29857 |
. . 3
โข
Sโ = {โ โ ๐ซ โ โฃ
(0โ โ โ โง ( +โ โ (โ ร โ)) โ โ โง ( ยทโ
โ (โ ร โ))
โ โ)} |
15 | 13, 14 | elrab2 3637 |
. 2
โข (๐ป โ
Sโ โ (๐ป โ ๐ซ โ โง
(0โ โ ๐ป โง ( +โ โ (๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป))) |
16 | | anass 469 |
. 2
โข (((๐ป โ โ โง
0โ โ ๐ป) โง (( +โ โ
(๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป)) โ (๐ป โ โ โง (0โ
โ ๐ป โง ((
+โ โ (๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป)))) |
17 | 4, 15, 16 | 3bitr4i 302 |
1
โข (๐ป โ
Sโ โ ((๐ป โ โ โง 0โ
โ ๐ป) โง ((
+โ โ (๐ป ร ๐ป)) โ ๐ป โง ( ยทโ
โ (โ ร ๐ป)) โ ๐ป))) |