Step | Hyp | Ref
| Expression |
1 | | aacllem.0 |
. 2
β’ (π β π΄ β β) |
2 | | aacllem.1 |
. . . . . . 7
β’ (π β π β
β0) |
3 | 2 | nn0red 12479 |
. . . . . 6
β’ (π β π β β) |
4 | 3 | ltp1d 12090 |
. . . . 5
β’ (π β π < (π + 1)) |
5 | | peano2nn0 12458 |
. . . . . . . 8
β’ (π β β0
β (π + 1) β
β0) |
6 | 2, 5 | syl 17 |
. . . . . . 7
β’ (π β (π + 1) β
β0) |
7 | 6 | nn0red 12479 |
. . . . . 6
β’ (π β (π + 1) β β) |
8 | 3, 7 | ltnled 11307 |
. . . . 5
β’ (π β (π < (π + 1) β Β¬ (π + 1) β€ π)) |
9 | 4, 8 | mpbid 231 |
. . . 4
β’ (π β Β¬ (π + 1) β€ π) |
10 | | aacllem.3 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π) β§ π β (1...π)) β πΆ β β) |
11 | 10 | 3expa 1119 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π β (1...π)) β πΆ β β) |
12 | 11 | fmpttd 7064 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (π β (1...π) β¦ πΆ):(1...π)βΆβ) |
13 | | qex 12891 |
. . . . . . . . . . 11
β’ β
β V |
14 | | ovex 7391 |
. . . . . . . . . . 11
β’
(1...π) β
V |
15 | 13, 14 | elmap 8812 |
. . . . . . . . . 10
β’ ((π β (1...π) β¦ πΆ) β (β βm
(1...π)) β (π β (1...π) β¦ πΆ):(1...π)βΆβ) |
16 | 12, 15 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β (π β (1...π) β¦ πΆ) β (β βm
(1...π))) |
17 | 16 | fmpttd 7064 |
. . . . . . . 8
β’ (π β (π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)βΆ(β βm
(1...π))) |
18 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(βfld βΎs β) =
(βfld βΎs β) |
19 | 18 | qdrng 26984 |
. . . . . . . . . . 11
β’
(βfld βΎs β) β
DivRing |
20 | | drngring 20204 |
. . . . . . . . . . 11
β’
((βfld βΎs β) β DivRing
β (βfld βΎs β) β
Ring) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . 10
β’
(βfld βΎs β) β
Ring |
22 | | fzfi 13883 |
. . . . . . . . . 10
β’
(1...π) β
Fin |
23 | | eqid 2733 |
. . . . . . . . . . 11
β’
((βfld βΎs β) freeLMod (1...π)) = ((βfld
βΎs β) freeLMod (1...π)) |
24 | 23 | frlmlmod 21171 |
. . . . . . . . . 10
β’
(((βfld βΎs β) β Ring β§
(1...π) β Fin) β
((βfld βΎs β) freeLMod (1...π)) β LMod) |
25 | 21, 22, 24 | mp2an 691 |
. . . . . . . . 9
β’
((βfld βΎs β) freeLMod (1...π)) β LMod |
26 | | fzfi 13883 |
. . . . . . . . 9
β’
(0...π) β
Fin |
27 | 18 | qrngbas 26983 |
. . . . . . . . . . . 12
β’ β =
(Baseβ(βfld βΎs
β)) |
28 | 23, 27 | frlmfibas 21184 |
. . . . . . . . . . 11
β’
(((βfld βΎs β) β DivRing
β§ (1...π) β Fin)
β (β βm (1...π)) = (Baseβ((βfld
βΎs β) freeLMod (1...π)))) |
29 | 19, 22, 28 | mp2an 691 |
. . . . . . . . . 10
β’ (β
βm (1...π))
= (Baseβ((βfld βΎs β) freeLMod
(1...π))) |
30 | 23 | frlmsca 21175 |
. . . . . . . . . . 11
β’
(((βfld βΎs β) β DivRing
β§ (1...π) β Fin)
β (βfld βΎs β) =
(Scalarβ((βfld βΎs β) freeLMod
(1...π)))) |
31 | 19, 22, 30 | mp2an 691 |
. . . . . . . . . 10
β’
(βfld βΎs β) =
(Scalarβ((βfld βΎs β) freeLMod
(1...π))) |
32 | | eqid 2733 |
. . . . . . . . . 10
β’ (
Β·π β((βfld
βΎs β) freeLMod (1...π))) = ( Β·π
β((βfld βΎs β) freeLMod (1...π))) |
33 | 18 | qrng0 26985 |
. . . . . . . . . . . 12
β’ 0 =
(0gβ(βfld βΎs
β)) |
34 | 23, 33 | frlm0 21176 |
. . . . . . . . . . 11
β’
(((βfld βΎs β) β Ring β§
(1...π) β Fin) β
((1...π) Γ {0}) =
(0gβ((βfld βΎs β)
freeLMod (1...π)))) |
35 | 21, 22, 34 | mp2an 691 |
. . . . . . . . . 10
β’
((1...π) Γ
{0}) = (0gβ((βfld βΎs
β) freeLMod (1...π))) |
36 | | eqid 2733 |
. . . . . . . . . . . 12
β’
((βfld βΎs β) freeLMod (0...π)) = ((βfld
βΎs β) freeLMod (0...π)) |
37 | 36, 27 | frlmfibas 21184 |
. . . . . . . . . . 11
β’
(((βfld βΎs β) β DivRing
β§ (0...π) β Fin)
β (β βm (0...π)) = (Baseβ((βfld
βΎs β) freeLMod (0...π)))) |
38 | 19, 26, 37 | mp2an 691 |
. . . . . . . . . 10
β’ (β
βm (0...π))
= (Baseβ((βfld βΎs β) freeLMod
(0...π))) |
39 | 29, 31, 32, 35, 33, 38 | islindf4 21260 |
. . . . . . . . 9
β’
((((βfld βΎs β) freeLMod
(1...π)) β LMod β§
(0...π) β Fin β§
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)βΆ(β βm
(1...π))) β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)) LIndF ((βfld
βΎs β) freeLMod (1...π)) β βπ€ β (β βm
(0...π))((((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = ((1...π) Γ {0}) β π€ = ((0...π) Γ {0})))) |
40 | 25, 26, 39 | mp3an12 1452 |
. . . . . . . 8
β’ ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)βΆ(β βm
(1...π)) β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)) LIndF ((βfld
βΎs β) freeLMod (1...π)) β βπ€ β (β βm
(0...π))((((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = ((1...π) Γ {0}) β π€ = ((0...π) Γ {0})))) |
41 | 17, 40 | syl 17 |
. . . . . . 7
β’ (π β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)) LIndF ((βfld
βΎs β) freeLMod (1...π)) β βπ€ β (β βm
(0...π))((((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = ((1...π) Γ {0}) β π€ = ((0...π) Γ {0})))) |
42 | | elmapi 8790 |
. . . . . . . . 9
β’ (π€ β (β
βm (0...π))
β π€:(0...π)βΆβ) |
43 | | fzfid 13884 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€:(0...π)βΆβ) β (0...π) β Fin) |
44 | | fvexd 6858 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (π€βπ) β V) |
45 | 14 | mptex 7174 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β¦ πΆ) β V |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (π β (1...π) β¦ πΆ) β V) |
47 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π€:(0...π)βΆβ) β π€:(0...π)βΆβ) |
48 | 47 | feqmptd 6911 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€:(0...π)βΆβ) β π€ = (π β (0...π) β¦ (π€βπ))) |
49 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€:(0...π)βΆβ) β (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) = (π β (0...π) β¦ (π β (1...π) β¦ πΆ))) |
50 | 43, 44, 46, 48, 49 | offval2 7638 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€:(0...π)βΆβ) β (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ))) = (π β (0...π) β¦ ((π€βπ)( Β·π
β((βfld βΎs β) freeLMod (1...π)))(π β (1...π) β¦ πΆ)))) |
51 | | fzfid 13884 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (1...π) β Fin) |
52 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π€:(0...π)βΆβ β§ π β (0...π)) β (π€βπ) β β) |
53 | 52 | adantll 713 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (π€βπ) β β) |
54 | 16 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (π β (1...π) β¦ πΆ) β (β βm
(1...π))) |
55 | | cnfldmul 20818 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ Β·
= (.rββfld) |
56 | 18, 55 | ressmulr 17193 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β
β V β Β· = (.rβ(βfld
βΎs β))) |
57 | 13, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ Β·
= (.rβ(βfld βΎs
β)) |
58 | 23, 29, 27, 51, 53, 54, 32, 57 | frlmvscafval 21188 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β ((π€βπ)( Β·π
β((βfld βΎs β) freeLMod (1...π)))(π β (1...π) β¦ πΆ)) = (((1...π) Γ {(π€βπ)}) βf Β· (π β (1...π) β¦ πΆ))) |
59 | | fvexd 6858 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β§ π β (1...π)) β (π€βπ) β V) |
60 | 11 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β§ π β (1...π)) β πΆ β β) |
61 | | fconstmpt 5695 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((1...π) Γ
{(π€βπ)}) = (π β (1...π) β¦ (π€βπ)) |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β ((1...π) Γ {(π€βπ)}) = (π β (1...π) β¦ (π€βπ))) |
63 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (π β (1...π) β¦ πΆ) = (π β (1...π) β¦ πΆ)) |
64 | 51, 59, 60, 62, 63 | offval2 7638 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (((1...π) Γ {(π€βπ)}) βf Β· (π β (1...π) β¦ πΆ)) = (π β (1...π) β¦ ((π€βπ) Β· πΆ))) |
65 | 58, 64 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β ((π€βπ)( Β·π
β((βfld βΎs β) freeLMod (1...π)))(π β (1...π) β¦ πΆ)) = (π β (1...π) β¦ ((π€βπ) Β· πΆ))) |
66 | 65 | mpteq2dva 5206 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€:(0...π)βΆβ) β (π β (0...π) β¦ ((π€βπ)( Β·π
β((βfld βΎs β) freeLMod (1...π)))(π β (1...π) β¦ πΆ))) = (π β (0...π) β¦ (π β (1...π) β¦ ((π€βπ) Β· πΆ)))) |
67 | 50, 66 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€:(0...π)βΆβ) β (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ))) = (π β (0...π) β¦ (π β (1...π) β¦ ((π€βπ) Β· πΆ)))) |
68 | 67 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π€:(0...π)βΆβ) β
(((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = (((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π β (0...π) β¦ (π β (1...π) β¦ ((π€βπ) Β· πΆ))))) |
69 | | fzfid 13884 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€:(0...π)βΆβ) β (1...π) β Fin) |
70 | 21 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€:(0...π)βΆβ) β
(βfld βΎs β) β
Ring) |
71 | 53 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β§ π β (0...π)) β (π€βπ) β β) |
72 | 11 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (1...π)) β§ π β (0...π)) β πΆ β β) |
73 | 72 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β§ π β (0...π)) β πΆ β β) |
74 | | qmulcl 12897 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π€βπ) β β β§ πΆ β β) β ((π€βπ) Β· πΆ) β β) |
75 | 71, 73, 74 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β§ π β (0...π)) β ((π€βπ) Β· πΆ) β β) |
76 | 75 | an32s 651 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β§ π β (1...π)) β ((π€βπ) Β· πΆ) β β) |
77 | 76 | fmpttd 7064 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (π β (1...π) β¦ ((π€βπ) Β· πΆ)):(1...π)βΆβ) |
78 | 13, 14 | elmap 8812 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (1...π) β¦ ((π€βπ) Β· πΆ)) β (β βm
(1...π)) β (π β (1...π) β¦ ((π€βπ) Β· πΆ)):(1...π)βΆβ) |
79 | 77, 78 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (π β (1...π) β¦ ((π€βπ) Β· πΆ)) β (β βm
(1...π))) |
80 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π) β¦ (π β (1...π) β¦ ((π€βπ) Β· πΆ))) = (π β (0...π) β¦ (π β (1...π) β¦ ((π€βπ) Β· πΆ))) |
81 | 14 | mptex 7174 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β¦ ((π€βπ) Β· πΆ)) β V |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (π β (1...π) β¦ ((π€βπ) Β· πΆ)) β V) |
83 | | snex 5389 |
. . . . . . . . . . . . . . . . . . 19
β’ {0}
β V |
84 | 14, 83 | xpex 7688 |
. . . . . . . . . . . . . . . . . 18
β’
((1...π) Γ
{0}) β V |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€:(0...π)βΆβ) β ((1...π) Γ {0}) β
V) |
86 | 80, 43, 82, 85 | fsuppmptdm 9321 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€:(0...π)βΆβ) β (π β (0...π) β¦ (π β (1...π) β¦ ((π€βπ) Β· πΆ))) finSupp ((1...π) Γ {0})) |
87 | 23, 29, 35, 69, 43, 70, 79, 86 | frlmgsum 21194 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π€:(0...π)βΆβ) β
(((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π β (0...π) β¦ (π β (1...π) β¦ ((π€βπ) Β· πΆ)))) = (π β (1...π) β¦ ((βfld
βΎs β) Ξ£g (π β (0...π) β¦ ((π€βπ) Β· πΆ))))) |
88 | | cnfldbas 20816 |
. . . . . . . . . . . . . . . . . 18
β’ β =
(Baseββfld) |
89 | | cnfldadd 20817 |
. . . . . . . . . . . . . . . . . 18
β’ + =
(+gββfld) |
90 | | cnfldex 20815 |
. . . . . . . . . . . . . . . . . . 19
β’
βfld β V |
91 | 90 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β βfld β
V) |
92 | | fzfid 13884 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β (0...π) β Fin) |
93 | | qsscn 12890 |
. . . . . . . . . . . . . . . . . . 19
β’ β
β β |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β β β
β) |
95 | 75 | fmpttd 7064 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β (π β (0...π) β¦ ((π€βπ) Β· πΆ)):(0...π)βΆβ) |
96 | | 0z 12515 |
. . . . . . . . . . . . . . . . . . . 20
β’ 0 β
β€ |
97 | | zq 12884 |
. . . . . . . . . . . . . . . . . . . 20
β’ (0 β
β€ β 0 β β) |
98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 β
β |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β 0 β β) |
100 | | addid2 11343 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β (0 +
π₯) = π₯) |
101 | | addid1 11340 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β (π₯ + 0) = π₯) |
102 | 100, 101 | jca 513 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β ((0 +
π₯) = π₯ β§ (π₯ + 0) = π₯)) |
103 | 102 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β§ π₯ β β) β ((0 + π₯) = π₯ β§ (π₯ + 0) = π₯)) |
104 | 88, 89, 18, 91, 92, 94, 95, 99, 103 | gsumress 18542 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β (βfld
Ξ£g (π β (0...π) β¦ ((π€βπ) Β· πΆ))) = ((βfld
βΎs β) Ξ£g (π β (0...π) β¦ ((π€βπ) Β· πΆ)))) |
105 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β π€:(0...π)βΆβ) |
106 | | qcn 12893 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π€βπ) β β β (π€βπ) β β) |
107 | 52, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π€:(0...π)βΆβ β§ π β (0...π)) β (π€βπ) β β) |
108 | 105, 107 | sylan 581 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β§ π β (0...π)) β (π€βπ) β β) |
109 | | qcn 12893 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΆ β β β πΆ β
β) |
110 | 11, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0...π)) β§ π β (1...π)) β πΆ β β) |
111 | 110 | an32s 651 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (1...π)) β§ π β (0...π)) β πΆ β β) |
112 | 111 | adantllr 718 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β§ π β (0...π)) β πΆ β β) |
113 | 108, 112 | mulcld 11180 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β§ π β (0...π)) β ((π€βπ) Β· πΆ) β β) |
114 | 92, 113 | gsumfsum 20880 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β (βfld
Ξ£g (π β (0...π) β¦ ((π€βπ) Β· πΆ))) = Ξ£π β (0...π)((π€βπ) Β· πΆ)) |
115 | 104, 114 | eqtr3d 2775 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β ((βfld
βΎs β) Ξ£g (π β (0...π) β¦ ((π€βπ) Β· πΆ))) = Ξ£π β (0...π)((π€βπ) Β· πΆ)) |
116 | 115 | mpteq2dva 5206 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π€:(0...π)βΆβ) β (π β (1...π) β¦ ((βfld
βΎs β) Ξ£g (π β (0...π) β¦ ((π€βπ) Β· πΆ)))) = (π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ))) |
117 | 68, 87, 116 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€:(0...π)βΆβ) β
(((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = (π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ))) |
118 | | qaddcl 12895 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
119 | 118 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β§ (π₯ β β β§ π¦ β β)) β (π₯ + π¦) β β) |
120 | 94, 119, 92, 75, 99 | fsumcllem 15622 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β Ξ£π β (0...π)((π€βπ) Β· πΆ) β β) |
121 | 120 | fmpttd 7064 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π€:(0...π)βΆβ) β (π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ)):(1...π)βΆβ) |
122 | 13, 14 | elmap 8812 |
. . . . . . . . . . . . . . 15
β’ ((π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ)) β (β βm
(1...π)) β (π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ)):(1...π)βΆβ) |
123 | 121, 122 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€:(0...π)βΆβ) β (π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ)) β (β βm
(1...π))) |
124 | 117, 123 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ ((π β§ π€:(0...π)βΆβ) β
(((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) β (β βm
(1...π))) |
125 | | elmapi 8790 |
. . . . . . . . . . . . 13
β’
((((βfld βΎs β) freeLMod
(1...π))
Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) β (β βm
(1...π)) β
(((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))):(1...π)βΆβ) |
126 | | ffn 6669 |
. . . . . . . . . . . . 13
β’
((((βfld βΎs β) freeLMod
(1...π))
Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))):(1...π)βΆβ β
(((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) Fn (1...π)) |
127 | 124, 125,
126 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ π€:(0...π)βΆβ) β
(((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) Fn (1...π)) |
128 | | c0ex 11154 |
. . . . . . . . . . . . 13
β’ 0 β
V |
129 | | fnconstg 6731 |
. . . . . . . . . . . . 13
β’ (0 β
V β ((1...π) Γ
{0}) Fn (1...π)) |
130 | 128, 129 | ax-mp 5 |
. . . . . . . . . . . 12
β’
((1...π) Γ
{0}) Fn (1...π) |
131 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π((βfld βΎs
β) freeLMod (1...π)) |
132 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π
Ξ£g |
133 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²ππ€ |
134 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²π
βf ( Β·π
β((βfld βΎs β) freeLMod (1...π))) |
135 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
β’
β²π(0...π) |
136 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . 16
β’
β²π(π β (1...π) β¦ πΆ) |
137 | 135, 136 | nfmpt 5213 |
. . . . . . . . . . . . . . 15
β’
β²π(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) |
138 | 133, 134,
137 | nfov 7388 |
. . . . . . . . . . . . . 14
β’
β²π(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ))) |
139 | 131, 132,
138 | nfov 7388 |
. . . . . . . . . . . . 13
β’
β²π(((βfld βΎs
β) freeLMod (1...π))
Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) |
140 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π((1...π) Γ {0}) |
141 | 139, 140 | eqfnfv2f 6987 |
. . . . . . . . . . . 12
β’
(((((βfld βΎs β) freeLMod
(1...π))
Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) Fn (1...π) β§ ((1...π) Γ {0}) Fn (1...π)) β ((((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = ((1...π) Γ {0}) β βπ β (1...π)((((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ))))βπ) = (((1...π) Γ {0})βπ))) |
142 | 127, 130,
141 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β§ π€:(0...π)βΆβ) β
((((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = ((1...π) Γ {0}) β βπ β (1...π)((((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ))))βπ) = (((1...π) Γ {0})βπ))) |
143 | 117 | fveq1d 6845 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€:(0...π)βΆβ) β
((((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ))))βπ) = ((π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ))βπ)) |
144 | | sumex 15578 |
. . . . . . . . . . . . . . 15
β’
Ξ£π β
(0...π)((π€βπ) Β· πΆ) β V |
145 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ)) = (π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ)) |
146 | 145 | fvmpt2 6960 |
. . . . . . . . . . . . . . 15
β’ ((π β (1...π) β§ Ξ£π β (0...π)((π€βπ) Β· πΆ) β V) β ((π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ))βπ) = Ξ£π β (0...π)((π€βπ) Β· πΆ)) |
147 | 144, 146 | mpan2 690 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β ((π β (1...π) β¦ Ξ£π β (0...π)((π€βπ) Β· πΆ))βπ) = Ξ£π β (0...π)((π€βπ) Β· πΆ)) |
148 | 143, 147 | sylan9eq 2793 |
. . . . . . . . . . . . 13
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β ((((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ))))βπ) = Ξ£π β (0...π)((π€βπ) Β· πΆ)) |
149 | 128 | fvconst2 7154 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β (((1...π) Γ {0})βπ) = 0) |
150 | 149 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β (((1...π) Γ {0})βπ) = 0) |
151 | 148, 150 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β (((((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ))))βπ) = (((1...π) Γ {0})βπ) β Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) |
152 | 151 | ralbidva 3169 |
. . . . . . . . . . 11
β’ ((π β§ π€:(0...π)βΆβ) β (βπ β (1...π)((((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ))))βπ) = (((1...π) Γ {0})βπ) β βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) |
153 | 142, 152 | bitrd 279 |
. . . . . . . . . 10
β’ ((π β§ π€:(0...π)βΆβ) β
((((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = ((1...π) Γ {0}) β βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) |
154 | 153 | imbi1d 342 |
. . . . . . . . 9
β’ ((π β§ π€:(0...π)βΆβ) β
(((((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = ((1...π) Γ {0}) β π€ = ((0...π) Γ {0})) β (βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β π€ = ((0...π) Γ {0})))) |
155 | 42, 154 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π€ β (β βm
(0...π))) β
(((((βfld βΎs β) freeLMod (1...π)) Ξ£g
(π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = ((1...π) Γ {0}) β π€ = ((0...π) Γ {0})) β (βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β π€ = ((0...π) Γ {0})))) |
156 | 155 | ralbidva 3169 |
. . . . . . 7
β’ (π β (βπ€ β (β
βm (0...π))((((βfld
βΎs β) freeLMod (1...π)) Ξ£g (π€ βf (
Β·π β((βfld
βΎs β) freeLMod (1...π)))(π β (0...π) β¦ (π β (1...π) β¦ πΆ)))) = ((1...π) Γ {0}) β π€ = ((0...π) Γ {0})) β βπ€ β (β
βm (0...π))(βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β π€ = ((0...π) Γ {0})))) |
157 | 41, 156 | bitrd 279 |
. . . . . 6
β’ (π β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)) LIndF ((βfld
βΎs β) freeLMod (1...π)) β βπ€ β (β βm
(0...π))(βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β π€ = ((0...π) Γ {0})))) |
158 | | drngnzr 20748 |
. . . . . . . . 9
β’
((βfld βΎs β) β DivRing
β (βfld βΎs β) β
NzRing) |
159 | 19, 158 | ax-mp 5 |
. . . . . . . 8
β’
(βfld βΎs β) β
NzRing |
160 | 31 | islindf3 21248 |
. . . . . . . 8
β’
((((βfld βΎs β) freeLMod
(1...π)) β LMod β§
(βfld βΎs β) β NzRing) β
((π β (0...π) β¦ (π β (1...π) β¦ πΆ)) LIndF ((βfld
βΎs β) freeLMod (1...π)) β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):dom (π β (0...π) β¦ (π β (1...π) β¦ πΆ))β1-1βV β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))))) |
161 | 25, 159, 160 | mp2an 691 |
. . . . . . 7
β’ ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)) LIndF ((βfld
βΎs β) freeLMod (1...π)) β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):dom (π β (0...π) β¦ (π β (1...π) β¦ πΆ))β1-1βV β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π))))) |
162 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) = (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) |
163 | 45, 162 | dmmpti 6646 |
. . . . . . . . 9
β’ dom
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) = (0...π) |
164 | | f1eq2 6735 |
. . . . . . . . 9
β’ (dom
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) = (0...π) β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):dom (π β (0...π) β¦ (π β (1...π) β¦ πΆ))β1-1βV β (π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV)) |
165 | 163, 164 | ax-mp 5 |
. . . . . . . 8
β’ ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):dom (π β (0...π) β¦ (π β (1...π) β¦ πΆ))β1-1βV β (π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV) |
166 | 165 | anbi1i 625 |
. . . . . . 7
β’ (((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):dom (π β (0...π) β¦ (π β (1...π) β¦ πΆ))β1-1βV β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π))))) |
167 | 161, 166 | bitri 275 |
. . . . . 6
β’ ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)) LIndF ((βfld
βΎs β) freeLMod (1...π)) β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π))))) |
168 | | con34b 316 |
. . . . . . . . 9
β’
((βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β π€ = ((0...π) Γ {0})) β (Β¬ π€ = ((0...π) Γ {0}) β Β¬ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) |
169 | | df-nel 3047 |
. . . . . . . . . . 11
β’ (π€ β {((0...π) Γ {0})} β Β¬
π€ β {((0...π) Γ
{0})}) |
170 | | velsn 4603 |
. . . . . . . . . . 11
β’ (π€ β {((0...π) Γ {0})} β π€ = ((0...π) Γ {0})) |
171 | 169, 170 | xchbinx 334 |
. . . . . . . . . 10
β’ (π€ β {((0...π) Γ {0})} β Β¬
π€ = ((0...π) Γ {0})) |
172 | 171 | imbi1i 350 |
. . . . . . . . 9
β’ ((π€ β {((0...π) Γ {0})} β Β¬
βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0) β (Β¬ π€ = ((0...π) Γ {0}) β Β¬ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) |
173 | 168, 172 | bitr4i 278 |
. . . . . . . 8
β’
((βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β π€ = ((0...π) Γ {0})) β (π€ β {((0...π) Γ {0})} β Β¬ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) |
174 | 173 | ralbii 3093 |
. . . . . . 7
β’
(βπ€ β
(β βm (0...π))(βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β π€ = ((0...π) Γ {0})) β βπ€ β (β
βm (0...π))(π€ β {((0...π) Γ {0})} β Β¬ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) |
175 | | raldifb 4105 |
. . . . . . 7
β’
(βπ€ β
(β βm (0...π))(π€ β {((0...π) Γ {0})} β Β¬ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0) β βπ€ β ((β βm
(0...π)) β
{((0...π) Γ {0})})
Β¬ βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0) |
176 | | ralnex 3072 |
. . . . . . 7
β’
(βπ€ β
((β βm (0...π)) β {((0...π) Γ {0})}) Β¬ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β Β¬ βπ€ β ((β βm
(0...π)) β
{((0...π) Γ
{0})})βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0) |
177 | 174, 175,
176 | 3bitri 297 |
. . . . . 6
β’
(βπ€ β
(β βm (0...π))(βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β π€ = ((0...π) Γ {0})) β Β¬ βπ€ β ((β
βm (0...π))
β {((0...π) Γ
{0})})βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0) |
178 | 157, 167,
177 | 3bitr3g 313 |
. . . . 5
β’ (π β (((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β Β¬
βπ€ β ((β
βm (0...π))
β {((0...π) Γ
{0})})βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) |
179 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(LSubSpβ((βfld βΎs β)
freeLMod (1...π))) =
(LSubSpβ((βfld βΎs β) freeLMod
(1...π))) |
180 | 29, 179 | lssmre 20442 |
. . . . . . . . . . . 12
β’
(((βfld βΎs β) freeLMod
(1...π)) β LMod β
(LSubSpβ((βfld βΎs β) freeLMod
(1...π))) β
(Mooreβ(β βm (1...π)))) |
181 | 25, 180 | ax-mp 5 |
. . . . . . . . . . 11
β’
(LSubSpβ((βfld βΎs β)
freeLMod (1...π))) β
(Mooreβ(β βm (1...π))) |
182 | 181 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β
(LSubSpβ((βfld βΎs β) freeLMod
(1...π))) β
(Mooreβ(β βm (1...π)))) |
183 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(LSpanβ((βfld βΎs β)
freeLMod (1...π))) =
(LSpanβ((βfld βΎs β) freeLMod
(1...π))) |
184 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(mrClsβ(LSubSpβ((βfld βΎs
β) freeLMod (1...π)))) =
(mrClsβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π)))) |
185 | 179, 183,
184 | mrclsp 20465 |
. . . . . . . . . . 11
β’
(((βfld βΎs β) freeLMod
(1...π)) β LMod β
(LSpanβ((βfld βΎs β) freeLMod
(1...π))) =
(mrClsβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π))))) |
186 | 25, 185 | ax-mp 5 |
. . . . . . . . . 10
β’
(LSpanβ((βfld βΎs β)
freeLMod (1...π))) =
(mrClsβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π)))) |
187 | | eqid 2733 |
. . . . . . . . . 10
β’
(mrIndβ(LSubSpβ((βfld βΎs
β) freeLMod (1...π)))) =
(mrIndβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π)))) |
188 | 31 | islvec 20580 |
. . . . . . . . . . . . 13
β’
(((βfld βΎs β) freeLMod
(1...π)) β LVec β
(((βfld βΎs β) freeLMod (1...π)) β LMod β§
(βfld βΎs β) β
DivRing)) |
189 | 25, 19, 188 | mpbir2an 710 |
. . . . . . . . . . . 12
β’
((βfld βΎs β) freeLMod (1...π)) β LVec |
190 | 179, 186,
29 | lssacsex 20621 |
. . . . . . . . . . . . 13
β’
(((βfld βΎs β) freeLMod
(1...π)) β LVec β
((LSubSpβ((βfld βΎs β) freeLMod
(1...π))) β
(ACSβ(β βm (1...π))) β§ βπ§ β π« (β βm
(1...π))βπ₯ β (β
βm (1...π))βπ¦ β
(((LSpanβ((βfld βΎs β) freeLMod
(1...π)))β(π§ βͺ {π₯})) β
((LSpanβ((βfld βΎs β) freeLMod
(1...π)))βπ§))π₯ β ((LSpanβ((βfld
βΎs β) freeLMod (1...π)))β(π§ βͺ {π¦})))) |
191 | 190 | simprd 497 |
. . . . . . . . . . . 12
β’
(((βfld βΎs β) freeLMod
(1...π)) β LVec β
βπ§ β π«
(β βm (1...π))βπ₯ β (β βm
(1...π))βπ¦ β
(((LSpanβ((βfld βΎs β) freeLMod
(1...π)))β(π§ βͺ {π₯})) β
((LSpanβ((βfld βΎs β) freeLMod
(1...π)))βπ§))π₯ β ((LSpanβ((βfld
βΎs β) freeLMod (1...π)))β(π§ βͺ {π¦}))) |
192 | 189, 191 | ax-mp 5 |
. . . . . . . . . . 11
β’
βπ§ β
π« (β βm (1...π))βπ₯ β (β βm
(1...π))βπ¦ β
(((LSpanβ((βfld βΎs β) freeLMod
(1...π)))β(π§ βͺ {π₯})) β
((LSpanβ((βfld βΎs β) freeLMod
(1...π)))βπ§))π₯ β ((LSpanβ((βfld
βΎs β) freeLMod (1...π)))β(π§ βͺ {π¦})) |
193 | 192 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β
βπ§ β π«
(β βm (1...π))βπ₯ β (β βm
(1...π))βπ¦ β
(((LSpanβ((βfld βΎs β) freeLMod
(1...π)))β(π§ βͺ {π₯})) β
((LSpanβ((βfld βΎs β) freeLMod
(1...π)))βπ§))π₯ β ((LSpanβ((βfld
βΎs β) freeLMod (1...π)))β(π§ βͺ {π¦}))) |
194 | 17 | frnd 6677 |
. . . . . . . . . . . 12
β’ (π β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β (β βm
(1...π))) |
195 | | dif0 4333 |
. . . . . . . . . . . 12
β’ ((β
βm (1...π))
β β
) = (β βm (1...π)) |
196 | 194, 195 | sseqtrrdi 3996 |
. . . . . . . . . . 11
β’ (π β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β ((β βm
(1...π)) β
β
)) |
197 | 196 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β ((β βm
(1...π)) β
β
)) |
198 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
((βfld βΎs β) unitVec (1...π)) = ((βfld
βΎs β) unitVec (1...π)) |
199 | 198, 23, 29 | uvcff 21213 |
. . . . . . . . . . . . . 14
β’
(((βfld βΎs β) β Ring β§
(1...π) β Fin) β
((βfld βΎs β) unitVec (1...π)):(1...π)βΆ(β βm
(1...π))) |
200 | 21, 22, 199 | mp2an 691 |
. . . . . . . . . . . . 13
β’
((βfld βΎs β) unitVec (1...π)):(1...π)βΆ(β βm
(1...π)) |
201 | | frn 6676 |
. . . . . . . . . . . . 13
β’
(((βfld βΎs β) unitVec (1...π)):(1...π)βΆ(β βm
(1...π)) β ran
((βfld βΎs β) unitVec (1...π)) β (β
βm (1...π))) |
202 | 200, 201 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ran
((βfld βΎs β) unitVec (1...π)) β (β
βm (1...π)) |
203 | 202, 195 | sseqtrri 3982 |
. . . . . . . . . . 11
β’ ran
((βfld βΎs β) unitVec (1...π)) β ((β
βm (1...π))
β β
) |
204 | 203 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β ran
((βfld βΎs β) unitVec (1...π)) β ((β
βm (1...π))
β β
)) |
205 | | un0 4351 |
. . . . . . . . . . . . . 14
β’ (ran
((βfld βΎs β) unitVec (1...π)) βͺ β
) = ran
((βfld βΎs β) unitVec (1...π)) |
206 | 205 | fveq2i 6846 |
. . . . . . . . . . . . 13
β’
((LSpanβ((βfld βΎs β)
freeLMod (1...π)))β(ran ((βfld
βΎs β) unitVec (1...π)) βͺ β
)) =
((LSpanβ((βfld βΎs β) freeLMod
(1...π)))βran
((βfld βΎs β) unitVec (1...π))) |
207 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(LBasisβ((βfld βΎs β)
freeLMod (1...π))) =
(LBasisβ((βfld βΎs β) freeLMod
(1...π))) |
208 | 23, 198, 207 | frlmlbs 21219 |
. . . . . . . . . . . . . . 15
β’
(((βfld βΎs β) β Ring β§
(1...π) β Fin) β
ran ((βfld βΎs β) unitVec (1...π)) β
(LBasisβ((βfld βΎs β) freeLMod
(1...π)))) |
209 | 21, 22, 208 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ ran
((βfld βΎs β) unitVec (1...π)) β
(LBasisβ((βfld βΎs β) freeLMod
(1...π))) |
210 | 29, 207, 183 | lbssp 20555 |
. . . . . . . . . . . . . 14
β’ (ran
((βfld βΎs β) unitVec (1...π)) β
(LBasisβ((βfld βΎs β) freeLMod
(1...π))) β
((LSpanβ((βfld βΎs β) freeLMod
(1...π)))βran
((βfld βΎs β) unitVec (1...π))) = (β
βm (1...π))) |
211 | 209, 210 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
((LSpanβ((βfld βΎs β)
freeLMod (1...π)))βran ((βfld
βΎs β) unitVec (1...π))) = (β βm (1...π)) |
212 | 206, 211 | eqtri 2761 |
. . . . . . . . . . . 12
β’
((LSpanβ((βfld βΎs β)
freeLMod (1...π)))β(ran ((βfld
βΎs β) unitVec (1...π)) βͺ β
)) = (β
βm (1...π)) |
213 | 194, 212 | sseqtrrdi 3996 |
. . . . . . . . . . 11
β’ (π β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
((LSpanβ((βfld βΎs β) freeLMod
(1...π)))β(ran
((βfld βΎs β) unitVec (1...π)) βͺ
β
))) |
214 | 213 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
((LSpanβ((βfld βΎs β) freeLMod
(1...π)))β(ran
((βfld βΎs β) unitVec (1...π)) βͺ
β
))) |
215 | | un0 4351 |
. . . . . . . . . . 11
β’ (ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) βͺ β
) = ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) |
216 | 25, 159 | pm3.2i 472 |
. . . . . . . . . . . . . 14
β’
(((βfld βΎs β) freeLMod
(1...π)) β LMod β§
(βfld βΎs β) β
NzRing) |
217 | 183, 31 | lindsind2 21241 |
. . . . . . . . . . . . . 14
β’
(((((βfld βΎs β) freeLMod
(1...π)) β LMod β§
(βfld βΎs β) β NzRing) β§ ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π))) β§ π₯ β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ))) β Β¬ π₯ β ((LSpanβ((βfld
βΎs β) freeLMod (1...π)))β(ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β {π₯}))) |
218 | 216, 217 | mp3an1 1449 |
. . . . . . . . . . . . 13
β’ ((ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π))) β§ π₯ β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ))) β Β¬ π₯ β ((LSpanβ((βfld
βΎs β) freeLMod (1...π)))β(ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β {π₯}))) |
219 | 218 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π))) β
βπ₯ β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) Β¬ π₯ β ((LSpanβ((βfld
βΎs β) freeLMod (1...π)))β(ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β {π₯}))) |
220 | 186, 187 | ismri2 17517 |
. . . . . . . . . . . . . 14
β’
(((LSubSpβ((βfld βΎs β)
freeLMod (1...π))) β
(Mooreβ(β βm (1...π))) β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β (β βm
(1...π))) β (ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(mrIndβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π)))) β
βπ₯ β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) Β¬ π₯ β ((LSpanβ((βfld
βΎs β) freeLMod (1...π)))β(ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β {π₯})))) |
221 | 181, 194,
220 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π β (ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(mrIndβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π)))) β
βπ₯ β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) Β¬ π₯ β ((LSpanβ((βfld
βΎs β) freeLMod (1...π)))β(ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β {π₯})))) |
222 | 221 | biimpar 479 |
. . . . . . . . . . . 12
β’ ((π β§ βπ₯ β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) Β¬ π₯ β ((LSpanβ((βfld
βΎs β) freeLMod (1...π)))β(ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β {π₯}))) β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(mrIndβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π))))) |
223 | 219, 222 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(mrIndβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π))))) |
224 | 215, 223 | eqeltrid 2838 |
. . . . . . . . . 10
β’ ((π β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β (ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) βͺ β
) β
(mrIndβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π))))) |
225 | | mptfi 9298 |
. . . . . . . . . . . . 13
β’
((0...π) β Fin
β (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β Fin) |
226 | | rnfi 9282 |
. . . . . . . . . . . . 13
β’ ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β Fin β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β Fin) |
227 | 26, 225, 226 | mp2b 10 |
. . . . . . . . . . . 12
β’ ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β Fin |
228 | 227 | orci 864 |
. . . . . . . . . . 11
β’ (ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β Fin β¨ ran
((βfld βΎs β) unitVec (1...π)) β Fin) |
229 | 228 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β (ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β Fin β¨ ran
((βfld βΎs β) unitVec (1...π)) β Fin)) |
230 | 182, 186,
187, 193, 197, 204, 214, 224, 229 | mreexexd 17533 |
. . . . . . . . 9
β’ ((π β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β
βπ£ β π«
ran ((βfld βΎs β) unitVec (1...π))(ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β π£ β§ (π£ βͺ β
) β
(mrIndβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π)))))) |
231 | 230 | ex 414 |
. . . . . . . 8
β’ (π β (ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π))) β
βπ£ β π«
ran ((βfld βΎs β) unitVec (1...π))(ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β π£ β§ (π£ βͺ β
) β
(mrIndβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π))))))) |
232 | | ovex 7391 |
. . . . . . . . . . . . 13
β’
((βfld βΎs β) unitVec (1...π)) β V |
233 | 232 | rnex 7850 |
. . . . . . . . . . . 12
β’ ran
((βfld βΎs β) unitVec (1...π)) β V |
234 | | elpwi 4568 |
. . . . . . . . . . . 12
β’ (π£ β π« ran
((βfld βΎs β) unitVec (1...π)) β π£ β ran ((βfld
βΎs β) unitVec (1...π))) |
235 | | ssdomg 8943 |
. . . . . . . . . . . 12
β’ (ran
((βfld βΎs β) unitVec (1...π)) β V β (π£ β ran
((βfld βΎs β) unitVec (1...π)) β π£ βΌ ran ((βfld
βΎs β) unitVec (1...π)))) |
236 | 233, 234,
235 | mpsyl 68 |
. . . . . . . . . . 11
β’ (π£ β π« ran
((βfld βΎs β) unitVec (1...π)) β π£ βΌ ran ((βfld
βΎs β) unitVec (1...π))) |
237 | | endomtr 8955 |
. . . . . . . . . . . . . 14
β’ ((ran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β π£ β§ π£ βΌ ran ((βfld
βΎs β) unitVec (1...π))) β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) βΌ ran ((βfld
βΎs β) unitVec (1...π))) |
238 | 237 | ancoms 460 |
. . . . . . . . . . . . 13
β’ ((π£ βΌ ran
((βfld βΎs β) unitVec (1...π)) β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β π£) β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) βΌ ran ((βfld
βΎs β) unitVec (1...π))) |
239 | | f1f1orn 6796 |
. . . . . . . . . . . . . . . 16
β’ ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β (π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1-ontoβran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ))) |
240 | | ovex 7391 |
. . . . . . . . . . . . . . . . 17
β’
(0...π) β
V |
241 | 240 | f1oen 8916 |
. . . . . . . . . . . . . . . 16
β’ ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1-ontoβran
(π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β (0...π) β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ))) |
242 | 239, 241 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β (0...π) β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ))) |
243 | | endomtr 8955 |
. . . . . . . . . . . . . . . . 17
β’
(((0...π) β
ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) βΌ ran ((βfld
βΎs β) unitVec (1...π))) β (0...π) βΌ ran ((βfld
βΎs β) unitVec (1...π))) |
244 | 198 | uvcendim 21269 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((βfld βΎs β) β NzRing
β§ (1...π) β Fin)
β (1...π) β ran
((βfld βΎs β) unitVec (1...π))) |
245 | 159, 22, 244 | mp2an 691 |
. . . . . . . . . . . . . . . . . . 19
β’
(1...π) β ran
((βfld βΎs β) unitVec (1...π)) |
246 | 245 | ensymi 8947 |
. . . . . . . . . . . . . . . . . 18
β’ ran
((βfld βΎs β) unitVec (1...π)) β (1...π) |
247 | | domentr 8956 |
. . . . . . . . . . . . . . . . . . 19
β’
(((0...π) βΌ
ran ((βfld βΎs β) unitVec (1...π)) β§ ran
((βfld βΎs β) unitVec (1...π)) β (1...π)) β (0...π) βΌ (1...π)) |
248 | | hashdom 14285 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((0...π) β Fin
β§ (1...π) β Fin)
β ((β―β(0...π)) β€ (β―β(1...π)) β (0...π) βΌ (1...π))) |
249 | 26, 22, 248 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―β(0...π)) β€ (β―β(1...π)) β (0...π) βΌ (1...π)) |
250 | | hashfz0 14338 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β (β―β(0...π)) = (π + 1)) |
251 | 2, 250 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (β―β(0...π)) = (π + 1)) |
252 | | hashfz1 14252 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β (β―β(1...π)) = π) |
253 | 2, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (β―β(1...π)) = π) |
254 | 251, 253 | breq12d 5119 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((β―β(0...π)) β€
(β―β(1...π))
β (π + 1) β€ π)) |
255 | 249, 254 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((0...π) βΌ (1...π) β (π + 1) β€ π)) |
256 | 247, 255 | imbitrid 243 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((0...π) βΌ ran ((βfld
βΎs β) unitVec (1...π)) β§ ran ((βfld
βΎs β) unitVec (1...π)) β (1...π)) β (π + 1) β€ π)) |
257 | 246, 256 | mpan2i 696 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((0...π) βΌ ran ((βfld
βΎs β) unitVec (1...π)) β (π + 1) β€ π)) |
258 | 243, 257 | syl5 34 |
. . . . . . . . . . . . . . . 16
β’ (π β (((0...π) β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) βΌ ran ((βfld
βΎs β) unitVec (1...π))) β (π + 1) β€ π)) |
259 | 258 | expd 417 |
. . . . . . . . . . . . . . 15
β’ (π β ((0...π) β ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β (ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) βΌ ran ((βfld
βΎs β) unitVec (1...π)) β (π + 1) β€ π))) |
260 | 242, 259 | syl5 34 |
. . . . . . . . . . . . . 14
β’ (π β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β (ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) βΌ ran ((βfld
βΎs β) unitVec (1...π)) β (π + 1) β€ π))) |
261 | 260 | com23 86 |
. . . . . . . . . . . . 13
β’ (π β (ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) βΌ ran ((βfld
βΎs β) unitVec (1...π)) β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β (π + 1) β€ π))) |
262 | 238, 261 | syl5 34 |
. . . . . . . . . . . 12
β’ (π β ((π£ βΌ ran ((βfld
βΎs β) unitVec (1...π)) β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β π£) β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β (π + 1) β€ π))) |
263 | 262 | expdimp 454 |
. . . . . . . . . . 11
β’ ((π β§ π£ βΌ ran ((βfld
βΎs β) unitVec (1...π))) β (ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β π£ β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β (π + 1) β€ π))) |
264 | 236, 263 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ π£ β π« ran ((βfld
βΎs β) unitVec (1...π))) β (ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β π£ β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β (π + 1) β€ π))) |
265 | 264 | adantrd 493 |
. . . . . . . . 9
β’ ((π β§ π£ β π« ran ((βfld
βΎs β) unitVec (1...π))) β ((ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β π£ β§ (π£ βͺ β
) β
(mrIndβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π))))) β
((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β (π + 1) β€ π))) |
266 | 265 | rexlimdva 3149 |
. . . . . . . 8
β’ (π β (βπ£ β π« ran ((βfld
βΎs β) unitVec (1...π))(ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β π£ β§ (π£ βͺ β
) β
(mrIndβ(LSubSpβ((βfld βΎs β)
freeLMod (1...π))))) β
((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β (π + 1) β€ π))) |
267 | 231, 266 | syld 47 |
. . . . . . 7
β’ (π β (ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π))) β ((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β (π + 1) β€ π))) |
268 | 267 | impd 412 |
. . . . . 6
β’ (π β ((ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π))) β§ (π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV) β (π + 1) β€ π)) |
269 | 268 | ancomsd 467 |
. . . . 5
β’ (π β (((π β (0...π) β¦ (π β (1...π) β¦ πΆ)):(0...π)β1-1βV β§ ran (π β (0...π) β¦ (π β (1...π) β¦ πΆ)) β
(LIndSβ((βfld βΎs β) freeLMod
(1...π)))) β (π + 1) β€ π)) |
270 | 178, 269 | sylbird 260 |
. . . 4
β’ (π β (Β¬ βπ€ β ((β
βm (0...π))
β {((0...π) Γ
{0})})βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β (π + 1) β€ π)) |
271 | 9, 270 | mt3d 148 |
. . 3
β’ (π β βπ€ β ((β βm
(0...π)) β
{((0...π) Γ
{0})})βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0) |
272 | | eldifsn 4748 |
. . . . 5
β’ (π€ β ((β
βm (0...π))
β {((0...π) Γ
{0})}) β (π€ β
(β βm (0...π)) β§ π€ β ((0...π) Γ {0}))) |
273 | 42 | anim1i 616 |
. . . . 5
β’ ((π€ β (β
βm (0...π))
β§ π€ β ((0...π) Γ {0})) β (π€:(0...π)βΆβ β§ π€ β ((0...π) Γ {0}))) |
274 | 272, 273 | sylbi 216 |
. . . 4
β’ (π€ β ((β
βm (0...π))
β {((0...π) Γ
{0})}) β (π€:(0...π)βΆβ β§ π€ β ((0...π) Γ {0}))) |
275 | 93 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π€:(0...π)βΆβ) β β β
β) |
276 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π€:(0...π)βΆβ) β π β
β0) |
277 | 275, 276,
53 | elplyd 25579 |
. . . . . . . 8
β’ ((π β§ π€:(0...π)βΆβ) β (π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β
(Polyββ)) |
278 | 277 | adantrr 716 |
. . . . . . 7
β’ ((π β§ (π€:(0...π)βΆβ β§ π€ β ((0...π) Γ {0}))) β (π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β
(Polyββ)) |
279 | | uzdisj 13520 |
. . . . . . . . . . . . . . . . . 18
β’
((0...((π + 1)
β 1)) β© (β€β₯β(π + 1))) = β
|
280 | 2 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β β) |
281 | | pncan1 11584 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β ((π + 1) β 1) = π) |
282 | 280, 281 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π + 1) β 1) = π) |
283 | 282 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0...((π + 1) β 1)) = (0...π)) |
284 | 283 | ineq1d 4172 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((0...((π + 1) β 1)) β©
(β€β₯β(π + 1))) = ((0...π) β© (β€β₯β(π + 1)))) |
285 | 279, 284 | eqtr3id 2787 |
. . . . . . . . . . . . . . . . 17
β’ (π β β
= ((0...π) β©
(β€β₯β(π + 1)))) |
286 | 285 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β ((0...π) β© (β€β₯β(π + 1))) =
β
) |
287 | 128 | fconst 6729 |
. . . . . . . . . . . . . . . . . 18
β’
((β€β₯β(π + 1)) Γ
{0}):(β€β₯β(π + 1))βΆ{0} |
288 | | snssi 4769 |
. . . . . . . . . . . . . . . . . . . 20
β’ (0 β
β β {0} β β) |
289 | 96, 97, 288 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
β’ {0}
β β |
290 | 289, 93 | sstri 3954 |
. . . . . . . . . . . . . . . . . 18
β’ {0}
β β |
291 | | fss 6686 |
. . . . . . . . . . . . . . . . . 18
β’
((((β€β₯β(π + 1)) Γ
{0}):(β€β₯β(π + 1))βΆ{0} β§ {0} β β)
β ((β€β₯β(π + 1)) Γ
{0}):(β€β₯β(π + 1))βΆβ) |
292 | 287, 290,
291 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
β’
((β€β₯β(π + 1)) Γ
{0}):(β€β₯β(π + 1))βΆβ |
293 | | fun 6705 |
. . . . . . . . . . . . . . . . 17
β’ (((π€:(0...π)βΆβ β§
((β€β₯β(π + 1)) Γ
{0}):(β€β₯β(π + 1))βΆβ) β§ ((0...π) β©
(β€β₯β(π + 1))) = β
) β (π€ βͺ
((β€β₯β(π + 1)) Γ {0})):((0...π) βͺ (β€β₯β(π + 1)))βΆ(β βͺ
β)) |
294 | 292, 293 | mpanl2 700 |
. . . . . . . . . . . . . . . 16
β’ ((π€:(0...π)βΆβ β§ ((0...π) β©
(β€β₯β(π + 1))) = β
) β (π€ βͺ
((β€β₯β(π + 1)) Γ {0})):((0...π) βͺ (β€β₯β(π + 1)))βΆ(β βͺ
β)) |
295 | 286, 294 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((π€:(0...π)βΆβ β§ π) β (π€ βͺ ((β€β₯β(π + 1)) Γ {0})):((0...π) βͺ
(β€β₯β(π + 1)))βΆ(β βͺ
β)) |
296 | 295 | ancoms 460 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€:(0...π)βΆβ) β (π€ βͺ ((β€β₯β(π + 1)) Γ {0})):((0...π) βͺ
(β€β₯β(π + 1)))βΆ(β βͺ
β)) |
297 | | nn0uz 12810 |
. . . . . . . . . . . . . . . . . 18
β’
β0 = (β€β₯β0) |
298 | 6, 297 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π + 1) β
(β€β₯β0)) |
299 | | uzsplit 13519 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π + 1) β
(β€β₯β0) β (β€β₯β0) =
((0...((π + 1) β 1))
βͺ (β€β₯β(π + 1)))) |
300 | 298, 299 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β0) = ((0...((π + 1) β 1)) βͺ
(β€β₯β(π + 1)))) |
301 | 297, 300 | eqtrid 2785 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0 =
((0...((π + 1) β 1))
βͺ (β€β₯β(π + 1)))) |
302 | 283 | uneq1d 4123 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((0...((π + 1) β 1)) βͺ
(β€β₯β(π + 1))) = ((0...π) βͺ (β€β₯β(π + 1)))) |
303 | 301, 302 | eqtr2d 2774 |
. . . . . . . . . . . . . . . 16
β’ (π β ((0...π) βͺ (β€β₯β(π + 1))) =
β0) |
304 | | ssequn1 4141 |
. . . . . . . . . . . . . . . . . 18
β’ (β
β β β (β βͺ β) = β) |
305 | 93, 304 | mpbi 229 |
. . . . . . . . . . . . . . . . 17
β’ (β
βͺ β) = β |
306 | 305 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β (β βͺ β) =
β) |
307 | 303, 306 | feq23d 6664 |
. . . . . . . . . . . . . . 15
β’ (π β ((π€ βͺ ((β€β₯β(π + 1)) Γ {0})):((0...π) βͺ
(β€β₯β(π + 1)))βΆ(β βͺ β)
β (π€ βͺ
((β€β₯β(π + 1)) Γ
{0})):β0βΆβ)) |
308 | 307 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€:(0...π)βΆβ) β ((π€ βͺ
((β€β₯β(π + 1)) Γ {0})):((0...π) βͺ (β€β₯β(π + 1)))βΆ(β βͺ
β) β (π€ βͺ
((β€β₯β(π + 1)) Γ
{0})):β0βΆβ)) |
309 | 296, 308 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π€:(0...π)βΆβ) β (π€ βͺ ((β€β₯β(π + 1)) Γ
{0})):β0βΆβ) |
310 | | ffn 6669 |
. . . . . . . . . . . . . . . 16
β’ (π€:(0...π)βΆβ β π€ Fn (0...π)) |
311 | | fnimadisj 6634 |
. . . . . . . . . . . . . . . 16
β’ ((π€ Fn (0...π) β§ ((0...π) β© (β€β₯β(π + 1))) = β
) β (π€ β
(β€β₯β(π + 1))) = β
) |
312 | 310, 286,
311 | syl2anr 598 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π€:(0...π)βΆβ) β (π€ β (β€β₯β(π + 1))) =
β
) |
313 | 2 | nn0zd 12530 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β€) |
314 | 313 | peano2zd 12615 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π + 1) β β€) |
315 | | uzid 12783 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π + 1) β β€ β
(π + 1) β
(β€β₯β(π + 1))) |
316 | | ne0i 4295 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π + 1) β
(β€β₯β(π + 1)) β
(β€β₯β(π + 1)) β β
) |
317 | 314, 315,
316 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β(π + 1)) β β
) |
318 | | inidm 4179 |
. . . . . . . . . . . . . . . . . . 19
β’
((β€β₯β(π + 1)) β©
(β€β₯β(π + 1))) =
(β€β₯β(π + 1)) |
319 | 318 | neeq1i 3005 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€β₯β(π + 1)) β©
(β€β₯β(π + 1))) β β
β
(β€β₯β(π + 1)) β β
) |
320 | 317, 319 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (π β
((β€β₯β(π + 1)) β©
(β€β₯β(π + 1))) β β
) |
321 | | xpima2 6137 |
. . . . . . . . . . . . . . . . 17
β’
(((β€β₯β(π + 1)) β©
(β€β₯β(π + 1))) β β
β
(((β€β₯β(π + 1)) Γ {0}) β
(β€β₯β(π + 1))) = {0}) |
322 | 320, 321 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β
(((β€β₯β(π + 1)) Γ {0}) β
(β€β₯β(π + 1))) = {0}) |
323 | 322 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π€:(0...π)βΆβ) β
(((β€β₯β(π + 1)) Γ {0}) β
(β€β₯β(π + 1))) = {0}) |
324 | 312, 323 | uneq12d 4125 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€:(0...π)βΆβ) β ((π€ β
(β€β₯β(π + 1))) βͺ
(((β€β₯β(π + 1)) Γ {0}) β
(β€β₯β(π + 1)))) = (β
βͺ
{0})) |
325 | | imaundir 6104 |
. . . . . . . . . . . . . 14
β’ ((π€ βͺ
((β€β₯β(π + 1)) Γ {0})) β
(β€β₯β(π + 1))) = ((π€ β (β€β₯β(π + 1))) βͺ
(((β€β₯β(π + 1)) Γ {0}) β
(β€β₯β(π + 1)))) |
326 | | uncom 4114 |
. . . . . . . . . . . . . . 15
β’ (β
βͺ {0}) = ({0} βͺ β
) |
327 | | un0 4351 |
. . . . . . . . . . . . . . 15
β’ ({0}
βͺ β
) = {0} |
328 | 326, 327 | eqtr2i 2762 |
. . . . . . . . . . . . . 14
β’ {0} =
(β
βͺ {0}) |
329 | 324, 325,
328 | 3eqtr4g 2798 |
. . . . . . . . . . . . 13
β’ ((π β§ π€:(0...π)βΆβ) β ((π€ βͺ
((β€β₯β(π + 1)) Γ {0})) β
(β€β₯β(π + 1))) = {0}) |
330 | 286, 310 | anim12ci 615 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€:(0...π)βΆβ) β (π€ Fn (0...π) β§ ((0...π) β© (β€β₯β(π + 1))) =
β
)) |
331 | | fnconstg 6731 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (0 β
V β ((β€β₯β(π + 1)) Γ {0}) Fn
(β€β₯β(π + 1))) |
332 | 128, 331 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β€β₯β(π + 1)) Γ {0}) Fn
(β€β₯β(π + 1)) |
333 | | fvun1 6933 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π€ Fn (0...π) β§
((β€β₯β(π + 1)) Γ {0}) Fn
(β€β₯β(π + 1)) β§ (((0...π) β© (β€β₯β(π + 1))) = β
β§ π β (0...π))) β ((π€ βͺ ((β€β₯β(π + 1)) Γ {0}))βπ) = (π€βπ)) |
334 | 332, 333 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π€ Fn (0...π) β§ (((0...π) β© (β€β₯β(π + 1))) = β
β§ π β (0...π))) β ((π€ βͺ ((β€β₯β(π + 1)) Γ {0}))βπ) = (π€βπ)) |
335 | 334 | anassrs 469 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ Fn (0...π) β§ ((0...π) β© (β€β₯β(π + 1))) = β
) β§ π β (0...π)) β ((π€ βͺ ((β€β₯β(π + 1)) Γ {0}))βπ) = (π€βπ)) |
336 | 330, 335 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β ((π€ βͺ ((β€β₯β(π + 1)) Γ {0}))βπ) = (π€βπ)) |
337 | 336 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (π€βπ) = ((π€ βͺ ((β€β₯β(π + 1)) Γ {0}))βπ)) |
338 | 337 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β ((π€βπ) Β· (π¦βπ)) = (((π€ βͺ ((β€β₯β(π + 1)) Γ {0}))βπ) Β· (π¦βπ))) |
339 | 338 | sumeq2dv 15593 |
. . . . . . . . . . . . . 14
β’ ((π β§ π€:(0...π)βΆβ) β Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)) = Ξ£π β (0...π)(((π€ βͺ ((β€β₯β(π + 1)) Γ {0}))βπ) Β· (π¦βπ))) |
340 | 339 | mpteq2dv 5208 |
. . . . . . . . . . . . 13
β’ ((π β§ π€:(0...π)βΆβ) β (π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) = (π¦ β β β¦ Ξ£π β (0...π)(((π€ βͺ ((β€β₯β(π + 1)) Γ {0}))βπ) Β· (π¦βπ)))) |
341 | 277, 276,
309, 329, 340 | coeeq 25604 |
. . . . . . . . . . . 12
β’ ((π β§ π€:(0...π)βΆβ) β (coeffβ(π¦ β β β¦
Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))) = (π€ βͺ ((β€β₯β(π + 1)) Γ
{0}))) |
342 | 341 | reseq1d 5937 |
. . . . . . . . . . 11
β’ ((π β§ π€:(0...π)βΆβ) β
((coeffβ(π¦ β
β β¦ Ξ£π
β (0...π)((π€βπ) Β· (π¦βπ)))) βΎ (0...π)) = ((π€ βͺ ((β€β₯β(π + 1)) Γ {0})) βΎ
(0...π))) |
343 | | res0 5942 |
. . . . . . . . . . . . . 14
β’ (π€ βΎ β
) =
β
|
344 | 285 | reseq2d 5938 |
. . . . . . . . . . . . . 14
β’ (π β (π€ βΎ β
) = (π€ βΎ ((0...π) β© (β€β₯β(π + 1))))) |
345 | | res0 5942 |
. . . . . . . . . . . . . . 15
β’
(((β€β₯β(π + 1)) Γ {0}) βΎ β
) =
β
|
346 | 285 | reseq2d 5938 |
. . . . . . . . . . . . . . 15
β’ (π β
(((β€β₯β(π + 1)) Γ {0}) βΎ β
) =
(((β€β₯β(π + 1)) Γ {0}) βΎ ((0...π) β©
(β€β₯β(π + 1))))) |
347 | 345, 346 | eqtr3id 2787 |
. . . . . . . . . . . . . 14
β’ (π β β
=
(((β€β₯β(π + 1)) Γ {0}) βΎ ((0...π) β©
(β€β₯β(π + 1))))) |
348 | 343, 344,
347 | 3eqtr3a 2797 |
. . . . . . . . . . . . 13
β’ (π β (π€ βΎ ((0...π) β© (β€β₯β(π + 1)))) =
(((β€β₯β(π + 1)) Γ {0}) βΎ ((0...π) β©
(β€β₯β(π + 1))))) |
349 | | fss 6686 |
. . . . . . . . . . . . . . 15
β’
((((β€β₯β(π + 1)) Γ
{0}):(β€β₯β(π + 1))βΆ{0} β§ {0} β β)
β ((β€β₯β(π + 1)) Γ
{0}):(β€β₯β(π + 1))βΆβ) |
350 | 287, 289,
349 | mp2an 691 |
. . . . . . . . . . . . . 14
β’
((β€β₯β(π + 1)) Γ
{0}):(β€β₯β(π + 1))βΆβ |
351 | | fresaunres1 6716 |
. . . . . . . . . . . . . 14
β’ ((π€:(0...π)βΆβ β§
((β€β₯β(π + 1)) Γ
{0}):(β€β₯β(π + 1))βΆβ β§ (π€ βΎ ((0...π) β© (β€β₯β(π + 1)))) =
(((β€β₯β(π + 1)) Γ {0}) βΎ ((0...π) β©
(β€β₯β(π + 1))))) β ((π€ βͺ ((β€β₯β(π + 1)) Γ {0})) βΎ
(0...π)) = π€) |
352 | 350, 351 | mp3an2 1450 |
. . . . . . . . . . . . 13
β’ ((π€:(0...π)βΆβ β§ (π€ βΎ ((0...π) β© (β€β₯β(π + 1)))) =
(((β€β₯β(π + 1)) Γ {0}) βΎ ((0...π) β©
(β€β₯β(π + 1))))) β ((π€ βͺ ((β€β₯β(π + 1)) Γ {0})) βΎ
(0...π)) = π€) |
353 | 348, 352 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π€:(0...π)βΆβ β§ π) β ((π€ βͺ ((β€β₯β(π + 1)) Γ {0})) βΎ
(0...π)) = π€) |
354 | 353 | ancoms 460 |
. . . . . . . . . . 11
β’ ((π β§ π€:(0...π)βΆβ) β ((π€ βͺ
((β€β₯β(π + 1)) Γ {0})) βΎ (0...π)) = π€) |
355 | 342, 354 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π€:(0...π)βΆβ) β
((coeffβ(π¦ β
β β¦ Ξ£π
β (0...π)((π€βπ) Β· (π¦βπ)))) βΎ (0...π)) = π€) |
356 | | fveq2 6843 |
. . . . . . . . . . 11
β’ ((π¦ β β β¦
Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) = 0π β
(coeffβ(π¦ β
β β¦ Ξ£π
β (0...π)((π€βπ) Β· (π¦βπ)))) =
(coeffβ0π)) |
357 | 356 | reseq1d 5937 |
. . . . . . . . . 10
β’ ((π¦ β β β¦
Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) = 0π β
((coeffβ(π¦ β
β β¦ Ξ£π
β (0...π)((π€βπ) Β· (π¦βπ)))) βΎ (0...π)) = ((coeffβ0π)
βΎ (0...π))) |
358 | | eqtr2 2757 |
. . . . . . . . . . . 12
β’
((((coeffβ(π¦
β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))) βΎ (0...π)) = π€ β§ ((coeffβ(π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))) βΎ (0...π)) = ((coeffβ0π)
βΎ (0...π))) β
π€ =
((coeffβ0π) βΎ (0...π))) |
359 | | coe0 25633 |
. . . . . . . . . . . . . 14
β’
(coeffβ0π) = (β0 Γ
{0}) |
360 | 359 | reseq1i 5934 |
. . . . . . . . . . . . 13
β’
((coeffβ0π) βΎ (0...π)) = ((β0 Γ {0})
βΎ (0...π)) |
361 | | elfznn0 13540 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (0...π) β π₯ β β0) |
362 | 361 | ssriv 3949 |
. . . . . . . . . . . . . 14
β’
(0...π) β
β0 |
363 | | xpssres 5975 |
. . . . . . . . . . . . . 14
β’
((0...π) β
β0 β ((β0 Γ {0}) βΎ
(0...π)) = ((0...π) Γ {0})) |
364 | 362, 363 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
((β0 Γ {0}) βΎ (0...π)) = ((0...π) Γ {0}) |
365 | 360, 364 | eqtri 2761 |
. . . . . . . . . . . 12
β’
((coeffβ0π) βΎ (0...π)) = ((0...π) Γ {0}) |
366 | 358, 365 | eqtrdi 2789 |
. . . . . . . . . . 11
β’
((((coeffβ(π¦
β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))) βΎ (0...π)) = π€ β§ ((coeffβ(π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))) βΎ (0...π)) = ((coeffβ0π)
βΎ (0...π))) β
π€ = ((0...π) Γ {0})) |
367 | 366 | ex 414 |
. . . . . . . . . 10
β’
(((coeffβ(π¦
β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))) βΎ (0...π)) = π€ β (((coeffβ(π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))) βΎ (0...π)) = ((coeffβ0π)
βΎ (0...π)) β
π€ = ((0...π) Γ {0}))) |
368 | 355, 357,
367 | syl2im 40 |
. . . . . . . . 9
β’ ((π β§ π€:(0...π)βΆβ) β ((π¦ β β β¦
Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) = 0π β π€ = ((0...π) Γ {0}))) |
369 | 368 | necon3d 2961 |
. . . . . . . 8
β’ ((π β§ π€:(0...π)βΆβ) β (π€ β ((0...π) Γ {0}) β (π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β
0π)) |
370 | 369 | impr 456 |
. . . . . . 7
β’ ((π β§ (π€:(0...π)βΆβ β§ π€ β ((0...π) Γ {0}))) β (π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β
0π) |
371 | | eldifsn 4748 |
. . . . . . 7
β’ ((π¦ β β β¦
Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β ((Polyββ) β
{0π}) β ((π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β (Polyββ) β§ (π¦ β β β¦
Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β
0π)) |
372 | 278, 370,
371 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ (π€:(0...π)βΆβ β§ π€ β ((0...π) Γ {0}))) β (π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β ((Polyββ) β
{0π})) |
373 | 372 | adantrr 716 |
. . . . 5
β’ ((π β§ ((π€:(0...π)βΆβ β§ π€ β ((0...π) Γ {0})) β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β (π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β ((Polyββ) β
{0π})) |
374 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π¦ = π΄ β (π¦βπ) = (π΄βπ)) |
375 | 374 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β ((π€βπ) Β· (π¦βπ)) = ((π€βπ) Β· (π΄βπ))) |
376 | 375 | sumeq2sdv 15594 |
. . . . . . . . . 10
β’ (π¦ = π΄ β Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)) = Ξ£π β (0...π)((π€βπ) Β· (π΄βπ))) |
377 | | eqid 2733 |
. . . . . . . . . 10
β’ (π¦ β β β¦
Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) = (π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) |
378 | | sumex 15578 |
. . . . . . . . . 10
β’
Ξ£π β
(0...π)((π€βπ) Β· (π΄βπ)) β V |
379 | 376, 377,
378 | fvmpt 6949 |
. . . . . . . . 9
β’ (π΄ β β β ((π¦ β β β¦
Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))βπ΄) = Ξ£π β (0...π)((π€βπ) Β· (π΄βπ))) |
380 | 1, 379 | syl 17 |
. . . . . . . 8
β’ (π β ((π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))βπ΄) = Ξ£π β (0...π)((π€βπ) Β· (π΄βπ))) |
381 | 380 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β ((π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))βπ΄) = Ξ£π β (0...π)((π€βπ) Β· (π΄βπ))) |
382 | 107 | adantll 713 |
. . . . . . . . . . . . . 14
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β (π€βπ) β β) |
383 | | aacllem.2 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β π β β) |
384 | 383 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0...π)) β§ π β (1...π)) β π β β) |
385 | 110, 384 | mulcld 11180 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π)) β§ π β (1...π)) β (πΆ Β· π) β β) |
386 | 385 | adantllr 718 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β§ π β (1...π)) β (πΆ Β· π) β β) |
387 | 51, 382, 386 | fsummulc2 15674 |
. . . . . . . . . . . . 13
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β ((π€βπ) Β· Ξ£π β (1...π)(πΆ Β· π)) = Ξ£π β (1...π)((π€βπ) Β· (πΆ Β· π))) |
388 | | aacllem.4 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...π)) β (π΄βπ) = Ξ£π β (1...π)(πΆ Β· π)) |
389 | 388 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β ((π€βπ) Β· (π΄βπ)) = ((π€βπ) Β· Ξ£π β (1...π)(πΆ Β· π))) |
390 | 389 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β ((π€βπ) Β· (π΄βπ)) = ((π€βπ) Β· Ξ£π β (1...π)(πΆ Β· π))) |
391 | 382 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β§ π β (1...π)) β (π€βπ) β β) |
392 | 110 | adantllr 718 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β§ π β (1...π)) β πΆ β β) |
393 | | simpll 766 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β π) |
394 | 393, 383 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β§ π β (1...π)) β π β β) |
395 | 391, 392,
394 | mulassd 11183 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β§ π β (1...π)) β (((π€βπ) Β· πΆ) Β· π) = ((π€βπ) Β· (πΆ Β· π))) |
396 | 395 | sumeq2dv 15593 |
. . . . . . . . . . . . 13
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β Ξ£π β (1...π)(((π€βπ) Β· πΆ) Β· π) = Ξ£π β (1...π)((π€βπ) Β· (πΆ Β· π))) |
397 | 387, 390,
396 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (0...π)) β ((π€βπ) Β· (π΄βπ)) = Ξ£π β (1...π)(((π€βπ) Β· πΆ) Β· π)) |
398 | 397 | sumeq2dv 15593 |
. . . . . . . . . . 11
β’ ((π β§ π€:(0...π)βΆβ) β Ξ£π β (0...π)((π€βπ) Β· (π΄βπ)) = Ξ£π β (0...π)Ξ£π β (1...π)(((π€βπ) Β· πΆ) Β· π)) |
399 | 107 | ad2ant2lr 747 |
. . . . . . . . . . . . . 14
β’ (((π β§ π€:(0...π)βΆβ) β§ (π β (0...π) β§ π β (1...π))) β (π€βπ) β β) |
400 | 110 | anasss 468 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β (0...π) β§ π β (1...π))) β πΆ β β) |
401 | 400 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ π€:(0...π)βΆβ) β§ (π β (0...π) β§ π β (1...π))) β πΆ β β) |
402 | 399, 401 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ (((π β§ π€:(0...π)βΆβ) β§ (π β (0...π) β§ π β (1...π))) β ((π€βπ) Β· πΆ) β β) |
403 | 383 | ad2ant2rl 748 |
. . . . . . . . . . . . 13
β’ (((π β§ π€:(0...π)βΆβ) β§ (π β (0...π) β§ π β (1...π))) β π β β) |
404 | 402, 403 | mulcld 11180 |
. . . . . . . . . . . 12
β’ (((π β§ π€:(0...π)βΆβ) β§ (π β (0...π) β§ π β (1...π))) β (((π€βπ) Β· πΆ) Β· π) β β) |
405 | 43, 69, 404 | fsumcom 15665 |
. . . . . . . . . . 11
β’ ((π β§ π€:(0...π)βΆβ) β Ξ£π β (0...π)Ξ£π β (1...π)(((π€βπ) Β· πΆ) Β· π) = Ξ£π β (1...π)Ξ£π β (0...π)(((π€βπ) Β· πΆ) Β· π)) |
406 | 398, 405 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π€:(0...π)βΆβ) β Ξ£π β (0...π)((π€βπ) Β· (π΄βπ)) = Ξ£π β (1...π)Ξ£π β (0...π)(((π€βπ) Β· πΆ) Β· π)) |
407 | 406 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β Ξ£π β (0...π)((π€βπ) Β· (π΄βπ)) = Ξ£π β (1...π)Ξ£π β (0...π)(((π€βπ) Β· πΆ) Β· π)) |
408 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²ππ |
409 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π π€:(0...π)βΆβ |
410 | | nfra1 3266 |
. . . . . . . . . . . . 13
β’
β²πβπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 |
411 | 409, 410 | nfan 1903 |
. . . . . . . . . . . 12
β’
β²π(π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0) |
412 | 408, 411 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π(π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) |
413 | | rspa 3230 |
. . . . . . . . . . . . . . . 16
β’
((βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β§ π β (1...π)) β Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0) |
414 | 413 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’
((βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0 β§ π β (1...π)) β (Ξ£π β (0...π)((π€βπ) Β· πΆ) Β· π) = (0 Β· π)) |
415 | 414 | adantll 713 |
. . . . . . . . . . . . . 14
β’ (((π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0) β§ π β (1...π)) β (Ξ£π β (0...π)((π€βπ) Β· πΆ) Β· π) = (0 Β· π)) |
416 | 415 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β§ π β (1...π)) β (Ξ£π β (0...π)((π€βπ) Β· πΆ) Β· π) = (0 Β· π)) |
417 | 383 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β π β β) |
418 | 92, 417, 113 | fsummulc1 15675 |
. . . . . . . . . . . . . 14
β’ (((π β§ π€:(0...π)βΆβ) β§ π β (1...π)) β (Ξ£π β (0...π)((π€βπ) Β· πΆ) Β· π) = Ξ£π β (0...π)(((π€βπ) Β· πΆ) Β· π)) |
419 | 418 | adantlrr 720 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β§ π β (1...π)) β (Ξ£π β (0...π)((π€βπ) Β· πΆ) Β· π) = Ξ£π β (0...π)(((π€βπ) Β· πΆ) Β· π)) |
420 | 383 | mul02d 11358 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (0 Β· π) = 0) |
421 | 420 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β§ π β (1...π)) β (0 Β· π) = 0) |
422 | 416, 419,
421 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
β’ (((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β§ π β (1...π)) β Ξ£π β (0...π)(((π€βπ) Β· πΆ) Β· π) = 0) |
423 | 422 | ex 414 |
. . . . . . . . . . 11
β’ ((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β (π β (1...π) β Ξ£π β (0...π)(((π€βπ) Β· πΆ) Β· π) = 0)) |
424 | 412, 423 | ralrimi 3239 |
. . . . . . . . . 10
β’ ((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β βπ β (1...π)Ξ£π β (0...π)(((π€βπ) Β· πΆ) Β· π) = 0) |
425 | 424 | sumeq2d 15592 |
. . . . . . . . 9
β’ ((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β Ξ£π β (1...π)Ξ£π β (0...π)(((π€βπ) Β· πΆ) Β· π) = Ξ£π β (1...π)0) |
426 | 407, 425 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β Ξ£π β (0...π)((π€βπ) Β· (π΄βπ)) = Ξ£π β (1...π)0) |
427 | 22 | olci 865 |
. . . . . . . . 9
β’
((1...π) β
(β€β₯βπ΅) β¨ (1...π) β Fin) |
428 | | sumz 15612 |
. . . . . . . . 9
β’
(((1...π) β
(β€β₯βπ΅) β¨ (1...π) β Fin) β Ξ£π β (1...π)0 = 0) |
429 | 427, 428 | ax-mp 5 |
. . . . . . . 8
β’
Ξ£π β
(1...π)0 =
0 |
430 | 426, 429 | eqtrdi 2789 |
. . . . . . 7
β’ ((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β Ξ£π β (0...π)((π€βπ) Β· (π΄βπ)) = 0) |
431 | 381, 430 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ (π€:(0...π)βΆβ β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β ((π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))βπ΄) = 0) |
432 | 431 | adantrlr 722 |
. . . . 5
β’ ((π β§ ((π€:(0...π)βΆβ β§ π€ β ((0...π) Γ {0})) β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β ((π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))βπ΄) = 0) |
433 | | fveq1 6842 |
. . . . . . 7
β’ (π₯ = (π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β (π₯βπ΄) = ((π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))βπ΄)) |
434 | 433 | eqeq1d 2735 |
. . . . . 6
β’ (π₯ = (π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β ((π₯βπ΄) = 0 β ((π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))βπ΄) = 0)) |
435 | 434 | rspcev 3580 |
. . . . 5
β’ (((π¦ β β β¦
Ξ£π β (0...π)((π€βπ) Β· (π¦βπ))) β ((Polyββ) β
{0π}) β§ ((π¦ β β β¦ Ξ£π β (0...π)((π€βπ) Β· (π¦βπ)))βπ΄) = 0) β βπ₯ β ((Polyββ) β
{0π})(π₯βπ΄) = 0) |
436 | 373, 432,
435 | syl2anc 585 |
. . . 4
β’ ((π β§ ((π€:(0...π)βΆβ β§ π€ β ((0...π) Γ {0})) β§ βπ β (1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β βπ₯ β ((Polyββ) β
{0π})(π₯βπ΄) = 0) |
437 | 274, 436 | sylanr1 681 |
. . 3
β’ ((π β§ (π€ β ((β βm
(0...π)) β
{((0...π) Γ {0})})
β§ βπ β
(1...π)Ξ£π β (0...π)((π€βπ) Β· πΆ) = 0)) β βπ₯ β ((Polyββ) β
{0π})(π₯βπ΄) = 0) |
438 | 271, 437 | rexlimddv 3155 |
. 2
β’ (π β βπ₯ β ((Polyββ) β
{0π})(π₯βπ΄) = 0) |
439 | | elqaa 25698 |
. 2
β’ (π΄ β πΈ β (π΄ β β β§
βπ₯ β
((Polyββ) β {0π})(π₯βπ΄) = 0)) |
440 | 1, 438, 439 | sylanbrc 584 |
1
β’ (π β π΄ β πΈ) |