Step | Hyp | Ref
| Expression |
1 | | lmatfval.m |
. . . 4
β’ π = (litMatβπ) |
2 | | lmatfval.w |
. . . . 5
β’ (π β π β Word Word π) |
3 | | lmatval 32174 |
. . . . 5
β’ (π β Word Word π β (litMatβπ) = (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) |
4 | 2, 3 | syl 17 |
. . . 4
β’ (π β (litMatβπ) = (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) |
5 | 1, 4 | eqtrid 2790 |
. . 3
β’ (π β π = (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) |
6 | | lmatfval.1 |
. . . . 5
β’ (π β (β―βπ) = π) |
7 | 6 | oveq2d 7366 |
. . . 4
β’ (π β (1...(β―βπ)) = (1...π)) |
8 | | lmatfval.n |
. . . . . . 7
β’ (π β π β β) |
9 | | lbfzo0 13542 |
. . . . . . 7
β’ (0 β
(0..^π) β π β
β) |
10 | 8, 9 | sylibr 233 |
. . . . . 6
β’ (π β 0 β (0..^π)) |
11 | | 0nn0 12362 |
. . . . . . . 8
β’ 0 β
β0 |
12 | 11 | a1i 11 |
. . . . . . 7
β’ (π β 0 β
β0) |
13 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π = 0) β π = 0) |
14 | 13 | eleq1d 2823 |
. . . . . . . 8
β’ ((π β§ π = 0) β (π β (0..^π) β 0 β (0..^π))) |
15 | 13 | fveq2d 6842 |
. . . . . . . . 9
β’ ((π β§ π = 0) β (πβπ) = (πβ0)) |
16 | 15 | fveqeq2d 6846 |
. . . . . . . 8
β’ ((π β§ π = 0) β ((β―β(πβπ)) = π β (β―β(πβ0)) = π)) |
17 | 14, 16 | imbi12d 345 |
. . . . . . 7
β’ ((π β§ π = 0) β ((π β (0..^π) β (β―β(πβπ)) = π) β (0 β (0..^π) β (β―β(πβ0)) = π))) |
18 | | lmatfval.2 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (β―β(πβπ)) = π) |
19 | 18 | ex 414 |
. . . . . . 7
β’ (π β (π β (0..^π) β (β―β(πβπ)) = π)) |
20 | 12, 17, 19 | vtocld 3510 |
. . . . . 6
β’ (π β (0 β (0..^π) β (β―β(πβ0)) = π)) |
21 | 10, 20 | mpd 15 |
. . . . 5
β’ (π β (β―β(πβ0)) = π) |
22 | 21 | oveq2d 7366 |
. . . 4
β’ (π β (1...(β―β(πβ0))) = (1...π)) |
23 | | eqidd 2739 |
. . . 4
β’ (π β ((πβ(π β 1))β(π β 1)) = ((πβ(π β 1))β(π β 1))) |
24 | 7, 22, 23 | mpoeq123dv 7425 |
. . 3
β’ (π β (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1))) = (π β (1...π), π β (1...π) β¦ ((πβ(π β 1))β(π β 1)))) |
25 | 5, 24 | eqtrd 2778 |
. 2
β’ (π β π = (π β (1...π), π β (1...π) β¦ ((πβ(π β 1))β(π β 1)))) |
26 | | lmatcl.1 |
. . 3
β’ π = ((1...π) Mat π
) |
27 | | lmatcl.b |
. . 3
β’ π = (Baseβπ
) |
28 | | lmatcl.2 |
. . 3
β’ π = (Baseβπ) |
29 | | fzfid 13808 |
. . 3
β’ (π β (1...π) β Fin) |
30 | | lmatcl.r |
. . 3
β’ (π β π
β π) |
31 | 2 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π β (1...π) β§ π β (1...π)) β π β Word Word π) |
32 | | simp2 1138 |
. . . . . . 7
β’ ((π β§ π β (1...π) β§ π β (1...π)) β π β (1...π)) |
33 | | fz1fzo0m1 13550 |
. . . . . . 7
β’ (π β (1...π) β (π β 1) β (0..^π)) |
34 | 32, 33 | syl 17 |
. . . . . 6
β’ ((π β§ π β (1...π) β§ π β (1...π)) β (π β 1) β (0..^π)) |
35 | 6 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ π β (1...π) β§ π β (1...π)) β (β―βπ) = π) |
36 | 35 | oveq2d 7366 |
. . . . . 6
β’ ((π β§ π β (1...π) β§ π β (1...π)) β (0..^(β―βπ)) = (0..^π)) |
37 | 34, 36 | eleqtrrd 2842 |
. . . . 5
β’ ((π β§ π β (1...π) β§ π β (1...π)) β (π β 1) β (0..^(β―βπ))) |
38 | | wrdsymbcl 14344 |
. . . . 5
β’ ((π β Word Word π β§ (π β 1) β (0..^(β―βπ))) β (πβ(π β 1)) β Word π) |
39 | 31, 37, 38 | syl2anc 585 |
. . . 4
β’ ((π β§ π β (1...π) β§ π β (1...π)) β (πβ(π β 1)) β Word π) |
40 | | simp3 1139 |
. . . . . 6
β’ ((π β§ π β (1...π) β§ π β (1...π)) β π β (1...π)) |
41 | | fz1fzo0m1 13550 |
. . . . . 6
β’ (π β (1...π) β (π β 1) β (0..^π)) |
42 | 40, 41 | syl 17 |
. . . . 5
β’ ((π β§ π β (1...π) β§ π β (1...π)) β (π β 1) β (0..^π)) |
43 | | ovexd 7385 |
. . . . . . . . . 10
β’ (π β (π β 1) β V) |
44 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π = (π β 1)) β π = (π β 1)) |
45 | | eqidd 2739 |
. . . . . . . . . . . 12
β’ ((π β§ π = (π β 1)) β (0..^π) = (0..^π)) |
46 | 44, 45 | eleq12d 2833 |
. . . . . . . . . . 11
β’ ((π β§ π = (π β 1)) β (π β (0..^π) β (π β 1) β (0..^π))) |
47 | 44 | fveq2d 6842 |
. . . . . . . . . . . 12
β’ ((π β§ π = (π β 1)) β (πβπ) = (πβ(π β 1))) |
48 | 47 | fveqeq2d 6846 |
. . . . . . . . . . 11
β’ ((π β§ π = (π β 1)) β ((β―β(πβπ)) = π β (β―β(πβ(π β 1))) = π)) |
49 | 46, 48 | imbi12d 345 |
. . . . . . . . . 10
β’ ((π β§ π = (π β 1)) β ((π β (0..^π) β (β―β(πβπ)) = π) β ((π β 1) β (0..^π) β (β―β(πβ(π β 1))) = π))) |
50 | 43, 49, 19 | vtocld 3510 |
. . . . . . . . 9
β’ (π β ((π β 1) β (0..^π) β (β―β(πβ(π β 1))) = π)) |
51 | 50 | imp 408 |
. . . . . . . 8
β’ ((π β§ (π β 1) β (0..^π)) β (β―β(πβ(π β 1))) = π) |
52 | 33, 51 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (β―β(πβ(π β 1))) = π) |
53 | 52 | 3adant3 1133 |
. . . . . 6
β’ ((π β§ π β (1...π) β§ π β (1...π)) β (β―β(πβ(π β 1))) = π) |
54 | 53 | oveq2d 7366 |
. . . . 5
β’ ((π β§ π β (1...π) β§ π β (1...π)) β (0..^(β―β(πβ(π β 1)))) = (0..^π)) |
55 | 42, 54 | eleqtrrd 2842 |
. . . 4
β’ ((π β§ π β (1...π) β§ π β (1...π)) β (π β 1) β (0..^(β―β(πβ(π β 1))))) |
56 | | wrdsymbcl 14344 |
. . . 4
β’ (((πβ(π β 1)) β Word π β§ (π β 1) β (0..^(β―β(πβ(π β 1))))) β ((πβ(π β 1))β(π β 1)) β π) |
57 | 39, 55, 56 | syl2anc 585 |
. . 3
β’ ((π β§ π β (1...π) β§ π β (1...π)) β ((πβ(π β 1))β(π β 1)) β π) |
58 | 26, 27, 28, 29, 30, 57 | matbas2d 21700 |
. 2
β’ (π β (π β (1...π), π β (1...π) β¦ ((πβ(π β 1))β(π β 1))) β π) |
59 | 25, 58 | eqeltrd 2839 |
1
β’ (π β π β π) |