Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . 5
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | efgval.r |
. . . . 5
β’ βΌ = (
~FG βπΌ) |
3 | | efgval2.m |
. . . . 5
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
4 | | efgval2.t |
. . . . 5
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
5 | | efgred.d |
. . . . 5
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
6 | | efgred.s |
. . . . 5
β’ π = (π β {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
7 | 1, 2, 3, 4, 5, 6 | efgsfo 19528 |
. . . 4
β’ π:dom πβontoβπ |
8 | | foelrn 7061 |
. . . 4
β’ ((π:dom πβontoβπ β§ π΄ β π) β βπ β dom π π΄ = (πβπ)) |
9 | 7, 8 | mpan 689 |
. . 3
β’ (π΄ β π β βπ β dom π π΄ = (πβπ)) |
10 | 1, 2, 3, 4, 5, 6 | efgsdm 19519 |
. . . . . . 7
β’ (π β dom π β (π β (Word π β {β
}) β§ (πβ0) β π· β§ βπ β
(1..^(β―βπ))(πβπ) β ran (πβ(πβ(π β 1))))) |
11 | 10 | simp2bi 1147 |
. . . . . 6
β’ (π β dom π β (πβ0) β π·) |
12 | 1, 2, 3, 4, 5, 6 | efgsrel 19523 |
. . . . . . 7
β’ (π β dom π β (πβ0) βΌ (πβπ)) |
13 | 12 | adantl 483 |
. . . . . 6
β’ ((π΄ β π β§ π β dom π) β (πβ0) βΌ (πβπ)) |
14 | | breq1 5113 |
. . . . . . 7
β’ (π = (πβ0) β (π βΌ (πβπ) β (πβ0) βΌ (πβπ))) |
15 | 14 | rspcev 3584 |
. . . . . 6
β’ (((πβ0) β π· β§ (πβ0) βΌ (πβπ)) β βπ β π· π βΌ (πβπ)) |
16 | 11, 13, 15 | syl2an2 685 |
. . . . 5
β’ ((π΄ β π β§ π β dom π) β βπ β π· π βΌ (πβπ)) |
17 | | breq2 5114 |
. . . . . 6
β’ (π΄ = (πβπ) β (π βΌ π΄ β π βΌ (πβπ))) |
18 | 17 | rexbidv 3176 |
. . . . 5
β’ (π΄ = (πβπ) β (βπ β π· π βΌ π΄ β βπ β π· π βΌ (πβπ))) |
19 | 16, 18 | syl5ibrcom 247 |
. . . 4
β’ ((π΄ β π β§ π β dom π) β (π΄ = (πβπ) β βπ β π· π βΌ π΄)) |
20 | 19 | rexlimdva 3153 |
. . 3
β’ (π΄ β π β (βπ β dom π π΄ = (πβπ) β βπ β π· π βΌ π΄)) |
21 | 9, 20 | mpd 15 |
. 2
β’ (π΄ β π β βπ β π· π βΌ π΄) |
22 | 1, 2 | efger 19507 |
. . . . . . 7
β’ βΌ Er
π |
23 | 22 | a1i 11 |
. . . . . 6
β’ (((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β βΌ Er π) |
24 | | simprl 770 |
. . . . . 6
β’ (((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β π βΌ π΄) |
25 | | simprr 772 |
. . . . . 6
β’ (((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β π βΌ π΄) |
26 | 23, 24, 25 | ertr4d 8674 |
. . . . 5
β’ (((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β π βΌ π) |
27 | 1, 2, 3, 4, 5, 6 | efgrelex 19540 |
. . . . . 6
β’ (π βΌ π β βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0)) |
28 | | fofn 6763 |
. . . . . . . . . . . . . 14
β’ (π:dom πβontoβπ β π Fn dom π) |
29 | | fniniseg 7015 |
. . . . . . . . . . . . . 14
β’ (π Fn dom π β (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π))) |
30 | 7, 28, 29 | mp2b 10 |
. . . . . . . . . . . . 13
β’ (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π)) |
31 | 30 | simplbi 499 |
. . . . . . . . . . . 12
β’ (π β (β‘π β {π}) β π β dom π) |
32 | 31 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β dom π) |
33 | 1, 2, 3, 4, 5, 6 | efgsval 19520 |
. . . . . . . . . . 11
β’ (π β dom π β (πβπ) = (πβ((β―βπ) β 1))) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβπ) = (πβ((β―βπ) β 1))) |
35 | 30 | simprbi 498 |
. . . . . . . . . . 11
β’ (π β (β‘π β {π}) β (πβπ) = π) |
36 | 35 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβπ) = π) |
37 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (π β π· β§ π β π·)) |
38 | 37 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β π·) |
39 | 36, 38 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβπ) β π·) |
40 | 1, 2, 3, 4, 5, 6 | efgs1b 19525 |
. . . . . . . . . . . . . . 15
β’ (π β dom π β ((πβπ) β π· β (β―βπ) = 1)) |
41 | 32, 40 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β ((πβπ) β π· β (β―βπ) = 1)) |
42 | 39, 41 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (β―βπ) = 1) |
43 | 42 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β ((β―βπ) β 1) = (1 β
1)) |
44 | | 1m1e0 12232 |
. . . . . . . . . . . 12
β’ (1
β 1) = 0 |
45 | 43, 44 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β ((β―βπ) β 1) =
0) |
46 | 45 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβ((β―βπ) β 1)) = (πβ0)) |
47 | 34, 36, 46 | 3eqtr3rd 2786 |
. . . . . . . . 9
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβ0) = π) |
48 | | fniniseg 7015 |
. . . . . . . . . . . . . 14
β’ (π Fn dom π β (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π))) |
49 | 7, 28, 48 | mp2b 10 |
. . . . . . . . . . . . 13
β’ (π β (β‘π β {π}) β (π β dom π β§ (πβπ) = π)) |
50 | 49 | simplbi 499 |
. . . . . . . . . . . 12
β’ (π β (β‘π β {π}) β π β dom π) |
51 | 50 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β dom π) |
52 | 1, 2, 3, 4, 5, 6 | efgsval 19520 |
. . . . . . . . . . 11
β’ (π β dom π β (πβπ) = (πβ((β―βπ) β 1))) |
53 | 51, 52 | syl 17 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβπ) = (πβ((β―βπ) β 1))) |
54 | 49 | simprbi 498 |
. . . . . . . . . . 11
β’ (π β (β‘π β {π}) β (πβπ) = π) |
55 | 54 | ad2antll 728 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβπ) = π) |
56 | 37 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β π·) |
57 | 55, 56 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβπ) β π·) |
58 | 1, 2, 3, 4, 5, 6 | efgs1b 19525 |
. . . . . . . . . . . . . . 15
β’ (π β dom π β ((πβπ) β π· β (β―βπ) = 1)) |
59 | 51, 58 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β ((πβπ) β π· β (β―βπ) = 1)) |
60 | 57, 59 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (β―βπ) = 1) |
61 | 60 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β ((β―βπ) β 1) = (1 β
1)) |
62 | 61, 44 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β ((β―βπ) β 1) =
0) |
63 | 62 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβ((β―βπ) β 1)) = (πβ0)) |
64 | 53, 55, 63 | 3eqtr3rd 2786 |
. . . . . . . . 9
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β (πβ0) = π) |
65 | 47, 64 | eqeq12d 2753 |
. . . . . . . 8
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β ((πβ0) = (πβ0) β π = π)) |
66 | 65 | biimpd 228 |
. . . . . . 7
β’ ((((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β ((πβ0) = (πβ0) β π = π)) |
67 | 66 | rexlimdvva 3206 |
. . . . . 6
β’ (((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β (βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0) β π = π)) |
68 | 27, 67 | syl5 34 |
. . . . 5
β’ (((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β (π βΌ π β π = π)) |
69 | 26, 68 | mpd 15 |
. . . 4
β’ (((π΄ β π β§ (π β π· β§ π β π·)) β§ (π βΌ π΄ β§ π βΌ π΄)) β π = π) |
70 | 69 | ex 414 |
. . 3
β’ ((π΄ β π β§ (π β π· β§ π β π·)) β ((π βΌ π΄ β§ π βΌ π΄) β π = π)) |
71 | 70 | ralrimivva 3198 |
. 2
β’ (π΄ β π β βπ β π· βπ β π· ((π βΌ π΄ β§ π βΌ π΄) β π = π)) |
72 | | breq1 5113 |
. . 3
β’ (π = π β (π βΌ π΄ β π βΌ π΄)) |
73 | 72 | reu4 3694 |
. 2
β’
(β!π β
π· π βΌ π΄ β (βπ β π· π βΌ π΄ β§ βπ β π· βπ β π· ((π βΌ π΄ β§ π βΌ π΄) β π = π))) |
74 | 21, 71, 73 | sylanbrc 584 |
1
β’ (π΄ β π β β!π β π· π βΌ π΄) |