Step | Hyp | Ref
| Expression |
1 | | eluzelz 12829 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
2 | 1 | adantl 483 |
. . . . . . . . . . . 12
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โค) |
3 | | nfra1 3282 |
. . . . . . . . . . . . . . . . 17
โข
โฒ๐โ๐ โ ๐ด ( I โ๐ต) = ( I โ๐ถ) |
4 | | rsp 3245 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โ (๐ โ ๐ด โ ( I โ๐ต) = ( I โ๐ถ))) |
5 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โค) โ (๐ โ ๐ด โ ( I โ๐ต) = ( I โ๐ถ))) |
6 | | ifeq1 4532 |
. . . . . . . . . . . . . . . . . . . 20
โข (( I
โ๐ต) = ( I
โ๐ถ) โ if(๐ โ ๐ด, ( I โ๐ต), ( I โ1)) = if(๐ โ ๐ด, ( I โ๐ถ), ( I โ1))) |
7 | 5, 6 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โค) โ (๐ โ ๐ด โ if(๐ โ ๐ด, ( I โ๐ต), ( I โ1)) = if(๐ โ ๐ด, ( I โ๐ถ), ( I โ1)))) |
8 | | iffalse 4537 |
. . . . . . . . . . . . . . . . . . . 20
โข (ยฌ
๐ โ ๐ด โ if(๐ โ ๐ด, ( I โ๐ต), ( I โ1)) = ( I
โ1)) |
9 | | iffalse 4537 |
. . . . . . . . . . . . . . . . . . . 20
โข (ยฌ
๐ โ ๐ด โ if(๐ โ ๐ด, ( I โ๐ถ), ( I โ1)) = ( I
โ1)) |
10 | 8, 9 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . 19
โข (ยฌ
๐ โ ๐ด โ if(๐ โ ๐ด, ( I โ๐ต), ( I โ1)) = if(๐ โ ๐ด, ( I โ๐ถ), ( I โ1))) |
11 | 7, 10 | pm2.61d1 180 |
. . . . . . . . . . . . . . . . . 18
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โค) โ if(๐ โ ๐ด, ( I โ๐ต), ( I โ1)) = if(๐ โ ๐ด, ( I โ๐ถ), ( I โ1))) |
12 | | fvif 6905 |
. . . . . . . . . . . . . . . . . 18
โข ( I
โif(๐ โ ๐ด, ๐ต, 1)) = if(๐ โ ๐ด, ( I โ๐ต), ( I โ1)) |
13 | | fvif 6905 |
. . . . . . . . . . . . . . . . . 18
โข ( I
โif(๐ โ ๐ด, ๐ถ, 1)) = if(๐ โ ๐ด, ( I โ๐ถ), ( I โ1)) |
14 | 11, 12, 13 | 3eqtr4g 2798 |
. . . . . . . . . . . . . . . . 17
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โค) โ ( I โif(๐ โ ๐ด, ๐ต, 1)) = ( I โif(๐ โ ๐ด, ๐ถ, 1))) |
15 | 3, 14 | mpteq2da 5246 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โ (๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ต, 1))) = (๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ถ, 1)))) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . . 15
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ฅ โ (โคโฅโ๐)) โ (๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ต, 1))) = (๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ถ, 1)))) |
17 | 16 | fveq1d 6891 |
. . . . . . . . . . . . . 14
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ฅ โ (โคโฅโ๐)) โ ((๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ต, 1)))โ๐ฅ) = ((๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ถ, 1)))โ๐ฅ)) |
18 | 17 | adantlr 714 |
. . . . . . . . . . . . 13
โข
(((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ (โคโฅโ๐)) โง ๐ฅ โ (โคโฅโ๐)) โ ((๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ต, 1)))โ๐ฅ) = ((๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ถ, 1)))โ๐ฅ)) |
19 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) |
20 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โฆ ( I
โif(๐ โ ๐ด, ๐ต, 1))) = (๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ต, 1))) |
21 | 19, 20 | fvmptex 7010 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))โ๐ฅ) = ((๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ต, 1)))โ๐ฅ) |
22 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1)) = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1)) |
23 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โฆ ( I
โif(๐ โ ๐ด, ๐ถ, 1))) = (๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ถ, 1))) |
24 | 22, 23 | fvmptex 7010 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))โ๐ฅ) = ((๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ถ, 1)))โ๐ฅ) |
25 | 18, 21, 24 | 3eqtr4g 2798 |
. . . . . . . . . . . 12
โข
(((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ (โคโฅโ๐)) โง ๐ฅ โ (โคโฅโ๐)) โ ((๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))โ๐ฅ) = ((๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))โ๐ฅ)) |
26 | 2, 25 | seqfeq 13990 |
. . . . . . . . . . 11
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ (โคโฅโ๐)) โ seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) = seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1)))) |
27 | 26 | breq1d 5158 |
. . . . . . . . . 10
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ (โคโฅโ๐)) โ (seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ โ seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฆ)) |
28 | 27 | anbi2d 630 |
. . . . . . . . 9
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ (โคโฅโ๐)) โ ((๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โ (๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฆ))) |
29 | 28 | exbidv 1925 |
. . . . . . . 8
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ (โคโฅโ๐)) โ (โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฆ))) |
30 | 29 | rexbidva 3177 |
. . . . . . 7
โข
(โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โ (โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โ โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฆ))) |
31 | 30 | adantr 482 |
. . . . . 6
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โค) โ (โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โ โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฆ))) |
32 | | simpr 486 |
. . . . . . . 8
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โค) โ ๐ โ โค) |
33 | 15 | adantr 482 |
. . . . . . . . . . 11
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ฅ โ (โคโฅโ๐)) โ (๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ต, 1))) = (๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ถ, 1)))) |
34 | 33 | fveq1d 6891 |
. . . . . . . . . 10
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ฅ โ (โคโฅโ๐)) โ ((๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ต, 1)))โ๐ฅ) = ((๐ โ โค โฆ ( I โif(๐ โ ๐ด, ๐ถ, 1)))โ๐ฅ)) |
35 | 34, 21, 24 | 3eqtr4g 2798 |
. . . . . . . . 9
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ฅ โ (โคโฅโ๐)) โ ((๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))โ๐ฅ) = ((๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))โ๐ฅ)) |
36 | 35 | adantlr 714 |
. . . . . . . 8
โข
(((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โค) โง ๐ฅ โ (โคโฅโ๐)) โ ((๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))โ๐ฅ) = ((๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))โ๐ฅ)) |
37 | 32, 36 | seqfeq 13990 |
. . . . . . 7
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โค) โ seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) = seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1)))) |
38 | 37 | breq1d 5158 |
. . . . . 6
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โค) โ (seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ โ seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฅ)) |
39 | 31, 38 | 3anbi23d 1440 |
. . . . 5
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โค) โ ((๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โ (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฅ))) |
40 | 39 | rexbidva 3177 |
. . . 4
โข
(โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โ (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โ โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฅ))) |
41 | | simplr 768 |
. . . . . . . . . 10
โข
(((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โ ๐ โ โ) |
42 | | nnuz 12862 |
. . . . . . . . . 10
โข โ =
(โคโฅโ1) |
43 | 41, 42 | eleqtrdi 2844 |
. . . . . . . . 9
โข
(((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โ ๐ โ
(โคโฅโ1)) |
44 | | f1of 6831 |
. . . . . . . . . . . . . 14
โข (๐:(1...๐)โ1-1-ontoโ๐ด โ ๐:(1...๐)โถ๐ด) |
45 | 44 | ad2antlr 726 |
. . . . . . . . . . . . 13
โข
((((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ฅ โ (1...๐)) โ ๐:(1...๐)โถ๐ด) |
46 | | ffvelcdm 7081 |
. . . . . . . . . . . . 13
โข ((๐:(1...๐)โถ๐ด โง ๐ฅ โ (1...๐)) โ (๐โ๐ฅ) โ ๐ด) |
47 | 45, 46 | sylancom 589 |
. . . . . . . . . . . 12
โข
((((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ฅ โ (1...๐)) โ (๐โ๐ฅ) โ ๐ด) |
48 | | simplll 774 |
. . . . . . . . . . . 12
โข
((((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ฅ โ (1...๐)) โ โ๐ โ ๐ด ( I โ๐ต) = ( I โ๐ถ)) |
49 | | nfcsb1v 3918 |
. . . . . . . . . . . . . 14
โข
โฒ๐โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ต) |
50 | | nfcsb1v 3918 |
. . . . . . . . . . . . . 14
โข
โฒ๐โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ถ) |
51 | 49, 50 | nfeq 2917 |
. . . . . . . . . . . . 13
โข
โฒ๐โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ต) = โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ถ) |
52 | | csbeq1a 3907 |
. . . . . . . . . . . . . 14
โข (๐ = (๐โ๐ฅ) โ ( I โ๐ต) = โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ต)) |
53 | | csbeq1a 3907 |
. . . . . . . . . . . . . 14
โข (๐ = (๐โ๐ฅ) โ ( I โ๐ถ) = โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ถ)) |
54 | 52, 53 | eqeq12d 2749 |
. . . . . . . . . . . . 13
โข (๐ = (๐โ๐ฅ) โ (( I โ๐ต) = ( I โ๐ถ) โ โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ต) = โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ถ))) |
55 | 51, 54 | rspc 3601 |
. . . . . . . . . . . 12
โข ((๐โ๐ฅ) โ ๐ด โ (โ๐ โ ๐ด ( I โ๐ต) = ( I โ๐ถ) โ โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ต) = โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ถ))) |
56 | 47, 48, 55 | sylc 65 |
. . . . . . . . . . 11
โข
((((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ฅ โ (1...๐)) โ โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ต) = โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ถ)) |
57 | | fvex 6902 |
. . . . . . . . . . . 12
โข (๐โ๐ฅ) โ V |
58 | | csbfv2g 6938 |
. . . . . . . . . . . 12
โข ((๐โ๐ฅ) โ V โ โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ต) = ( I โโฆ(๐โ๐ฅ) / ๐โฆ๐ต)) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . 11
โข
โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ต) = ( I โโฆ(๐โ๐ฅ) / ๐โฆ๐ต) |
60 | | csbfv2g 6938 |
. . . . . . . . . . . 12
โข ((๐โ๐ฅ) โ V โ โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ถ) = ( I โโฆ(๐โ๐ฅ) / ๐โฆ๐ถ)) |
61 | 57, 60 | ax-mp 5 |
. . . . . . . . . . 11
โข
โฆ(๐โ๐ฅ) / ๐โฆ( I โ๐ถ) = ( I โโฆ(๐โ๐ฅ) / ๐โฆ๐ถ) |
62 | 56, 59, 61 | 3eqtr3g 2796 |
. . . . . . . . . 10
โข
((((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ฅ โ (1...๐)) โ ( I โโฆ(๐โ๐ฅ) / ๐โฆ๐ต) = ( I โโฆ(๐โ๐ฅ) / ๐โฆ๐ถ)) |
63 | | elfznn 13527 |
. . . . . . . . . . . 12
โข (๐ฅ โ (1...๐) โ ๐ฅ โ โ) |
64 | 63 | adantl 483 |
. . . . . . . . . . 11
โข
((((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ฅ โ (1...๐)) โ ๐ฅ โ โ) |
65 | | fveq2 6889 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฅ โ (๐โ๐) = (๐โ๐ฅ)) |
66 | 65 | csbeq1d 3897 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ โฆ(๐โ๐) / ๐โฆ๐ต = โฆ(๐โ๐ฅ) / ๐โฆ๐ต) |
67 | | eqid 2733 |
. . . . . . . . . . . 12
โข (๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ต) = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) |
68 | 66, 67 | fvmpti 6995 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ ((๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ต)โ๐ฅ) = ( I โโฆ(๐โ๐ฅ) / ๐โฆ๐ต)) |
69 | 64, 68 | syl 17 |
. . . . . . . . . 10
โข
((((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ฅ โ (1...๐)) โ ((๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต)โ๐ฅ) = ( I โโฆ(๐โ๐ฅ) / ๐โฆ๐ต)) |
70 | 65 | csbeq1d 3897 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ โฆ(๐โ๐) / ๐โฆ๐ถ = โฆ(๐โ๐ฅ) / ๐โฆ๐ถ) |
71 | | eqid 2733 |
. . . . . . . . . . . 12
โข (๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ถ) = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ) |
72 | 70, 71 | fvmpti 6995 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ ((๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ถ)โ๐ฅ) = ( I โโฆ(๐โ๐ฅ) / ๐โฆ๐ถ)) |
73 | 64, 72 | syl 17 |
. . . . . . . . . 10
โข
((((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ฅ โ (1...๐)) โ ((๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ)โ๐ฅ) = ( I โโฆ(๐โ๐ฅ) / ๐โฆ๐ถ)) |
74 | 62, 69, 73 | 3eqtr4d 2783 |
. . . . . . . . 9
โข
((((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ฅ โ (1...๐)) โ ((๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต)โ๐ฅ) = ((๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ)โ๐ฅ)) |
75 | 43, 74 | seqfveq 13989 |
. . . . . . . 8
โข
(((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โ (seq1( ยท ,
(๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ต))โ๐) = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ))โ๐)) |
76 | 75 | eqeq2d 2744 |
. . . . . . 7
โข
(((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โ (๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐) โ ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ))โ๐))) |
77 | 76 | pm5.32da 580 |
. . . . . 6
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โ ((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) โ (๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ))โ๐)))) |
78 | 77 | exbidv 1925 |
. . . . 5
โข
((โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โง ๐ โ โ) โ (โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ))โ๐)))) |
79 | 78 | rexbidva 3177 |
. . . 4
โข
(โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) โ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ))โ๐)))) |
80 | 40, 79 | orbi12d 918 |
. . 3
โข
(โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โ ((โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) โ (โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ))โ๐))))) |
81 | 80 | iotabidv 6525 |
. 2
โข
(โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โ (โฉ๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) = (โฉ๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ))โ๐))))) |
82 | | df-prod 15847 |
. 2
โข
โ๐ โ
๐ด ๐ต = (โฉ๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
83 | | df-prod 15847 |
. 2
โข
โ๐ โ
๐ด ๐ถ = (โฉ๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ถ, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ถ))โ๐)))) |
84 | 81, 82, 83 | 3eqtr4g 2798 |
1
โข
(โ๐ โ
๐ด ( I โ๐ต) = ( I โ๐ถ) โ โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ) |