Step | Hyp | Ref
| Expression |
1 | | pcoval.2 |
. . . . . . 7
โข (๐ โ ๐น โ (II Cn ๐ฝ)) |
2 | | iiuni 24397 |
. . . . . . . 8
โข (0[,]1) =
โช II |
3 | | eqid 2733 |
. . . . . . . 8
โข โช ๐ฝ =
โช ๐ฝ |
4 | 2, 3 | cnf 22750 |
. . . . . . 7
โข (๐น โ (II Cn ๐ฝ) โ ๐น:(0[,]1)โถโช
๐ฝ) |
5 | 1, 4 | syl 17 |
. . . . . 6
โข (๐ โ ๐น:(0[,]1)โถโช
๐ฝ) |
6 | | elii1 24451 |
. . . . . . 7
โข (๐ฅ โ (0[,](1 / 2)) โ
(๐ฅ โ (0[,]1) โง
๐ฅ โค (1 /
2))) |
7 | | iihalf1 24447 |
. . . . . . 7
โข (๐ฅ โ (0[,](1 / 2)) โ (2
ยท ๐ฅ) โ
(0[,]1)) |
8 | 6, 7 | sylbir 234 |
. . . . . 6
โข ((๐ฅ โ (0[,]1) โง ๐ฅ โค (1 / 2)) โ (2
ยท ๐ฅ) โ
(0[,]1)) |
9 | | fvco3 6991 |
. . . . . 6
โข ((๐น:(0[,]1)โถโช ๐ฝ
โง (2 ยท ๐ฅ) โ
(0[,]1)) โ ((๐ป โ
๐น)โ(2 ยท ๐ฅ)) = (๐ปโ(๐นโ(2 ยท ๐ฅ)))) |
10 | 5, 8, 9 | syl2an 597 |
. . . . 5
โข ((๐ โง (๐ฅ โ (0[,]1) โง ๐ฅ โค (1 / 2))) โ ((๐ป โ ๐น)โ(2 ยท ๐ฅ)) = (๐ปโ(๐นโ(2 ยท ๐ฅ)))) |
11 | 10 | anassrs 469 |
. . . 4
โข (((๐ โง ๐ฅ โ (0[,]1)) โง ๐ฅ โค (1 / 2)) โ ((๐ป โ ๐น)โ(2 ยท ๐ฅ)) = (๐ปโ(๐นโ(2 ยท ๐ฅ)))) |
12 | | pcoval.3 |
. . . . . . 7
โข (๐ โ ๐บ โ (II Cn ๐ฝ)) |
13 | 2, 3 | cnf 22750 |
. . . . . . 7
โข (๐บ โ (II Cn ๐ฝ) โ ๐บ:(0[,]1)โถโช
๐ฝ) |
14 | 12, 13 | syl 17 |
. . . . . 6
โข (๐ โ ๐บ:(0[,]1)โถโช
๐ฝ) |
15 | | elii2 24452 |
. . . . . . 7
โข ((๐ฅ โ (0[,]1) โง ยฌ
๐ฅ โค (1 / 2)) โ
๐ฅ โ ((1 /
2)[,]1)) |
16 | | iihalf2 24449 |
. . . . . . 7
โข (๐ฅ โ ((1 / 2)[,]1) โ ((2
ยท ๐ฅ) โ 1)
โ (0[,]1)) |
17 | 15, 16 | syl 17 |
. . . . . 6
โข ((๐ฅ โ (0[,]1) โง ยฌ
๐ฅ โค (1 / 2)) โ ((2
ยท ๐ฅ) โ 1)
โ (0[,]1)) |
18 | | fvco3 6991 |
. . . . . 6
โข ((๐บ:(0[,]1)โถโช ๐ฝ
โง ((2 ยท ๐ฅ)
โ 1) โ (0[,]1)) โ ((๐ป โ ๐บ)โ((2 ยท ๐ฅ) โ 1)) = (๐ปโ(๐บโ((2 ยท ๐ฅ) โ 1)))) |
19 | 14, 17, 18 | syl2an 597 |
. . . . 5
โข ((๐ โง (๐ฅ โ (0[,]1) โง ยฌ ๐ฅ โค (1 / 2))) โ ((๐ป โ ๐บ)โ((2 ยท ๐ฅ) โ 1)) = (๐ปโ(๐บโ((2 ยท ๐ฅ) โ 1)))) |
20 | 19 | anassrs 469 |
. . . 4
โข (((๐ โง ๐ฅ โ (0[,]1)) โง ยฌ ๐ฅ โค (1 / 2)) โ ((๐ป โ ๐บ)โ((2 ยท ๐ฅ) โ 1)) = (๐ปโ(๐บโ((2 ยท ๐ฅ) โ 1)))) |
21 | 11, 20 | ifeq12da 4562 |
. . 3
โข ((๐ โง ๐ฅ โ (0[,]1)) โ if(๐ฅ โค (1 / 2), ((๐ป โ ๐น)โ(2 ยท ๐ฅ)), ((๐ป โ ๐บ)โ((2 ยท ๐ฅ) โ 1))) = if(๐ฅ โค (1 / 2), (๐ปโ(๐นโ(2 ยท ๐ฅ))), (๐ปโ(๐บโ((2 ยท ๐ฅ) โ 1))))) |
22 | 21 | mpteq2dva 5249 |
. 2
โข (๐ โ (๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), ((๐ป โ ๐น)โ(2 ยท ๐ฅ)), ((๐ป โ ๐บ)โ((2 ยท ๐ฅ) โ 1)))) = (๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), (๐ปโ(๐นโ(2 ยท ๐ฅ))), (๐ปโ(๐บโ((2 ยท ๐ฅ) โ 1)))))) |
23 | | copco.6 |
. . . 4
โข (๐ โ ๐ป โ (๐ฝ Cn ๐พ)) |
24 | | cnco 22770 |
. . . 4
โข ((๐น โ (II Cn ๐ฝ) โง ๐ป โ (๐ฝ Cn ๐พ)) โ (๐ป โ ๐น) โ (II Cn ๐พ)) |
25 | 1, 23, 24 | syl2anc 585 |
. . 3
โข (๐ โ (๐ป โ ๐น) โ (II Cn ๐พ)) |
26 | | cnco 22770 |
. . . 4
โข ((๐บ โ (II Cn ๐ฝ) โง ๐ป โ (๐ฝ Cn ๐พ)) โ (๐ป โ ๐บ) โ (II Cn ๐พ)) |
27 | 12, 23, 26 | syl2anc 585 |
. . 3
โข (๐ โ (๐ป โ ๐บ) โ (II Cn ๐พ)) |
28 | 25, 27 | pcoval 24527 |
. 2
โข (๐ โ ((๐ป โ ๐น)(*๐โ๐พ)(๐ป โ ๐บ)) = (๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), ((๐ป โ ๐น)โ(2 ยท ๐ฅ)), ((๐ป โ ๐บ)โ((2 ยท ๐ฅ) โ 1))))) |
29 | 1, 12 | pcoval 24527 |
. . . . . 6
โข (๐ โ (๐น(*๐โ๐ฝ)๐บ) = (๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1))))) |
30 | | pcoval2.4 |
. . . . . . 7
โข (๐ โ (๐นโ1) = (๐บโ0)) |
31 | 1, 12, 30 | pcocn 24533 |
. . . . . 6
โข (๐ โ (๐น(*๐โ๐ฝ)๐บ) โ (II Cn ๐ฝ)) |
32 | 29, 31 | eqeltrrd 2835 |
. . . . 5
โข (๐ โ (๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1)))) โ (II Cn ๐ฝ)) |
33 | 2, 3 | cnf 22750 |
. . . . 5
โข ((๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1)))) โ (II Cn ๐ฝ) โ (๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1)))):(0[,]1)โถโช ๐ฝ) |
34 | 32, 33 | syl 17 |
. . . 4
โข (๐ โ (๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1)))):(0[,]1)โถโช ๐ฝ) |
35 | | eqid 2733 |
. . . . 5
โข (๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1)))) = (๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1)))) |
36 | 35 | fmpt 7110 |
. . . 4
โข
(โ๐ฅ โ
(0[,]1)if(๐ฅ โค (1 / 2),
(๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1))) โ โช ๐ฝ
โ (๐ฅ โ (0[,]1)
โฆ if(๐ฅ โค (1 / 2),
(๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1)))):(0[,]1)โถโช ๐ฝ) |
37 | 34, 36 | sylibr 233 |
. . 3
โข (๐ โ โ๐ฅ โ (0[,]1)if(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1))) โ โช ๐ฝ) |
38 | | eqid 2733 |
. . . . . 6
โข โช ๐พ =
โช ๐พ |
39 | 3, 38 | cnf 22750 |
. . . . 5
โข (๐ป โ (๐ฝ Cn ๐พ) โ ๐ป:โช ๐ฝโถโช ๐พ) |
40 | 23, 39 | syl 17 |
. . . 4
โข (๐ โ ๐ป:โช ๐ฝโถโช ๐พ) |
41 | 40 | feqmptd 6961 |
. . 3
โข (๐ โ ๐ป = (๐ฆ โ โช ๐ฝ โฆ (๐ปโ๐ฆ))) |
42 | | fveq2 6892 |
. . . 4
โข (๐ฆ = if(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1))) โ (๐ปโ๐ฆ) = (๐ปโif(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1))))) |
43 | | fvif 6908 |
. . . 4
โข (๐ปโif(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1)))) = if(๐ฅ โค (1 / 2), (๐ปโ(๐นโ(2 ยท ๐ฅ))), (๐ปโ(๐บโ((2 ยท ๐ฅ) โ 1)))) |
44 | 42, 43 | eqtrdi 2789 |
. . 3
โข (๐ฆ = if(๐ฅ โค (1 / 2), (๐นโ(2 ยท ๐ฅ)), (๐บโ((2 ยท ๐ฅ) โ 1))) โ (๐ปโ๐ฆ) = if(๐ฅ โค (1 / 2), (๐ปโ(๐นโ(2 ยท ๐ฅ))), (๐ปโ(๐บโ((2 ยท ๐ฅ) โ 1))))) |
45 | 37, 29, 41, 44 | fmptcof 7128 |
. 2
โข (๐ โ (๐ป โ (๐น(*๐โ๐ฝ)๐บ)) = (๐ฅ โ (0[,]1) โฆ if(๐ฅ โค (1 / 2), (๐ปโ(๐นโ(2 ยท ๐ฅ))), (๐ปโ(๐บโ((2 ยท ๐ฅ) โ 1)))))) |
46 | 22, 28, 45 | 3eqtr4rd 2784 |
1
โข (๐ โ (๐ป โ (๐น(*๐โ๐ฝ)๐บ)) = ((๐ป โ ๐น)(*๐โ๐พ)(๐ป โ ๐บ))) |