Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
3 | | eqid 2733 |
. . . . 5
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
4 | 1, 2, 3 | lcoval 46579 |
. . . 4
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(πΆ β (π LinCo π) β (πΆ β (Baseβπ) β§ βπ¦ β ((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))))) |
5 | 1, 2, 3 | lcoval 46579 |
. . . 4
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(π· β (π LinCo π) β (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))))) |
6 | 4, 5 | anbi12d 632 |
. . 3
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
((πΆ β (π LinCo π) β§ π· β (π LinCo π)) β ((πΆ β (Baseβπ) β§ βπ¦ β ((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))))) |
7 | | simpll 766 |
. . . . . 6
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
((πΆ β
(Baseβπ) β§
βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))))) β π β LMod) |
8 | | simpll 766 |
. . . . . . 7
β’ (((πΆ β (Baseβπ) β§ βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β πΆ β (Baseβπ)) |
9 | 8 | adantl 483 |
. . . . . 6
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
((πΆ β
(Baseβπ) β§
βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))))) β πΆ β (Baseβπ)) |
10 | | simprl 770 |
. . . . . . 7
β’ (((πΆ β (Baseβπ) β§ βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β π· β (Baseβπ)) |
11 | 10 | adantl 483 |
. . . . . 6
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
((πΆ β
(Baseβπ) β§
βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))))) β π· β (Baseβπ)) |
12 | | lincsumcl.b |
. . . . . . 7
β’ + =
(+gβπ) |
13 | 1, 12 | lmodvacl 20351 |
. . . . . 6
β’ ((π β LMod β§ πΆ β (Baseβπ) β§ π· β (Baseβπ)) β (πΆ + π·) β (Baseβπ)) |
14 | 7, 9, 11, 13 | syl3anc 1372 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
((πΆ β
(Baseβπ) β§
βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))))) β (πΆ + π·) β (Baseβπ)) |
15 | 2 | lmodfgrp 20345 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β LMod β
(Scalarβπ) β
Grp) |
16 | 15 | grpmndd 18765 |
. . . . . . . . . . . . . . . . . 18
β’ (π β LMod β
(Scalarβπ) β
Mnd) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(Scalarβπ) β
Mnd) |
18 | 17 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β (Scalarβπ) β Mnd) |
19 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
π β π«
(Baseβπ)) |
20 | 19 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β π β π« (Baseβπ)) |
21 | | simpll 766 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β π¦ β ((Baseβ(Scalarβπ)) βm π)) |
22 | | simpl 484 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β
((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β π₯ β ((Baseβ(Scalarβπ)) βm π)) |
23 | 21, 22 | anim12i 614 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β (π¦ β ((Baseβ(Scalarβπ)) βm π) β§ π₯ β ((Baseβ(Scalarβπ)) βm π))) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β (π¦ β ((Baseβ(Scalarβπ)) βm π) β§ π₯ β ((Baseβ(Scalarβπ)) βm π))) |
25 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
26 | 3, 25 | ofaddmndmap 46505 |
. . . . . . . . . . . . . . . 16
β’
(((Scalarβπ)
β Mnd β§ π β
π« (Baseβπ)
β§ (π¦ β
((Baseβ(Scalarβπ)) βm π) β§ π₯ β ((Baseβ(Scalarβπ)) βm π))) β (π¦ βf
(+gβ(Scalarβπ))π₯) β ((Baseβ(Scalarβπ)) βm π)) |
27 | 18, 20, 24, 26 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β (π¦ βf
(+gβ(Scalarβπ))π₯) β ((Baseβ(Scalarβπ)) βm π)) |
28 | 16 | anim1i 616 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
((Scalarβπ) β
Mnd β§ π β
π« (Baseβπ))) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β ((Scalarβπ) β Mnd β§ π β π«
(Baseβπ))) |
30 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β π¦ finSupp
(0gβ(Scalarβπ))) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β π¦ finSupp
(0gβ(Scalarβπ))) |
32 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β
((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β π₯ finSupp
(0gβ(Scalarβπ))) |
33 | 31, 32 | anim12i 614 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β (π¦ finSupp
(0gβ(Scalarβπ)) β§ π₯ finSupp
(0gβ(Scalarβπ)))) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β (π¦ finSupp
(0gβ(Scalarβπ)) β§ π₯ finSupp
(0gβ(Scalarβπ)))) |
35 | 3 | mndpfsupp 46538 |
. . . . . . . . . . . . . . . 16
β’
((((Scalarβπ)
β Mnd β§ π β
π« (Baseβπ))
β§ (π¦ β
((Baseβ(Scalarβπ)) βm π) β§ π₯ β ((Baseβ(Scalarβπ)) βm π)) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ π₯ finSupp
(0gβ(Scalarβπ)))) β (π¦ βf
(+gβ(Scalarβπ))π₯) finSupp
(0gβ(Scalarβπ))) |
36 | 29, 24, 34, 35 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β (π¦ βf
(+gβ(Scalarβπ))π₯) finSupp
(0gβ(Scalarβπ))) |
37 | | oveq12 7367 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΆ = (π¦( linC βπ)π) β§ π· = (π₯( linC βπ)π)) β (πΆ + π·) = ((π¦( linC βπ)π) + (π₯( linC βπ)π))) |
38 | 37 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π· = (π₯( linC βπ)π) β (πΆ = (π¦( linC βπ)π) β (πΆ + π·) = ((π¦( linC βπ)π) + (π₯( linC βπ)π)))) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)) β (πΆ = (π¦( linC βπ)π) β (πΆ + π·) = ((π¦( linC βπ)π) + (π₯( linC βπ)π)))) |
40 | 39 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β
((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (πΆ = (π¦( linC βπ)π) β (πΆ + π·) = ((π¦( linC βπ)π) + (π₯( linC βπ)π)))) |
41 | 40 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΆ = (π¦( linC βπ)π) β ((π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (πΆ + π·) = ((π¦( linC βπ)π) + (π₯( linC βπ)π)))) |
42 | 41 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π)) β ((π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (πΆ + π·) = ((π¦( linC βπ)π) + (π₯( linC βπ)π)))) |
43 | 42 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β ((π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (πΆ + π·) = ((π¦( linC βπ)π) + (π₯( linC βπ)π)))) |
44 | 43 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β ((π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (πΆ + π·) = ((π¦( linC βπ)π) + (π₯( linC βπ)π)))) |
45 | 44 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β (πΆ + π·) = ((π¦( linC βπ)π) + (π₯( linC βπ)π))) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β (πΆ + π·) = ((π¦( linC βπ)π) + (π₯( linC βπ)π))) |
47 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β (π β LMod β§ π β π« (Baseβπ))) |
48 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦( linC βπ)π) = (π¦( linC βπ)π) |
49 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯( linC βπ)π) = (π₯( linC βπ)π) |
50 | 12, 48, 49, 2, 3, 25 | lincsum 46596 |
. . . . . . . . . . . . . . . . 17
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π¦ β
((Baseβ(Scalarβπ)) βm π) β§ π₯ β ((Baseβ(Scalarβπ)) βm π)) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ π₯ finSupp
(0gβ(Scalarβπ)))) β ((π¦( linC βπ)π) + (π₯( linC βπ)π)) = ((π¦ βf
(+gβ(Scalarβπ))π₯)( linC βπ)π)) |
51 | 47, 24, 34, 50 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β ((π¦( linC βπ)π) + (π₯( linC βπ)π)) = ((π¦ βf
(+gβ(Scalarβπ))π₯)( linC βπ)π)) |
52 | 46, 51 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β (πΆ + π·) = ((π¦ βf
(+gβ(Scalarβπ))π₯)( linC βπ)π)) |
53 | | breq1 5109 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π¦ βf
(+gβ(Scalarβπ))π₯) β (π finSupp
(0gβ(Scalarβπ)) β (π¦ βf
(+gβ(Scalarβπ))π₯) finSupp
(0gβ(Scalarβπ)))) |
54 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π¦ βf
(+gβ(Scalarβπ))π₯) β (π ( linC βπ)π) = ((π¦ βf
(+gβ(Scalarβπ))π₯)( linC βπ)π)) |
55 | 54 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π¦ βf
(+gβ(Scalarβπ))π₯) β ((πΆ + π·) = (π ( linC βπ)π) β (πΆ + π·) = ((π¦ βf
(+gβ(Scalarβπ))π₯)( linC βπ)π))) |
56 | 53, 55 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ (π = (π¦ βf
(+gβ(Scalarβπ))π₯) β ((π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π)) β ((π¦ βf
(+gβ(Scalarβπ))π₯) finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = ((π¦ βf
(+gβ(Scalarβπ))π₯)( linC βπ)π)))) |
57 | 56 | rspcev 3580 |
. . . . . . . . . . . . . . 15
β’ (((π¦ βf
(+gβ(Scalarβπ))π₯) β ((Baseβ(Scalarβπ)) βm π) β§ ((π¦ βf
(+gβ(Scalarβπ))π₯) finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = ((π¦ βf
(+gβ(Scalarβπ))π₯)( linC βπ)π))) β βπ β ((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π))) |
58 | 27, 36, 52, 57 | syl12anc 836 |
. . . . . . . . . . . . . 14
β’
(((((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (πΆ β (Baseβπ) β§ π· β (Baseβπ))) β§ (π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β§ (π β LMod β§ π β π« (Baseβπ))) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π))) |
59 | 58 | exp41 436 |
. . . . . . . . . . . . 13
β’ ((π¦ β
((Baseβ(Scalarβπ)) βm π) β§ (π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β ((πΆ β (Baseβπ) β§ π· β (Baseβπ)) β ((π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β ((π β LMod β§ π β π« (Baseβπ)) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π)))))) |
60 | 59 | rexlimiva 3141 |
. . . . . . . . . . . 12
β’
(βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π)) β ((πΆ β (Baseβπ) β§ π· β (Baseβπ)) β ((π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β ((π β LMod β§ π β π« (Baseβπ)) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π)))))) |
61 | 60 | expd 417 |
. . . . . . . . . . 11
β’
(βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π)) β (πΆ β (Baseβπ) β (π· β (Baseβπ) β ((π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β ((π β LMod β§ π β π« (Baseβπ)) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π))))))) |
62 | 61 | impcom 409 |
. . . . . . . . . 10
β’ ((πΆ β (Baseβπ) β§ βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β (π· β (Baseβπ) β ((π₯ β ((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β ((π β LMod β§ π β π« (Baseβπ)) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π)))))) |
63 | 62 | com13 88 |
. . . . . . . . 9
β’ ((π₯ β
((Baseβ(Scalarβπ)) βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (π· β (Baseβπ) β ((πΆ β (Baseβπ) β§ βπ¦ β ((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β ((π β LMod β§ π β π« (Baseβπ)) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π)))))) |
64 | 63 | rexlimiva 3141 |
. . . . . . . 8
β’
(βπ₯ β
((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)) β (π· β (Baseβπ) β ((πΆ β (Baseβπ) β§ βπ¦ β ((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β ((π β LMod β§ π β π« (Baseβπ)) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π)))))) |
65 | 64 | impcom 409 |
. . . . . . 7
β’ ((π· β (Baseβπ) β§ βπ₯ β
((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β ((πΆ β (Baseβπ) β§ βπ¦ β ((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β ((π β LMod β§ π β π« (Baseβπ)) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π))))) |
66 | 65 | impcom 409 |
. . . . . 6
β’ (((πΆ β (Baseβπ) β§ βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β ((π β LMod β§ π β π« (Baseβπ)) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π)))) |
67 | 66 | impcom 409 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
((πΆ β
(Baseβπ) β§
βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))))) β βπ β ((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π))) |
68 | 1, 2, 3 | lcoval 46579 |
. . . . . 6
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
((πΆ + π·) β (π LinCo π) β ((πΆ + π·) β (Baseβπ) β§ βπ β ((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π))))) |
69 | 68 | adantr 482 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
((πΆ β
(Baseβπ) β§
βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))))) β ((πΆ + π·) β (π LinCo π) β ((πΆ + π·) β (Baseβπ) β§ βπ β ((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ + π·) = (π ( linC βπ)π))))) |
70 | 14, 67, 69 | mpbir2and 712 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
((πΆ β
(Baseβπ) β§
βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))))) β (πΆ + π·) β (π LinCo π)) |
71 | 70 | ex 414 |
. . 3
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(((πΆ β
(Baseβπ) β§
βπ¦ β
((Baseβ(Scalarβπ)) βm π)(π¦ finSupp
(0gβ(Scalarβπ)) β§ πΆ = (π¦( linC βπ)π))) β§ (π· β (Baseβπ) β§ βπ₯ β ((Baseβ(Scalarβπ)) βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β (πΆ + π·) β (π LinCo π))) |
72 | 6, 71 | sylbid 239 |
. 2
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
((πΆ β (π LinCo π) β§ π· β (π LinCo π)) β (πΆ + π·) β (π LinCo π))) |
73 | 72 | imp 408 |
1
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(πΆ β (π LinCo π) β§ π· β (π LinCo π))) β (πΆ + π·) β (π LinCo π)) |