Step | Hyp | Ref
| Expression |
1 | | phtpcer 24502 |
. . . 4
โข (
โphโ๐ฝ) Er (II Cn ๐ฝ) |
2 | 1 | a1i 11 |
. . 3
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (
โphโ๐ฝ) Er (II Cn ๐ฝ)) |
3 | | pcophtb.1 |
. . . . . . . 8
โข (๐ โ (๐นโ1) = (๐บโ1)) |
4 | | pcophtb.g |
. . . . . . . . . 10
โข (๐ โ ๐บ โ (II Cn ๐ฝ)) |
5 | | pcophtb.h |
. . . . . . . . . . 11
โข ๐ป = (๐ฅ โ (0[,]1) โฆ (๐บโ(1 โ ๐ฅ))) |
6 | 5 | pcorevcl 24532 |
. . . . . . . . . 10
โข (๐บ โ (II Cn ๐ฝ) โ (๐ป โ (II Cn ๐ฝ) โง (๐ปโ0) = (๐บโ1) โง (๐ปโ1) = (๐บโ0))) |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ป โ (II Cn ๐ฝ) โง (๐ปโ0) = (๐บโ1) โง (๐ปโ1) = (๐บโ0))) |
8 | 7 | simp2d 1143 |
. . . . . . . 8
โข (๐ โ (๐ปโ0) = (๐บโ1)) |
9 | 3, 8 | eqtr4d 2775 |
. . . . . . 7
โข (๐ โ (๐นโ1) = (๐ปโ0)) |
10 | 7 | simp1d 1142 |
. . . . . . . 8
โข (๐ โ ๐ป โ (II Cn ๐ฝ)) |
11 | 10, 4 | pco0 24521 |
. . . . . . 7
โข (๐ โ ((๐ป(*๐โ๐ฝ)๐บ)โ0) = (๐ปโ0)) |
12 | 9, 11 | eqtr4d 2775 |
. . . . . 6
โข (๐ โ (๐นโ1) = ((๐ป(*๐โ๐ฝ)๐บ)โ0)) |
13 | 12 | adantr 481 |
. . . . 5
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐นโ1) = ((๐ป(*๐โ๐ฝ)๐บ)โ0)) |
14 | | pcophtb.f |
. . . . . . 7
โข (๐ โ ๐น โ (II Cn ๐ฝ)) |
15 | 14 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ ๐น โ (II Cn ๐ฝ)) |
16 | 2, 15 | erref 8719 |
. . . . 5
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ ๐น( โphโ๐ฝ)๐น) |
17 | | eqid 2732 |
. . . . . . . 8
โข ((0[,]1)
ร {(๐บโ1)}) =
((0[,]1) ร {(๐บโ1)}) |
18 | 5, 17 | pcorev 24534 |
. . . . . . 7
โข (๐บ โ (II Cn ๐ฝ) โ (๐ป(*๐โ๐ฝ)๐บ)( โphโ๐ฝ)((0[,]1) ร {(๐บโ1)})) |
19 | 4, 18 | syl 17 |
. . . . . 6
โข (๐ โ (๐ป(*๐โ๐ฝ)๐บ)( โphโ๐ฝ)((0[,]1) ร {(๐บโ1)})) |
20 | 19 | adantr 481 |
. . . . 5
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐ป(*๐โ๐ฝ)๐บ)( โphโ๐ฝ)((0[,]1) ร {(๐บโ1)})) |
21 | 13, 16, 20 | pcohtpy 24527 |
. . . 4
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐น(*๐โ๐ฝ)(๐ป(*๐โ๐ฝ)๐บ))( โphโ๐ฝ)(๐น(*๐โ๐ฝ)((0[,]1) ร {(๐บโ1)}))) |
22 | 3 | adantr 481 |
. . . . 5
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐นโ1) = (๐บโ1)) |
23 | 17 | pcopt2 24530 |
. . . . 5
โข ((๐น โ (II Cn ๐ฝ) โง (๐นโ1) = (๐บโ1)) โ (๐น(*๐โ๐ฝ)((0[,]1) ร {(๐บโ1)}))(
โphโ๐ฝ)๐น) |
24 | 15, 22, 23 | syl2anc 584 |
. . . 4
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐น(*๐โ๐ฝ)((0[,]1) ร {(๐บโ1)}))(
โphโ๐ฝ)๐น) |
25 | 2, 21, 24 | ertrd 8715 |
. . 3
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐น(*๐โ๐ฝ)(๐ป(*๐โ๐ฝ)๐บ))( โphโ๐ฝ)๐น) |
26 | 10 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ ๐ป โ (II Cn ๐ฝ)) |
27 | 4 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ ๐บ โ (II Cn ๐ฝ)) |
28 | 9 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐นโ1) = (๐ปโ0)) |
29 | 7 | simp3d 1144 |
. . . . . . 7
โข (๐ โ (๐ปโ1) = (๐บโ0)) |
30 | 29 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐ปโ1) = (๐บโ0)) |
31 | | eqid 2732 |
. . . . . 6
โข (๐ฆ โ (0[,]1) โฆ if(๐ฆ โค (1 / 2), if(๐ฆ โค (1 / 4), (2 ยท ๐ฆ), (๐ฆ + (1 / 4))), ((๐ฆ / 2) + (1 / 2)))) = (๐ฆ โ (0[,]1) โฆ if(๐ฆ โค (1 / 2), if(๐ฆ โค (1 / 4), (2 ยท ๐ฆ), (๐ฆ + (1 / 4))), ((๐ฆ / 2) + (1 / 2)))) |
32 | 15, 26, 27, 28, 30, 31 | pcoass 24531 |
. . . . 5
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ ((๐น(*๐โ๐ฝ)๐ป)(*๐โ๐ฝ)๐บ)( โphโ๐ฝ)(๐น(*๐โ๐ฝ)(๐ป(*๐โ๐ฝ)๐บ))) |
33 | 14, 10 | pco1 24522 |
. . . . . . . 8
โข (๐ โ ((๐น(*๐โ๐ฝ)๐ป)โ1) = (๐ปโ1)) |
34 | 33, 29 | eqtrd 2772 |
. . . . . . 7
โข (๐ โ ((๐น(*๐โ๐ฝ)๐ป)โ1) = (๐บโ0)) |
35 | 34 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ ((๐น(*๐โ๐ฝ)๐ป)โ1) = (๐บโ0)) |
36 | | simpr 485 |
. . . . . 6
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) |
37 | 2, 27 | erref 8719 |
. . . . . 6
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ ๐บ( โphโ๐ฝ)๐บ) |
38 | 35, 36, 37 | pcohtpy 24527 |
. . . . 5
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ ((๐น(*๐โ๐ฝ)๐ป)(*๐โ๐ฝ)๐บ)( โphโ๐ฝ)(๐(*๐โ๐ฝ)๐บ)) |
39 | 2, 32, 38 | ertr3d 8717 |
. . . 4
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐น(*๐โ๐ฝ)(๐ป(*๐โ๐ฝ)๐บ))( โphโ๐ฝ)(๐(*๐โ๐ฝ)๐บ)) |
40 | | pcophtb.0 |
. . . . . . 7
โข (๐ โ (๐นโ0) = (๐บโ0)) |
41 | 40 | adantr 481 |
. . . . . 6
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐นโ0) = (๐บโ0)) |
42 | 41 | eqcomd 2738 |
. . . . 5
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐บโ0) = (๐นโ0)) |
43 | | pcophtb.p |
. . . . . 6
โข ๐ = ((0[,]1) ร {(๐นโ0)}) |
44 | 43 | pcopt 24529 |
. . . . 5
โข ((๐บ โ (II Cn ๐ฝ) โง (๐บโ0) = (๐นโ0)) โ (๐(*๐โ๐ฝ)๐บ)( โphโ๐ฝ)๐บ) |
45 | 27, 42, 44 | syl2anc 584 |
. . . 4
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐(*๐โ๐ฝ)๐บ)( โphโ๐ฝ)๐บ) |
46 | 2, 39, 45 | ertrd 8715 |
. . 3
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ (๐น(*๐โ๐ฝ)(๐ป(*๐โ๐ฝ)๐บ))( โphโ๐ฝ)๐บ) |
47 | 2, 25, 46 | ertr3d 8717 |
. 2
โข ((๐ โง (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) โ ๐น( โphโ๐ฝ)๐บ) |
48 | 1 | a1i 11 |
. . 3
โข ((๐ โง ๐น( โphโ๐ฝ)๐บ) โ (
โphโ๐ฝ) Er (II Cn ๐ฝ)) |
49 | 9 | adantr 481 |
. . . 4
โข ((๐ โง ๐น( โphโ๐ฝ)๐บ) โ (๐นโ1) = (๐ปโ0)) |
50 | | simpr 485 |
. . . 4
โข ((๐ โง ๐น( โphโ๐ฝ)๐บ) โ ๐น( โphโ๐ฝ)๐บ) |
51 | 10 | adantr 481 |
. . . . 5
โข ((๐ โง ๐น( โphโ๐ฝ)๐บ) โ ๐ป โ (II Cn ๐ฝ)) |
52 | 48, 51 | erref 8719 |
. . . 4
โข ((๐ โง ๐น( โphโ๐ฝ)๐บ) โ ๐ป( โphโ๐ฝ)๐ป) |
53 | 49, 50, 52 | pcohtpy 24527 |
. . 3
โข ((๐ โง ๐น( โphโ๐ฝ)๐บ) โ (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)(๐บ(*๐โ๐ฝ)๐ป)) |
54 | | eqid 2732 |
. . . . . . 7
โข ((0[,]1)
ร {(๐บโ0)}) =
((0[,]1) ร {(๐บโ0)}) |
55 | 5, 54 | pcorev2 24535 |
. . . . . 6
โข (๐บ โ (II Cn ๐ฝ) โ (๐บ(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)((0[,]1) ร {(๐บโ0)})) |
56 | 4, 55 | syl 17 |
. . . . 5
โข (๐ โ (๐บ(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)((0[,]1) ร {(๐บโ0)})) |
57 | 40 | sneqd 4639 |
. . . . . . 7
โข (๐ โ {(๐นโ0)} = {(๐บโ0)}) |
58 | 57 | xpeq2d 5705 |
. . . . . 6
โข (๐ โ ((0[,]1) ร {(๐นโ0)}) = ((0[,]1) ร
{(๐บโ0)})) |
59 | 43, 58 | eqtrid 2784 |
. . . . 5
โข (๐ โ ๐ = ((0[,]1) ร {(๐บโ0)})) |
60 | 56, 59 | breqtrrd 5175 |
. . . 4
โข (๐ โ (๐บ(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) |
61 | 60 | adantr 481 |
. . 3
โข ((๐ โง ๐น( โphโ๐ฝ)๐บ) โ (๐บ(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) |
62 | 48, 53, 61 | ertrd 8715 |
. 2
โข ((๐ โง ๐น( โphโ๐ฝ)๐บ) โ (๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐) |
63 | 47, 62 | impbida 799 |
1
โข (๐ โ ((๐น(*๐โ๐ฝ)๐ป)( โphโ๐ฝ)๐ โ ๐น( โphโ๐ฝ)๐บ)) |