Step | Hyp | Ref
| Expression |
1 | | psgnunilem3.l |
. . . 4
β’ (π β (β―βπ) = πΏ) |
2 | | psgnunilem3.w2 |
. . . 4
β’ (π β (β―βπ) β
β) |
3 | 1, 2 | eqeltrrd 2839 |
. . 3
β’ (π β πΏ β β) |
4 | 3 | nnnn0d 12480 |
. 2
β’ (π β πΏ β
β0) |
5 | | psgnunilem3.w1 |
. . . . . . 7
β’ (π β π β Word π) |
6 | | wrdf 14414 |
. . . . . . 7
β’ (π β Word π β π:(0..^(β―βπ))βΆπ) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ (π β π:(0..^(β―βπ))βΆπ) |
8 | | 0nn0 12435 |
. . . . . . . . 9
β’ 0 β
β0 |
9 | 8 | a1i 11 |
. . . . . . . 8
β’ (π β 0 β
β0) |
10 | 3 | nngt0d 12209 |
. . . . . . . 8
β’ (π β 0 < πΏ) |
11 | | elfzo0 13620 |
. . . . . . . 8
β’ (0 β
(0..^πΏ) β (0 β
β0 β§ πΏ
β β β§ 0 < πΏ)) |
12 | 9, 3, 10, 11 | syl3anbrc 1344 |
. . . . . . 7
β’ (π β 0 β (0..^πΏ)) |
13 | 1 | oveq2d 7378 |
. . . . . . 7
β’ (π β (0..^(β―βπ)) = (0..^πΏ)) |
14 | 12, 13 | eleqtrrd 2841 |
. . . . . 6
β’ (π β 0 β
(0..^(β―βπ))) |
15 | 7, 14 | ffvelcdmd 7041 |
. . . . 5
β’ (π β (πβ0) β π) |
16 | | eqid 2737 |
. . . . . 6
β’
(pmTrspβπ·) =
(pmTrspβπ·) |
17 | | psgnunilem3.t |
. . . . . 6
β’ π = ran (pmTrspβπ·) |
18 | 16, 17 | pmtrfmvdn0 19251 |
. . . . 5
β’ ((πβ0) β π β dom ((πβ0) β I ) β
β
) |
19 | 15, 18 | syl 17 |
. . . 4
β’ (π β dom ((πβ0) β I ) β
β
) |
20 | | n0 4311 |
. . . 4
β’ (dom
((πβ0) β I )
β β
β βπ π β dom ((πβ0) β I )) |
21 | 19, 20 | sylib 217 |
. . 3
β’ (π β βπ π β dom ((πβ0) β I )) |
22 | | fzonel 13593 |
. . . . . . . 8
β’ Β¬
πΏ β (0..^πΏ) |
23 | | simpr1 1195 |
. . . . . . . 8
β’ ((((πΊ Ξ£g
π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (πΏ β (0..^πΏ) β§ π β dom ((π€βπΏ) β I ) β§ βπ β (0..^πΏ) Β¬ π β dom ((π€βπ) β I ))) β πΏ β (0..^πΏ)) |
24 | 22, 23 | mto 196 |
. . . . . . 7
β’ Β¬
(((πΊ
Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (πΏ β (0..^πΏ) β§ π β dom ((π€βπΏ) β I ) β§ βπ β (0..^πΏ) Β¬ π β dom ((π€βπ) β I ))) |
25 | 24 | a1i 11 |
. . . . . 6
β’ (π€ β Word π β Β¬ (((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (πΏ β (0..^πΏ) β§ π β dom ((π€βπΏ) β I ) β§ βπ β (0..^πΏ) Β¬ π β dom ((π€βπ) β I )))) |
26 | 25 | nrex 3078 |
. . . . 5
β’ Β¬
βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (πΏ β (0..^πΏ) β§ π β dom ((π€βπΏ) β I ) β§ βπ β (0..^πΏ) Β¬ π β dom ((π€βπ) β I ))) |
27 | | eleq1 2826 |
. . . . . . . . . 10
β’ (π = 0 β (π β (0..^πΏ) β 0 β (0..^πΏ))) |
28 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = 0 β (π€βπ) = (π€β0)) |
29 | 28 | difeq1d 4086 |
. . . . . . . . . . . 12
β’ (π = 0 β ((π€βπ) β I ) = ((π€β0) β I )) |
30 | 29 | dmeqd 5866 |
. . . . . . . . . . 11
β’ (π = 0 β dom ((π€βπ) β I ) = dom ((π€β0) β I )) |
31 | 30 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π = 0 β (π β dom ((π€βπ) β I ) β π β dom ((π€β0) β I ))) |
32 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = 0 β (0..^π) = (0..^0)) |
33 | 32 | raleqdv 3316 |
. . . . . . . . . 10
β’ (π = 0 β (βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ) β βπ β (0..^0) Β¬ π β dom ((π€βπ) β I ))) |
34 | 27, 31, 33 | 3anbi123d 1437 |
. . . . . . . . 9
β’ (π = 0 β ((π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I )) β (0 β (0..^πΏ) β§ π β dom ((π€β0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((π€βπ) β I )))) |
35 | 34 | anbi2d 630 |
. . . . . . . 8
β’ (π = 0 β ((((πΊ Ξ£g
π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β (((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (0 β (0..^πΏ) β§ π β dom ((π€β0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((π€βπ) β I ))))) |
36 | 35 | rexbidv 3176 |
. . . . . . 7
β’ (π = 0 β (βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (0 β (0..^πΏ) β§ π β dom ((π€β0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((π€βπ) β I ))))) |
37 | 36 | imbi2d 341 |
. . . . . 6
β’ (π = 0 β (((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I )))) β ((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (0 β (0..^πΏ) β§ π β dom ((π€β0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((π€βπ) β I )))))) |
38 | | eleq1 2826 |
. . . . . . . . . . 11
β’ (π = π β (π β (0..^πΏ) β π β (0..^πΏ))) |
39 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = π β (π€βπ) = (π€βπ)) |
40 | 39 | difeq1d 4086 |
. . . . . . . . . . . . 13
β’ (π = π β ((π€βπ) β I ) = ((π€βπ) β I )) |
41 | 40 | dmeqd 5866 |
. . . . . . . . . . . 12
β’ (π = π β dom ((π€βπ) β I ) = dom ((π€βπ) β I )) |
42 | 41 | eleq2d 2824 |
. . . . . . . . . . 11
β’ (π = π β (π β dom ((π€βπ) β I ) β π β dom ((π€βπ) β I ))) |
43 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = π β (0..^π) = (0..^π)) |
44 | 43 | raleqdv 3316 |
. . . . . . . . . . 11
β’ (π = π β (βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ) β βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) |
45 | 38, 42, 44 | 3anbi123d 1437 |
. . . . . . . . . 10
β’ (π = π β ((π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I )) β (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I )))) |
46 | 45 | anbi2d 630 |
. . . . . . . . 9
β’ (π = π β ((((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β (((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))))) |
47 | 46 | rexbidv 3176 |
. . . . . . . 8
β’ (π = π β (βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))))) |
48 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π€ = π₯ β (πΊ Ξ£g π€) = (πΊ Ξ£g π₯)) |
49 | 48 | eqeq1d 2739 |
. . . . . . . . . . 11
β’ (π€ = π₯ β ((πΊ Ξ£g π€) = ( I βΎ π·) β (πΊ Ξ£g π₯) = ( I βΎ π·))) |
50 | | fveqeq2 6856 |
. . . . . . . . . . 11
β’ (π€ = π₯ β ((β―βπ€) = πΏ β (β―βπ₯) = πΏ)) |
51 | 49, 50 | anbi12d 632 |
. . . . . . . . . 10
β’ (π€ = π₯ β (((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β ((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ))) |
52 | | fveq1 6846 |
. . . . . . . . . . . . . 14
β’ (π€ = π₯ β (π€βπ) = (π₯βπ)) |
53 | 52 | difeq1d 4086 |
. . . . . . . . . . . . 13
β’ (π€ = π₯ β ((π€βπ) β I ) = ((π₯βπ) β I )) |
54 | 53 | dmeqd 5866 |
. . . . . . . . . . . 12
β’ (π€ = π₯ β dom ((π€βπ) β I ) = dom ((π₯βπ) β I )) |
55 | 54 | eleq2d 2824 |
. . . . . . . . . . 11
β’ (π€ = π₯ β (π β dom ((π€βπ) β I ) β π β dom ((π₯βπ) β I ))) |
56 | | fveq1 6846 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π₯ β (π€βπ) = (π₯βπ)) |
57 | 56 | difeq1d 4086 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π₯ β ((π€βπ) β I ) = ((π₯βπ) β I )) |
58 | 57 | dmeqd 5866 |
. . . . . . . . . . . . . . 15
β’ (π€ = π₯ β dom ((π€βπ) β I ) = dom ((π₯βπ) β I )) |
59 | 58 | eleq2d 2824 |
. . . . . . . . . . . . . 14
β’ (π€ = π₯ β (π β dom ((π€βπ) β I ) β π β dom ((π₯βπ) β I ))) |
60 | 59 | notbid 318 |
. . . . . . . . . . . . 13
β’ (π€ = π₯ β (Β¬ π β dom ((π€βπ) β I ) β Β¬ π β dom ((π₯βπ) β I ))) |
61 | 60 | ralbidv 3175 |
. . . . . . . . . . . 12
β’ (π€ = π₯ β (βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ) β βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))) |
62 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π₯βπ) = (π₯βπ)) |
63 | 62 | difeq1d 4086 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π₯βπ) β I ) = ((π₯βπ) β I )) |
64 | 63 | dmeqd 5866 |
. . . . . . . . . . . . . . 15
β’ (π = π β dom ((π₯βπ) β I ) = dom ((π₯βπ) β I )) |
65 | 64 | eleq2d 2824 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β dom ((π₯βπ) β I ) β π β dom ((π₯βπ) β I ))) |
66 | 65 | notbid 318 |
. . . . . . . . . . . . 13
β’ (π = π β (Β¬ π β dom ((π₯βπ) β I ) β Β¬ π β dom ((π₯βπ) β I ))) |
67 | 66 | cbvralvw 3228 |
. . . . . . . . . . . 12
β’
(βπ β
(0..^π) Β¬ π β dom ((π₯βπ) β I ) β βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I )) |
68 | 61, 67 | bitrdi 287 |
. . . . . . . . . . 11
β’ (π€ = π₯ β (βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ) β βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))) |
69 | 55, 68 | 3anbi23d 1440 |
. . . . . . . . . 10
β’ (π€ = π₯ β ((π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I )) β (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I )))) |
70 | 51, 69 | anbi12d 632 |
. . . . . . . . 9
β’ (π€ = π₯ β ((((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β (((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) |
71 | 70 | cbvrexvw 3229 |
. . . . . . . 8
β’
(βπ€ β
Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β βπ₯ β Word π(((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I )))) |
72 | 47, 71 | bitrdi 287 |
. . . . . . 7
β’ (π = π β (βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β βπ₯ β Word π(((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) |
73 | 72 | imbi2d 341 |
. . . . . 6
β’ (π = π β (((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I )))) β ((π β§ π β dom ((πβ0) β I )) β βπ₯ β Word π(((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I )))))) |
74 | | eleq1 2826 |
. . . . . . . . . 10
β’ (π = (π + 1) β (π β (0..^πΏ) β (π + 1) β (0..^πΏ))) |
75 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (π€βπ) = (π€β(π + 1))) |
76 | 75 | difeq1d 4086 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β ((π€βπ) β I ) = ((π€β(π + 1)) β I )) |
77 | 76 | dmeqd 5866 |
. . . . . . . . . . 11
β’ (π = (π + 1) β dom ((π€βπ) β I ) = dom ((π€β(π + 1)) β I )) |
78 | 77 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π = (π + 1) β (π β dom ((π€βπ) β I ) β π β dom ((π€β(π + 1)) β I ))) |
79 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (0..^π) = (0..^(π + 1))) |
80 | 79 | raleqdv 3316 |
. . . . . . . . . 10
β’ (π = (π + 1) β (βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ) β βπ β (0..^(π + 1)) Β¬ π β dom ((π€βπ) β I ))) |
81 | 74, 78, 80 | 3anbi123d 1437 |
. . . . . . . . 9
β’ (π = (π + 1) β ((π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I )) β ((π + 1) β (0..^πΏ) β§ π β dom ((π€β(π + 1)) β I ) β§ βπ β (0..^(π + 1)) Β¬ π β dom ((π€βπ) β I )))) |
82 | 81 | anbi2d 630 |
. . . . . . . 8
β’ (π = (π + 1) β ((((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β (((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ ((π + 1) β (0..^πΏ) β§ π β dom ((π€β(π + 1)) β I ) β§ βπ β (0..^(π + 1)) Β¬ π β dom ((π€βπ) β I ))))) |
83 | 82 | rexbidv 3176 |
. . . . . . 7
β’ (π = (π + 1) β (βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ ((π + 1) β (0..^πΏ) β§ π β dom ((π€β(π + 1)) β I ) β§ βπ β (0..^(π + 1)) Β¬ π β dom ((π€βπ) β I ))))) |
84 | 83 | imbi2d 341 |
. . . . . 6
β’ (π = (π + 1) β (((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I )))) β ((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ ((π + 1) β (0..^πΏ) β§ π β dom ((π€β(π + 1)) β I ) β§ βπ β (0..^(π + 1)) Β¬ π β dom ((π€βπ) β I )))))) |
85 | | eleq1 2826 |
. . . . . . . . . 10
β’ (π = πΏ β (π β (0..^πΏ) β πΏ β (0..^πΏ))) |
86 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = πΏ β (π€βπ) = (π€βπΏ)) |
87 | 86 | difeq1d 4086 |
. . . . . . . . . . . 12
β’ (π = πΏ β ((π€βπ) β I ) = ((π€βπΏ) β I )) |
88 | 87 | dmeqd 5866 |
. . . . . . . . . . 11
β’ (π = πΏ β dom ((π€βπ) β I ) = dom ((π€βπΏ) β I )) |
89 | 88 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π = πΏ β (π β dom ((π€βπ) β I ) β π β dom ((π€βπΏ) β I ))) |
90 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = πΏ β (0..^π) = (0..^πΏ)) |
91 | 90 | raleqdv 3316 |
. . . . . . . . . 10
β’ (π = πΏ β (βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ) β βπ β (0..^πΏ) Β¬ π β dom ((π€βπ) β I ))) |
92 | 85, 89, 91 | 3anbi123d 1437 |
. . . . . . . . 9
β’ (π = πΏ β ((π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I )) β (πΏ β (0..^πΏ) β§ π β dom ((π€βπΏ) β I ) β§ βπ β (0..^πΏ) Β¬ π β dom ((π€βπ) β I )))) |
93 | 92 | anbi2d 630 |
. . . . . . . 8
β’ (π = πΏ β ((((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β (((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (πΏ β (0..^πΏ) β§ π β dom ((π€βπΏ) β I ) β§ βπ β (0..^πΏ) Β¬ π β dom ((π€βπ) β I ))))) |
94 | 93 | rexbidv 3176 |
. . . . . . 7
β’ (π = πΏ β (βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I ))) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (πΏ β (0..^πΏ) β§ π β dom ((π€βπΏ) β I ) β§ βπ β (0..^πΏ) Β¬ π β dom ((π€βπ) β I ))))) |
95 | 94 | imbi2d 341 |
. . . . . 6
β’ (π = πΏ β (((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π€βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π€βπ) β I )))) β ((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (πΏ β (0..^πΏ) β§ π β dom ((π€βπΏ) β I ) β§ βπ β (0..^πΏ) Β¬ π β dom ((π€βπ) β I )))))) |
96 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β dom ((πβ0) β I )) β π β Word π) |
97 | | psgnunilem3.w3 |
. . . . . . . . 9
β’ (π β (πΊ Ξ£g π) = ( I βΎ π·)) |
98 | 97, 1 | jca 513 |
. . . . . . . 8
β’ (π β ((πΊ Ξ£g π) = ( I βΎ π·) β§ (β―βπ) = πΏ)) |
99 | 98 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β dom ((πβ0) β I )) β ((πΊ Ξ£g
π) = ( I βΎ π·) β§ (β―βπ) = πΏ)) |
100 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β dom ((πβ0) β I )) β 0 β
(0..^πΏ)) |
101 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β dom ((πβ0) β I )) β π β dom ((πβ0) β I )) |
102 | | ral0 4475 |
. . . . . . . . . 10
β’
βπ β
β
Β¬ π β dom
((πβπ) β I ) |
103 | | fzo0 13603 |
. . . . . . . . . . 11
β’ (0..^0) =
β
|
104 | 103 | raleqi 3314 |
. . . . . . . . . 10
β’
(βπ β
(0..^0) Β¬ π β dom
((πβπ) β I ) β
βπ β β
Β¬ π β dom ((πβπ) β I )) |
105 | 102, 104 | mpbir 230 |
. . . . . . . . 9
β’
βπ β
(0..^0) Β¬ π β dom
((πβπ) β I ) |
106 | 105 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β dom ((πβ0) β I )) β βπ β (0..^0) Β¬ π β dom ((πβπ) β I )) |
107 | 100, 101,
106 | 3jca 1129 |
. . . . . . 7
β’ ((π β§ π β dom ((πβ0) β I )) β (0 β
(0..^πΏ) β§ π β dom ((πβ0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((πβπ) β I ))) |
108 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π€ = π β (πΊ Ξ£g π€) = (πΊ Ξ£g π)) |
109 | 108 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (π€ = π β ((πΊ Ξ£g π€) = ( I βΎ π·) β (πΊ Ξ£g π) = ( I βΎ π·))) |
110 | | fveqeq2 6856 |
. . . . . . . . . 10
β’ (π€ = π β ((β―βπ€) = πΏ β (β―βπ) = πΏ)) |
111 | 109, 110 | anbi12d 632 |
. . . . . . . . 9
β’ (π€ = π β (((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β ((πΊ Ξ£g π) = ( I βΎ π·) β§ (β―βπ) = πΏ))) |
112 | | fveq1 6846 |
. . . . . . . . . . . . 13
β’ (π€ = π β (π€β0) = (πβ0)) |
113 | 112 | difeq1d 4086 |
. . . . . . . . . . . 12
β’ (π€ = π β ((π€β0) β I ) = ((πβ0) β I )) |
114 | 113 | dmeqd 5866 |
. . . . . . . . . . 11
β’ (π€ = π β dom ((π€β0) β I ) = dom ((πβ0) β I
)) |
115 | 114 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π€ = π β (π β dom ((π€β0) β I ) β π β dom ((πβ0) β I ))) |
116 | | fveq1 6846 |
. . . . . . . . . . . . . . 15
β’ (π€ = π β (π€βπ) = (πβπ)) |
117 | 116 | difeq1d 4086 |
. . . . . . . . . . . . . 14
β’ (π€ = π β ((π€βπ) β I ) = ((πβπ) β I )) |
118 | 117 | dmeqd 5866 |
. . . . . . . . . . . . 13
β’ (π€ = π β dom ((π€βπ) β I ) = dom ((πβπ) β I )) |
119 | 118 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ (π€ = π β (π β dom ((π€βπ) β I ) β π β dom ((πβπ) β I ))) |
120 | 119 | notbid 318 |
. . . . . . . . . . 11
β’ (π€ = π β (Β¬ π β dom ((π€βπ) β I ) β Β¬ π β dom ((πβπ) β I ))) |
121 | 120 | ralbidv 3175 |
. . . . . . . . . 10
β’ (π€ = π β (βπ β (0..^0) Β¬ π β dom ((π€βπ) β I ) β βπ β (0..^0) Β¬ π β dom ((πβπ) β I ))) |
122 | 115, 121 | 3anbi23d 1440 |
. . . . . . . . 9
β’ (π€ = π β ((0 β (0..^πΏ) β§ π β dom ((π€β0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((π€βπ) β I )) β (0 β (0..^πΏ) β§ π β dom ((πβ0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((πβπ) β I )))) |
123 | 111, 122 | anbi12d 632 |
. . . . . . . 8
β’ (π€ = π β ((((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (0 β (0..^πΏ) β§ π β dom ((π€β0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((π€βπ) β I ))) β (((πΊ Ξ£g π) = ( I βΎ π·) β§ (β―βπ) = πΏ) β§ (0 β (0..^πΏ) β§ π β dom ((πβ0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((πβπ) β I ))))) |
124 | 123 | rspcev 3584 |
. . . . . . 7
β’ ((π β Word π β§ (((πΊ Ξ£g π) = ( I βΎ π·) β§ (β―βπ) = πΏ) β§ (0 β (0..^πΏ) β§ π β dom ((πβ0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((πβπ) β I )))) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (0 β (0..^πΏ) β§ π β dom ((π€β0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((π€βπ) β I )))) |
125 | 96, 99, 107, 124 | syl12anc 836 |
. . . . . 6
β’ ((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (0 β (0..^πΏ) β§ π β dom ((π€β0) β I ) β§ βπ β (0..^0) Β¬ π β dom ((π€βπ) β I )))) |
126 | | psgnunilem3.g |
. . . . . . . . . 10
β’ πΊ = (SymGrpβπ·) |
127 | | psgnunilem3.d |
. . . . . . . . . . 11
β’ (π β π· β π) |
128 | 127 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β dom ((πβ0) β I )) β§ (π₯ β Word π β§ (((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) β π· β π) |
129 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ π β dom ((πβ0) β I )) β§ (π₯ β Word π β§ (((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) β π₯ β Word π) |
130 | | simpll 766 |
. . . . . . . . . . 11
β’ ((((πΊ Ξ£g
π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))) β (πΊ Ξ£g π₯) = ( I βΎ π·)) |
131 | 130 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π β§ π β dom ((πβ0) β I )) β§ (π₯ β Word π β§ (((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) β (πΊ Ξ£g π₯) = ( I βΎ π·)) |
132 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((πΊ Ξ£g
π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))) β (β―βπ₯) = πΏ) |
133 | 132 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π β§ π β dom ((πβ0) β I )) β§ (π₯ β Word π β§ (((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) β (β―βπ₯) = πΏ) |
134 | | simpr1 1195 |
. . . . . . . . . . 11
β’ ((((πΊ Ξ£g
π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))) β π β (0..^πΏ)) |
135 | 134 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π β§ π β dom ((πβ0) β I )) β§ (π₯ β Word π β§ (((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) β π β (0..^πΏ)) |
136 | | simpr2 1196 |
. . . . . . . . . . 11
β’ ((((πΊ Ξ£g
π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))) β π β dom ((π₯βπ) β I )) |
137 | 136 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π β§ π β dom ((πβ0) β I )) β§ (π₯ β Word π β§ (((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) β π β dom ((π₯βπ) β I )) |
138 | | simpr3 1197 |
. . . . . . . . . . 11
β’ ((((πΊ Ξ£g
π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))) β βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I )) |
139 | 138 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π β§ π β dom ((πβ0) β I )) β§ (π₯ β Word π β§ (((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) β βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I )) |
140 | | psgnunilem3.in |
. . . . . . . . . . . 12
β’ (π β Β¬ βπ₯ β Word π((β―βπ₯) = (πΏ β 2) β§ (πΊ Ξ£g π₯) = ( I βΎ π·))) |
141 | | fveqeq2 6856 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β ((β―βπ₯) = (πΏ β 2) β (β―βπ¦) = (πΏ β 2))) |
142 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β (πΊ Ξ£g π₯) = (πΊ Ξ£g π¦)) |
143 | 142 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β ((πΊ Ξ£g π₯) = ( I βΎ π·) β (πΊ Ξ£g π¦) = ( I βΎ π·))) |
144 | 141, 143 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (((β―βπ₯) = (πΏ β 2) β§ (πΊ Ξ£g π₯) = ( I βΎ π·)) β ((β―βπ¦) = (πΏ β 2) β§ (πΊ Ξ£g π¦) = ( I βΎ π·)))) |
145 | 144 | cbvrexvw 3229 |
. . . . . . . . . . . 12
β’
(βπ₯ β
Word π((β―βπ₯) = (πΏ β 2) β§ (πΊ Ξ£g π₯) = ( I βΎ π·)) β βπ¦ β Word π((β―βπ¦) = (πΏ β 2) β§ (πΊ Ξ£g π¦) = ( I βΎ π·))) |
146 | 140, 145 | sylnib 328 |
. . . . . . . . . . 11
β’ (π β Β¬ βπ¦ β Word π((β―βπ¦) = (πΏ β 2) β§ (πΊ Ξ£g π¦) = ( I βΎ π·))) |
147 | 146 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β dom ((πβ0) β I )) β§ (π₯ β Word π β§ (((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) β Β¬ βπ¦ β Word π((β―βπ¦) = (πΏ β 2) β§ (πΊ Ξ£g π¦) = ( I βΎ π·))) |
148 | 126, 17, 128, 129, 131, 133, 135, 137, 139, 147 | psgnunilem2 19284 |
. . . . . . . . 9
β’ (((π β§ π β dom ((πβ0) β I )) β§ (π₯ β Word π β§ (((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))))) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ ((π + 1) β (0..^πΏ) β§ π β dom ((π€β(π + 1)) β I ) β§ βπ β (0..^(π + 1)) Β¬ π β dom ((π€βπ) β I )))) |
149 | 148 | rexlimdvaa 3154 |
. . . . . . . 8
β’ ((π β§ π β dom ((πβ0) β I )) β (βπ₯ β Word π(((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I ))) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ ((π + 1) β (0..^πΏ) β§ π β dom ((π€β(π + 1)) β I ) β§ βπ β (0..^(π + 1)) Β¬ π β dom ((π€βπ) β I ))))) |
150 | 149 | a2i 14 |
. . . . . . 7
β’ (((π β§ π β dom ((πβ0) β I )) β βπ₯ β Word π(((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I )))) β ((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ ((π + 1) β (0..^πΏ) β§ π β dom ((π€β(π + 1)) β I ) β§ βπ β (0..^(π + 1)) Β¬ π β dom ((π€βπ) β I ))))) |
151 | 150 | a1i 11 |
. . . . . 6
β’ (π β β0
β (((π β§ π β dom ((πβ0) β I )) β βπ₯ β Word π(((πΊ Ξ£g π₯) = ( I βΎ π·) β§ (β―βπ₯) = πΏ) β§ (π β (0..^πΏ) β§ π β dom ((π₯βπ) β I ) β§ βπ β (0..^π) Β¬ π β dom ((π₯βπ) β I )))) β ((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ ((π + 1) β (0..^πΏ) β§ π β dom ((π€β(π + 1)) β I ) β§ βπ β (0..^(π + 1)) Β¬ π β dom ((π€βπ) β I )))))) |
152 | 37, 73, 84, 95, 125, 151 | nn0ind 12605 |
. . . . 5
β’ (πΏ β β0
β ((π β§ π β dom ((πβ0) β I )) β βπ€ β Word π(((πΊ Ξ£g π€) = ( I βΎ π·) β§ (β―βπ€) = πΏ) β§ (πΏ β (0..^πΏ) β§ π β dom ((π€βπΏ) β I ) β§ βπ β (0..^πΏ) Β¬ π β dom ((π€βπ) β I ))))) |
153 | 26, 152 | mtoi 198 |
. . . 4
β’ (πΏ β β0
β Β¬ (π β§ π β dom ((πβ0) β I ))) |
154 | 153 | con2i 139 |
. . 3
β’ ((π β§ π β dom ((πβ0) β I )) β Β¬ πΏ β
β0) |
155 | 21, 154 | exlimddv 1939 |
. 2
β’ (π β Β¬ πΏ β
β0) |
156 | 4, 155 | pm2.65i 193 |
1
β’ Β¬
π |