Step | Hyp | Ref
| Expression |
1 | | df-prod 15852 |
. 2
โข
โ๐ โ
๐ด ๐ต = (โฉ๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
2 | | fvex 6895 |
. . 3
โข (seq1(
ยท , ๐บ)โ๐) โ V |
3 | | nfcv 2895 |
. . . . . . . . 9
โข
โฒ๐if(๐ โ ๐ด, ๐ต, 1) |
4 | | nfv 1909 |
. . . . . . . . . 10
โข
โฒ๐ ๐ โ ๐ด |
5 | | nfcsb1v 3911 |
. . . . . . . . . 10
โข
โฒ๐โฆ๐ / ๐โฆ๐ต |
6 | | nfcv 2895 |
. . . . . . . . . 10
โข
โฒ๐1 |
7 | 4, 5, 6 | nfif 4551 |
. . . . . . . . 9
โข
โฒ๐if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1) |
8 | | eleq1w 2808 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ โ ๐ด โ ๐ โ ๐ด)) |
9 | | csbeq1a 3900 |
. . . . . . . . . 10
โข (๐ = ๐ โ ๐ต = โฆ๐ / ๐โฆ๐ต) |
10 | 8, 9 | ifbieq1d 4545 |
. . . . . . . . 9
โข (๐ = ๐ โ if(๐ โ ๐ด, ๐ต, 1) = if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
11 | 3, 7, 10 | cbvmpt 5250 |
. . . . . . . 8
โข (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) = (๐ โ โค โฆ if(๐ โ ๐ด, โฆ๐ / ๐โฆ๐ต, 1)) |
12 | | fprod.4 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
13 | 12 | ralrimiva 3138 |
. . . . . . . . 9
โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) |
14 | 5 | nfel1 2911 |
. . . . . . . . . 10
โข
โฒ๐โฆ๐ / ๐โฆ๐ต โ โ |
15 | 9 | eleq1d 2810 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ต โ โ โ โฆ๐ / ๐โฆ๐ต โ โ)) |
16 | 14, 15 | rspc 3592 |
. . . . . . . . 9
โข (๐ โ ๐ด โ (โ๐ โ ๐ด ๐ต โ โ โ โฆ๐ / ๐โฆ๐ต โ โ)) |
17 | 13, 16 | mpan9 506 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ โฆ๐ / ๐โฆ๐ต โ โ) |
18 | | fveq2 6882 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
19 | 18 | csbeq1d 3890 |
. . . . . . . . . 10
โข (๐ = ๐ โ โฆ(๐โ๐) / ๐โฆ๐ต = โฆ(๐โ๐) / ๐โฆ๐ต) |
20 | | csbcow 3901 |
. . . . . . . . . 10
โข
โฆ(๐โ๐) / ๐โฆโฆ๐ / ๐โฆ๐ต = โฆ(๐โ๐) / ๐โฆ๐ต |
21 | 19, 20 | eqtr4di 2782 |
. . . . . . . . 9
โข (๐ = ๐ โ โฆ(๐โ๐) / ๐โฆ๐ต = โฆ(๐โ๐) / ๐โฆโฆ๐ / ๐โฆ๐ต) |
22 | 21 | cbvmptv 5252 |
. . . . . . . 8
โข (๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ต) = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆโฆ๐ / ๐โฆ๐ต) |
23 | 11, 17, 22 | prodmo 15882 |
. . . . . . 7
โข (๐ โ โ*๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
24 | | fprod.2 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
25 | | fprod.3 |
. . . . . . . . . . . 12
โข (๐ โ ๐น:(1...๐)โ1-1-ontoโ๐ด) |
26 | | f1of 6824 |
. . . . . . . . . . . 12
โข (๐น:(1...๐)โ1-1-ontoโ๐ด โ ๐น:(1...๐)โถ๐ด) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐น:(1...๐)โถ๐ด) |
28 | | ovex 7435 |
. . . . . . . . . . 11
โข
(1...๐) โ
V |
29 | | fex 7220 |
. . . . . . . . . . 11
โข ((๐น:(1...๐)โถ๐ด โง (1...๐) โ V) โ ๐น โ V) |
30 | 27, 28, 29 | sylancl 585 |
. . . . . . . . . 10
โข (๐ โ ๐น โ V) |
31 | | nnuz 12864 |
. . . . . . . . . . . . 13
โข โ =
(โคโฅโ1) |
32 | 24, 31 | eleqtrdi 2835 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ
(โคโฅโ1)) |
33 | | fprod.5 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...๐)) โ (๐บโ๐) = ๐ถ) |
34 | | elfznn 13531 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...๐) โ ๐ โ โ) |
35 | | fvex 6895 |
. . . . . . . . . . . . . . . . 17
โข (๐บโ๐) โ V |
36 | 33, 35 | eqeltrrdi 2834 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...๐)) โ ๐ถ โ V) |
37 | | eqid 2724 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โฆ ๐ถ) = (๐ โ โ โฆ ๐ถ) |
38 | 37 | fvmpt2 7000 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ถ โ V) โ ((๐ โ โ โฆ ๐ถ)โ๐) = ๐ถ) |
39 | 34, 36, 38 | syl2an2 683 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...๐)) โ ((๐ โ โ โฆ ๐ถ)โ๐) = ๐ถ) |
40 | 33, 39 | eqtr4d 2767 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...๐)) โ (๐บโ๐) = ((๐ โ โ โฆ ๐ถ)โ๐)) |
41 | 40 | ralrimiva 3138 |
. . . . . . . . . . . . 13
โข (๐ โ โ๐ โ (1...๐)(๐บโ๐) = ((๐ โ โ โฆ ๐ถ)โ๐)) |
42 | | nffvmpt1 6893 |
. . . . . . . . . . . . . . 15
โข
โฒ๐((๐ โ โ โฆ ๐ถ)โ๐) |
43 | 42 | nfeq2 2912 |
. . . . . . . . . . . . . 14
โข
โฒ๐(๐บโ๐) = ((๐ โ โ โฆ ๐ถ)โ๐) |
44 | | fveq2 6882 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐บโ๐) = (๐บโ๐)) |
45 | | fveq2 6882 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ((๐ โ โ โฆ ๐ถ)โ๐) = ((๐ โ โ โฆ ๐ถ)โ๐)) |
46 | 44, 45 | eqeq12d 2740 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((๐บโ๐) = ((๐ โ โ โฆ ๐ถ)โ๐) โ (๐บโ๐) = ((๐ โ โ โฆ ๐ถ)โ๐))) |
47 | 43, 46 | rspc 3592 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ (โ๐ โ (1...๐)(๐บโ๐) = ((๐ โ โ โฆ ๐ถ)โ๐) โ (๐บโ๐) = ((๐ โ โ โฆ ๐ถ)โ๐))) |
48 | 41, 47 | mpan9 506 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...๐)) โ (๐บโ๐) = ((๐ โ โ โฆ ๐ถ)โ๐)) |
49 | 32, 48 | seqfveq 13993 |
. . . . . . . . . . 11
โข (๐ โ (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ ๐ถ))โ๐)) |
50 | 25, 49 | jca 511 |
. . . . . . . . . 10
โข (๐ โ (๐น:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ ๐ถ))โ๐))) |
51 | | f1oeq1 6812 |
. . . . . . . . . . 11
โข (๐ = ๐น โ (๐:(1...๐)โ1-1-ontoโ๐ด โ ๐น:(1...๐)โ1-1-ontoโ๐ด)) |
52 | | fveq1 6881 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐น โ (๐โ๐) = (๐นโ๐)) |
53 | 52 | csbeq1d 3890 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐น โ โฆ(๐โ๐) / ๐โฆ๐ต = โฆ(๐นโ๐) / ๐โฆ๐ต) |
54 | | fvex 6895 |
. . . . . . . . . . . . . . . . 17
โข (๐นโ๐) โ V |
55 | | fprod.1 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐นโ๐) โ ๐ต = ๐ถ) |
56 | 54, 55 | csbie 3922 |
. . . . . . . . . . . . . . . 16
โข
โฆ(๐นโ๐) / ๐โฆ๐ต = ๐ถ |
57 | 53, 56 | eqtrdi 2780 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐น โ โฆ(๐โ๐) / ๐โฆ๐ต = ๐ถ) |
58 | 57 | mpteq2dv 5241 |
. . . . . . . . . . . . . 14
โข (๐ = ๐น โ (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) = (๐ โ โ โฆ ๐ถ)) |
59 | 58 | seqeq3d 13975 |
. . . . . . . . . . . . 13
โข (๐ = ๐น โ seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต)) = seq1( ยท , (๐ โ โ โฆ ๐ถ))) |
60 | 59 | fveq1d 6884 |
. . . . . . . . . . . 12
โข (๐ = ๐น โ (seq1( ยท , (๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ต))โ๐) = (seq1( ยท , (๐ โ โ โฆ ๐ถ))โ๐)) |
61 | 60 | eqeq2d 2735 |
. . . . . . . . . . 11
โข (๐ = ๐น โ ((seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐) โ (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ ๐ถ))โ๐))) |
62 | 51, 61 | anbi12d 630 |
. . . . . . . . . 10
โข (๐ = ๐น โ ((๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) โ (๐น:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ ๐ถ))โ๐)))) |
63 | 30, 50, 62 | spcedv 3580 |
. . . . . . . . 9
โข (๐ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) |
64 | | oveq2 7410 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (1...๐) = (1...๐)) |
65 | 64 | f1oeq2d 6820 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐:(1...๐)โ1-1-ontoโ๐ด โ ๐:(1...๐)โ1-1-ontoโ๐ด)) |
66 | | fveq2 6882 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (seq1( ยท , (๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ต))โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) |
67 | 66 | eqeq2d 2735 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐) โ (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) |
68 | 65, 67 | anbi12d 630 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) โ (๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
69 | 68 | exbidv 1916 |
. . . . . . . . . 10
โข (๐ = ๐ โ (โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
70 | 69 | rspcev 3604 |
. . . . . . . . 9
โข ((๐ โ โ โง
โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) |
71 | 24, 63, 70 | syl2anc 583 |
. . . . . . . 8
โข (๐ โ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) |
72 | 71 | olcd 871 |
. . . . . . 7
โข (๐ โ (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ (seq1( ยท , ๐บ)โ๐)) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
73 | | breq2 5143 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (seq1( ยท , ๐บ)โ๐) โ (seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ โ seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ (seq1( ยท , ๐บ)โ๐))) |
74 | 73 | 3anbi3d 1438 |
. . . . . . . . . . . . 13
โข (๐ฅ = (seq1( ยท , ๐บ)โ๐) โ ((๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โ (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ (seq1( ยท , ๐บ)โ๐)))) |
75 | 74 | rexbidv 3170 |
. . . . . . . . . . . 12
โข (๐ฅ = (seq1( ยท , ๐บ)โ๐) โ (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โ โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ (seq1( ยท , ๐บ)โ๐)))) |
76 | | eqeq1 2728 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (seq1( ยท , ๐บ)โ๐) โ (๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐) โ (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) |
77 | 76 | anbi2d 628 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (seq1( ยท , ๐บ)โ๐) โ ((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) โ (๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
78 | 77 | exbidv 1916 |
. . . . . . . . . . . . 13
โข (๐ฅ = (seq1( ยท , ๐บ)โ๐) โ (โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
79 | 78 | rexbidv 3170 |
. . . . . . . . . . . 12
โข (๐ฅ = (seq1( ยท , ๐บ)โ๐) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) โ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
80 | 75, 79 | orbi12d 915 |
. . . . . . . . . . 11
โข (๐ฅ = (seq1( ยท , ๐บ)โ๐) โ ((โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โ (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ (seq1( ยท , ๐บ)โ๐)) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))))) |
81 | 80 | moi2 3705 |
. . . . . . . . . 10
โข ((((seq1(
ยท , ๐บ)โ๐) โ V โง โ*๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) โง ((โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โง (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ (seq1( ยท , ๐บ)โ๐)) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))))) โ ๐ฅ = (seq1( ยท , ๐บ)โ๐)) |
82 | 2, 81 | mpanl1 697 |
. . . . . . . . 9
โข
((โ*๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โง ((โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โง (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ (seq1( ยท , ๐บ)โ๐)) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))))) โ ๐ฅ = (seq1( ยท , ๐บ)โ๐)) |
83 | 82 | ancom2s 647 |
. . . . . . . 8
โข
((โ*๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โง ((โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ (seq1( ยท , ๐บ)โ๐)) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โง (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))))) โ ๐ฅ = (seq1( ยท , ๐บ)โ๐)) |
84 | 83 | expr 456 |
. . . . . . 7
โข
((โ*๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โง (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ (seq1( ยท , ๐บ)โ๐)) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) โ ((โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โ ๐ฅ = (seq1( ยท , ๐บ)โ๐))) |
85 | 23, 72, 84 | syl2anc 583 |
. . . . . 6
โข (๐ โ ((โ๐ โ โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โ ๐ฅ = (seq1( ยท , ๐บ)โ๐))) |
86 | 72, 80 | syl5ibrcom 246 |
. . . . . 6
โข (๐ โ (๐ฅ = (seq1( ยท , ๐บ)โ๐) โ (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))))) |
87 | 85, 86 | impbid 211 |
. . . . 5
โข (๐ โ ((โ๐ โ โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โ ๐ฅ = (seq1( ยท , ๐บ)โ๐))) |
88 | 87 | adantr 480 |
. . . 4
โข ((๐ โง (seq1( ยท , ๐บ)โ๐) โ V) โ ((โ๐ โ โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โ ๐ฅ = (seq1( ยท , ๐บ)โ๐))) |
89 | 88 | iota5 6517 |
. . 3
โข ((๐ โง (seq1( ยท , ๐บ)โ๐) โ V) โ (โฉ๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) = (seq1( ยท , ๐บ)โ๐)) |
90 | 2, 89 | mpan2 688 |
. 2
โข (๐ โ (โฉ๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) = (seq1( ยท , ๐บ)โ๐)) |
91 | 1, 90 | eqtrid 2776 |
1
โข (๐ โ โ๐ โ ๐ด ๐ต = (seq1( ยท , ๐บ)โ๐)) |