Step | Hyp | Ref
| Expression |
1 | | fvex 6901 |
. . . 4
β’
(0gβπ) β V |
2 | 1 | snid 4663 |
. . 3
β’
(0gβπ) β {(0gβπ)} |
3 | | oveq2 7413 |
. . . 4
β’ (π = β
β (π LinCo π) = (π LinCo β
)) |
4 | | lmodgrp 20470 |
. . . . . 6
β’ (π β LMod β π β Grp) |
5 | | grpmnd 18822 |
. . . . . 6
β’ (π β Grp β π β Mnd) |
6 | | lco0 47061 |
. . . . . 6
β’ (π β Mnd β (π LinCo β
) =
{(0gβπ)}) |
7 | 4, 5, 6 | 3syl 18 |
. . . . 5
β’ (π β LMod β (π LinCo β
) =
{(0gβπ)}) |
8 | 7 | adantr 481 |
. . . 4
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(π LinCo β
) =
{(0gβπ)}) |
9 | 3, 8 | sylan9eq 2792 |
. . 3
β’ ((π = β
β§ (π β LMod β§ π β π«
(Baseβπ))) β
(π LinCo π) = {(0gβπ)}) |
10 | 2, 9 | eleqtrrid 2840 |
. 2
β’ ((π = β
β§ (π β LMod β§ π β π«
(Baseβπ))) β
(0gβπ)
β (π LinCo π)) |
11 | | eqid 2732 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
12 | | eqid 2732 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
13 | 11, 12 | lmod0vcl 20493 |
. . . . 5
β’ (π β LMod β
(0gβπ)
β (Baseβπ)) |
14 | 13 | adantr 481 |
. . . 4
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(0gβπ)
β (Baseβπ)) |
15 | 14 | adantl 482 |
. . 3
β’ ((Β¬
π = β
β§ (π β LMod β§ π β π«
(Baseβπ))) β
(0gβπ)
β (Baseβπ)) |
16 | | eqid 2732 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
17 | | eqid 2732 |
. . . . . 6
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
18 | | eqidd 2733 |
. . . . . . 7
β’ (π£ = π€ β
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ))) |
19 | 18 | cbvmptv 5260 |
. . . . . 6
β’ (π£ β π β¦
(0gβ(Scalarβπ))) = (π€ β π β¦
(0gβ(Scalarβπ))) |
20 | | eqid 2732 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
21 | 11, 16, 17, 12, 19, 20 | lcoc0 47056 |
. . . . 5
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
((π£ β π β¦
(0gβ(Scalarβπ))) β ((Baseβ(Scalarβπ)) βm π) β§ (π£ β π β¦
(0gβ(Scalarβπ))) finSupp
(0gβ(Scalarβπ)) β§ ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) = (0gβπ))) |
22 | 21 | adantl 482 |
. . . 4
β’ ((Β¬
π = β
β§ (π β LMod β§ π β π«
(Baseβπ))) β
((π£ β π β¦
(0gβ(Scalarβπ))) β ((Baseβ(Scalarβπ)) βm π) β§ (π£ β π β¦
(0gβ(Scalarβπ))) finSupp
(0gβ(Scalarβπ)) β§ ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) = (0gβπ))) |
23 | | simpl 483 |
. . . . . . . 8
β’ (((π£ β π β¦
(0gβ(Scalarβπ))) β ((Baseβ(Scalarβπ)) βm π) β§ (Β¬ π = β
β§ (π β LMod β§ π β π« (Baseβπ)))) β (π£ β π β¦
(0gβ(Scalarβπ))) β ((Baseβ(Scalarβπ)) βm π)) |
24 | | breq1 5150 |
. . . . . . . . . 10
β’ (π = (π£ β π β¦
(0gβ(Scalarβπ))) β (π finSupp
(0gβ(Scalarβπ)) β (π£ β π β¦
(0gβ(Scalarβπ))) finSupp
(0gβ(Scalarβπ)))) |
25 | | oveq1 7412 |
. . . . . . . . . . . 12
β’ (π = (π£ β π β¦
(0gβ(Scalarβπ))) β (π ( linC βπ)π) = ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π)) |
26 | 25 | eqeq2d 2743 |
. . . . . . . . . . 11
β’ (π = (π£ β π β¦
(0gβ(Scalarβπ))) β ((0gβπ) = (π ( linC βπ)π) β (0gβπ) = ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π))) |
27 | | eqcom 2739 |
. . . . . . . . . . 11
β’
((0gβπ) = ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) β ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) = (0gβπ)) |
28 | 26, 27 | bitrdi 286 |
. . . . . . . . . 10
β’ (π = (π£ β π β¦
(0gβ(Scalarβπ))) β ((0gβπ) = (π ( linC βπ)π) β ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) = (0gβπ))) |
29 | 24, 28 | anbi12d 631 |
. . . . . . . . 9
β’ (π = (π£ β π β¦
(0gβ(Scalarβπ))) β ((π finSupp
(0gβ(Scalarβπ)) β§ (0gβπ) = (π ( linC βπ)π)) β ((π£ β π β¦
(0gβ(Scalarβπ))) finSupp
(0gβ(Scalarβπ)) β§ ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) = (0gβπ)))) |
30 | 29 | adantl 482 |
. . . . . . . 8
β’ ((((π£ β π β¦
(0gβ(Scalarβπ))) β ((Baseβ(Scalarβπ)) βm π) β§ (Β¬ π = β
β§ (π β LMod β§ π β π« (Baseβπ)))) β§ π = (π£ β π β¦
(0gβ(Scalarβπ)))) β ((π finSupp
(0gβ(Scalarβπ)) β§ (0gβπ) = (π ( linC βπ)π)) β ((π£ β π β¦
(0gβ(Scalarβπ))) finSupp
(0gβ(Scalarβπ)) β§ ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) = (0gβπ)))) |
31 | 23, 30 | rspcedv 3605 |
. . . . . . 7
β’ (((π£ β π β¦
(0gβ(Scalarβπ))) β ((Baseβ(Scalarβπ)) βm π) β§ (Β¬ π = β
β§ (π β LMod β§ π β π« (Baseβπ)))) β (((π£ β π β¦
(0gβ(Scalarβπ))) finSupp
(0gβ(Scalarβπ)) β§ ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) = (0gβπ)) β βπ β ((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (0gβπ) = (π ( linC βπ)π)))) |
32 | 31 | ex 413 |
. . . . . 6
β’ ((π£ β π β¦
(0gβ(Scalarβπ))) β ((Baseβ(Scalarβπ)) βm π) β ((Β¬ π = β
β§ (π β LMod β§ π β π«
(Baseβπ))) β
(((π£ β π β¦
(0gβ(Scalarβπ))) finSupp
(0gβ(Scalarβπ)) β§ ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) = (0gβπ)) β βπ β ((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (0gβπ) = (π ( linC βπ)π))))) |
33 | 32 | com23 86 |
. . . . 5
β’ ((π£ β π β¦
(0gβ(Scalarβπ))) β ((Baseβ(Scalarβπ)) βm π) β (((π£ β π β¦
(0gβ(Scalarβπ))) finSupp
(0gβ(Scalarβπ)) β§ ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) = (0gβπ)) β ((Β¬ π = β
β§ (π β LMod β§ π β π« (Baseβπ))) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (0gβπ) = (π ( linC βπ)π))))) |
34 | 33 | 3impib 1116 |
. . . 4
β’ (((π£ β π β¦
(0gβ(Scalarβπ))) β ((Baseβ(Scalarβπ)) βm π) β§ (π£ β π β¦
(0gβ(Scalarβπ))) finSupp
(0gβ(Scalarβπ)) β§ ((π£ β π β¦
(0gβ(Scalarβπ)))( linC βπ)π) = (0gβπ)) β ((Β¬ π = β
β§ (π β LMod β§ π β π« (Baseβπ))) β βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (0gβπ) = (π ( linC βπ)π)))) |
35 | 22, 34 | mpcom 38 |
. . 3
β’ ((Β¬
π = β
β§ (π β LMod β§ π β π«
(Baseβπ))) β
βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (0gβπ) = (π ( linC βπ)π))) |
36 | 11, 16, 20 | lcoval 47046 |
. . . 4
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
((0gβπ)
β (π LinCo π) β
((0gβπ)
β (Baseβπ) β§
βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (0gβπ) = (π ( linC βπ)π))))) |
37 | 36 | adantl 482 |
. . 3
β’ ((Β¬
π = β
β§ (π β LMod β§ π β π«
(Baseβπ))) β
((0gβπ)
β (π LinCo π) β
((0gβπ)
β (Baseβπ) β§
βπ β
((Baseβ(Scalarβπ)) βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (0gβπ) = (π ( linC βπ)π))))) |
38 | 15, 35, 37 | mpbir2and 711 |
. 2
β’ ((Β¬
π = β
β§ (π β LMod β§ π β π«
(Baseβπ))) β
(0gβπ)
β (π LinCo π)) |
39 | 10, 38 | pm2.61ian 810 |
1
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(0gβπ)
β (π LinCo π)) |