Step | Hyp | Ref
| Expression |
1 | | lmatfval.m |
. . 3
β’ π = (litMatβπ) |
2 | | lmatfval.w |
. . . 4
β’ (π β π β Word Word π) |
3 | | lmatval 32451 |
. . . 4
β’ (π β Word Word π β (litMatβπ) = (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) |
4 | 2, 3 | syl 17 |
. . 3
β’ (π β (litMatβπ) = (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) |
5 | 1, 4 | eqtrid 2785 |
. 2
β’ (π β π = (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) |
6 | | simprl 770 |
. . . 4
β’ ((π β§ (π = πΌ β§ π = π½)) β π = πΌ) |
7 | 6 | fvoveq1d 7380 |
. . 3
β’ ((π β§ (π = πΌ β§ π = π½)) β (πβ(π β 1)) = (πβ(πΌ β 1))) |
8 | | simprr 772 |
. . . 4
β’ ((π β§ (π = πΌ β§ π = π½)) β π = π½) |
9 | 8 | oveq1d 7373 |
. . 3
β’ ((π β§ (π = πΌ β§ π = π½)) β (π β 1) = (π½ β 1)) |
10 | 7, 9 | fveq12d 6850 |
. 2
β’ ((π β§ (π = πΌ β§ π = π½)) β ((πβ(π β 1))β(π β 1)) = ((πβ(πΌ β 1))β(π½ β 1))) |
11 | | lmatfval.i |
. . 3
β’ (π β πΌ β (1...π)) |
12 | | lmatfval.1 |
. . . 4
β’ (π β (β―βπ) = π) |
13 | 12 | oveq2d 7374 |
. . 3
β’ (π β (1...(β―βπ)) = (1...π)) |
14 | 11, 13 | eleqtrrd 2837 |
. 2
β’ (π β πΌ β (1...(β―βπ))) |
15 | | lmatfval.j |
. . 3
β’ (π β π½ β (1...π)) |
16 | | 1m1e0 12230 |
. . . . . 6
β’ (1
β 1) = 0 |
17 | | lmatfval.n |
. . . . . . . . 9
β’ (π β π β β) |
18 | | nnuz 12811 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
19 | 17, 18 | eleqtrdi 2844 |
. . . . . . . 8
β’ (π β π β
(β€β₯β1)) |
20 | | eluzfz1 13454 |
. . . . . . . 8
β’ (π β
(β€β₯β1) β 1 β (1...π)) |
21 | 19, 20 | syl 17 |
. . . . . . 7
β’ (π β 1 β (1...π)) |
22 | | fz1fzo0m1 13626 |
. . . . . . 7
β’ (1 β
(1...π) β (1 β
1) β (0..^π)) |
23 | 21, 22 | syl 17 |
. . . . . 6
β’ (π β (1 β 1) β
(0..^π)) |
24 | 16, 23 | eqeltrrid 2839 |
. . . . 5
β’ (π β 0 β (0..^π)) |
25 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π = 0) β π = 0) |
26 | 25 | eleq1d 2819 |
. . . . . . 7
β’ ((π β§ π = 0) β (π β (0..^π) β 0 β (0..^π))) |
27 | 25 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ π = 0) β (πβπ) = (πβ0)) |
28 | 27 | fveqeq2d 6851 |
. . . . . . 7
β’ ((π β§ π = 0) β ((β―β(πβπ)) = π β (β―β(πβ0)) = π)) |
29 | 26, 28 | imbi12d 345 |
. . . . . 6
β’ ((π β§ π = 0) β ((π β (0..^π) β (β―β(πβπ)) = π) β (0 β (0..^π) β (β―β(πβ0)) = π))) |
30 | | lmatfval.2 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (β―β(πβπ)) = π) |
31 | 30 | ex 414 |
. . . . . 6
β’ (π β (π β (0..^π) β (β―β(πβπ)) = π)) |
32 | 24, 29, 31 | vtocld 3510 |
. . . . 5
β’ (π β (0 β (0..^π) β (β―β(πβ0)) = π)) |
33 | 24, 32 | mpd 15 |
. . . 4
β’ (π β (β―β(πβ0)) = π) |
34 | 33 | oveq2d 7374 |
. . 3
β’ (π β (1...(β―β(πβ0))) = (1...π)) |
35 | 15, 34 | eleqtrrd 2837 |
. 2
β’ (π β π½ β (1...(β―β(πβ0)))) |
36 | | fz1fzo0m1 13626 |
. . . . . 6
β’ (πΌ β (1...π) β (πΌ β 1) β (0..^π)) |
37 | 11, 36 | syl 17 |
. . . . 5
β’ (π β (πΌ β 1) β (0..^π)) |
38 | 12 | oveq2d 7374 |
. . . . 5
β’ (π β (0..^(β―βπ)) = (0..^π)) |
39 | 37, 38 | eleqtrrd 2837 |
. . . 4
β’ (π β (πΌ β 1) β (0..^(β―βπ))) |
40 | | wrdsymbcl 14421 |
. . . 4
β’ ((π β Word Word π β§ (πΌ β 1) β (0..^(β―βπ))) β (πβ(πΌ β 1)) β Word π) |
41 | 2, 39, 40 | syl2anc 585 |
. . 3
β’ (π β (πβ(πΌ β 1)) β Word π) |
42 | | fz1fzo0m1 13626 |
. . . . 5
β’ (π½ β (1...π) β (π½ β 1) β (0..^π)) |
43 | 15, 42 | syl 17 |
. . . 4
β’ (π β (π½ β 1) β (0..^π)) |
44 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π = (πΌ β 1)) β π = (πΌ β 1)) |
45 | 44 | eleq1d 2819 |
. . . . . . . 8
β’ ((π β§ π = (πΌ β 1)) β (π β (0..^π) β (πΌ β 1) β (0..^π))) |
46 | 44 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π β§ π = (πΌ β 1)) β (πβπ) = (πβ(πΌ β 1))) |
47 | 46 | fveqeq2d 6851 |
. . . . . . . 8
β’ ((π β§ π = (πΌ β 1)) β ((β―β(πβπ)) = π β (β―β(πβ(πΌ β 1))) = π)) |
48 | 45, 47 | imbi12d 345 |
. . . . . . 7
β’ ((π β§ π = (πΌ β 1)) β ((π β (0..^π) β (β―β(πβπ)) = π) β ((πΌ β 1) β (0..^π) β (β―β(πβ(πΌ β 1))) = π))) |
49 | 37, 48, 31 | vtocld 3510 |
. . . . . 6
β’ (π β ((πΌ β 1) β (0..^π) β (β―β(πβ(πΌ β 1))) = π)) |
50 | 37, 49 | mpd 15 |
. . . . 5
β’ (π β (β―β(πβ(πΌ β 1))) = π) |
51 | 50 | oveq2d 7374 |
. . . 4
β’ (π β (0..^(β―β(πβ(πΌ β 1)))) = (0..^π)) |
52 | 43, 51 | eleqtrrd 2837 |
. . 3
β’ (π β (π½ β 1) β
(0..^(β―β(πβ(πΌ β 1))))) |
53 | | wrdsymbcl 14421 |
. . 3
β’ (((πβ(πΌ β 1)) β Word π β§ (π½ β 1) β
(0..^(β―β(πβ(πΌ β 1))))) β ((πβ(πΌ β 1))β(π½ β 1)) β π) |
54 | 41, 52, 53 | syl2anc 585 |
. 2
β’ (π β ((πβ(πΌ β 1))β(π½ β 1)) β π) |
55 | 5, 10, 14, 35, 54 | ovmpod 7508 |
1
β’ (π β (πΌππ½) = ((πβ(πΌ β 1))β(π½ β 1))) |