Step | Hyp | Ref
| Expression |
1 | | 3simpa 1149 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅ β§ π β π) β (π β π΅ β§ π β π΅)) |
2 | 1 | ad2antlr 726 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (π β π΅ β§ π β π΅)) |
3 | | fvex 6905 |
. . . . . . . 8
β’
(1rβπ
) β V |
4 | | fvex 6905 |
. . . . . . . 8
β’
((invgβπ
)βπ΄) β V |
5 | 3, 4 | pm3.2i 472 |
. . . . . . 7
β’
((1rβπ
) β V β§
((invgβπ
)βπ΄) β V) |
6 | 5 | a1i 11 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ((1rβπ
) β V β§
((invgβπ
)βπ΄) β V)) |
7 | | simp3 1139 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅ β§ π β π) β π β π) |
8 | 7 | ad2antlr 726 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β π β π) |
9 | | fprg 7153 |
. . . . . 6
β’ (((π β π΅ β§ π β π΅) β§ ((1rβπ
) β V β§
((invgβπ
)βπ΄) β V) β§ π β π) β {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}:{π, π}βΆ{(1rβπ
), ((invgβπ
)βπ΄)}) |
10 | 2, 6, 8, 9 | syl3anc 1372 |
. . . . 5
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}:{π, π}βΆ{(1rβπ
), ((invgβπ
)βπ΄)}) |
11 | | prfi 9322 |
. . . . . 6
β’ {π, π} β Fin |
12 | 11 | a1i 11 |
. . . . 5
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β {π, π} β Fin) |
13 | | snlindsntor.0 |
. . . . . . 7
β’ 0 =
(0gβπ
) |
14 | 13 | fvexi 6906 |
. . . . . 6
β’ 0 β
V |
15 | 14 | a1i 11 |
. . . . 5
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β 0 β V) |
16 | 10, 12, 15 | fdmfifsupp 9373 |
. . . 4
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} finSupp 0 ) |
17 | 7 | anim2i 618 |
. . . . . . 7
β’ ((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β (π β LMod β§ π β π)) |
18 | 17 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (π β LMod β§ π β π)) |
19 | | snlindsntor.r |
. . . . . . . . 9
β’ π
= (Scalarβπ) |
20 | | snlindsntor.s |
. . . . . . . . 9
β’ π = (Baseβπ
) |
21 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπ
) = (1rβπ
) |
22 | 19, 20, 21 | lmod1cl 20499 |
. . . . . . . 8
β’ (π β LMod β
(1rβπ
)
β π) |
23 | | simp1 1137 |
. . . . . . . 8
β’ ((π β π΅ β§ π β π΅ β§ π β π) β π β π΅) |
24 | 22, 23 | anim12ci 615 |
. . . . . . 7
β’ ((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β (π β π΅ β§ (1rβπ
) β π)) |
25 | 24 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (π β π΅ β§ (1rβπ
) β π)) |
26 | | simp2 1138 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅ β§ π β π) β π β π΅) |
27 | 26 | ad2antlr 726 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β π β π΅) |
28 | 19 | lmodfgrp 20480 |
. . . . . . . 8
β’ (π β LMod β π
β Grp) |
29 | 28 | adantr 482 |
. . . . . . 7
β’ ((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β π
β Grp) |
30 | | simpl 484 |
. . . . . . 7
β’ ((π΄ β π β§ π = (π΄ Β· π)) β π΄ β π) |
31 | | eqid 2733 |
. . . . . . . 8
β’
(invgβπ
) = (invgβπ
) |
32 | 20, 31 | grpinvcl 18872 |
. . . . . . 7
β’ ((π
β Grp β§ π΄ β π) β ((invgβπ
)βπ΄) β π) |
33 | 29, 30, 32 | syl2an 597 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ((invgβπ
)βπ΄) β π) |
34 | | snlindsntor.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
35 | | snlindsntor.t |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
36 | | eqid 2733 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
37 | | eqid 2733 |
. . . . . . 7
β’
{β¨π,
(1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} = {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} |
38 | 34, 19, 20, 35, 36, 37 | lincvalpr 47099 |
. . . . . 6
β’ (((π β LMod β§ π β π) β§ (π β π΅ β§ (1rβπ
) β π) β§ (π β π΅ β§ ((invgβπ
)βπ΄) β π)) β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} ( linC βπ){π, π}) = (((1rβπ
) Β· π)(+gβπ)(((invgβπ
)βπ΄) Β· π))) |
39 | 18, 25, 27, 33, 38 | syl112anc 1375 |
. . . . 5
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} ( linC βπ){π, π}) = (((1rβπ
) Β· π)(+gβπ)(((invgβπ
)βπ΄) Β· π))) |
40 | | simpll 766 |
. . . . . . 7
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β π β LMod) |
41 | 23 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β π β π΅) |
42 | 30 | adantl 483 |
. . . . . . . 8
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β π΄ β π) |
43 | 41, 27, 42 | 3jca 1129 |
. . . . . . 7
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (π β π΅ β§ π β π΅ β§ π΄ β π)) |
44 | 40, 43 | jca 513 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (π β LMod β§ (π β π΅ β§ π β π΅ β§ π΄ β π))) |
45 | | simprr 772 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β π = (π΄ Β· π)) |
46 | | snlindsntor.z |
. . . . . . 7
β’ π = (0gβπ) |
47 | 34, 19, 20, 13, 46, 35, 21, 31 | ldepsprlem 47153 |
. . . . . 6
β’ ((π β LMod β§ (π β π΅ β§ π β π΅ β§ π΄ β π)) β (π = (π΄ Β· π) β (((1rβπ
) Β· π)(+gβπ)(((invgβπ
)βπ΄) Β· π)) = π)) |
48 | 44, 45, 47 | sylc 65 |
. . . . 5
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (((1rβπ
) Β· π)(+gβπ)(((invgβπ
)βπ΄) Β· π)) = π) |
49 | 39, 48 | eqtrd 2773 |
. . . 4
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} ( linC βπ){π, π}) = π) |
50 | 19 | lmodring 20479 |
. . . . . . . . . 10
β’ (π β LMod β π
β Ring) |
51 | | eqcom 2740 |
. . . . . . . . . . . 12
β’
((1rβπ
) = (0gβπ
) β (0gβπ
) = (1rβπ
)) |
52 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(0gβπ
) = (0gβπ
) |
53 | 20, 52, 21 | 01eq0ring 20305 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§
(0gβπ
) =
(1rβπ
))
β π =
{(0gβπ
)}) |
54 | | sneq 4639 |
. . . . . . . . . . . . . . . . 17
β’
((0gβπ
) = (1rβπ
) β {(0gβπ
)} = {(1rβπ
)}) |
55 | 54 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’
((0gβπ
) = (1rβπ
) β (π = {(0gβπ
)} β π = {(1rβπ
)})) |
56 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = {(1rβπ
)} β (π΄ β π β π΄ β {(1rβπ
)})) |
57 | | elsni 4646 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ β
{(1rβπ
)}
β π΄ =
(1rβπ
)) |
58 | | oveq1 7416 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ = (1rβπ
) β (π΄ Β· π) = ((1rβπ
) Β· π)) |
59 | 58 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄ = (1rβπ
) β (π = (π΄ Β· π) β π = ((1rβπ
) Β· π))) |
60 | 26 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β π΅ β§ π β π΅ β§ π β π) β§ π β LMod) β (π β π΅ β§ π β LMod)) |
61 | 60 | ancomd 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β π΅ β§ π β π΅ β§ π β π) β§ π β LMod) β (π β LMod β§ π β π΅)) |
62 | 34, 19, 35, 21 | lmodvs1 20500 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β LMod β§ π β π΅) β ((1rβπ
) Β· π) = π) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β π΅ β§ π β π΅ β§ π β π) β§ π β LMod) β
((1rβπ
)
Β·
π) = π) |
64 | 63 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β π΅ β§ π β π΅ β§ π β π) β§ π β LMod) β (π = ((1rβπ
) Β· π) β π = π)) |
65 | | eqneqall 2952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β (π β π β (Β¬ (1rβπ
) = (0gβπ
) β¨
((invgβπ
)βπ΄) β 0 ))) |
66 | 65 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β (π = π β (Β¬ (1rβπ
) = (0gβπ
) β¨
((invgβπ
)βπ΄) β 0 ))) |
67 | 66 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π΅ β§ π β π΅ β§ π β π) β (π = π β (Β¬ (1rβπ
) = (0gβπ
) β¨
((invgβπ
)βπ΄) β 0 ))) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β π΅ β§ π β π΅ β§ π β π) β§ π β LMod) β (π = π β (Β¬ (1rβπ
) = (0gβπ
) β¨
((invgβπ
)βπ΄) β 0 ))) |
69 | 64, 68 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β π΅ β§ π β π΅ β§ π β π) β§ π β LMod) β (π = ((1rβπ
) Β· π) β (Β¬ (1rβπ
) = (0gβπ
) β¨
((invgβπ
)βπ΄) β 0 ))) |
70 | 69 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β π΅ β§ π β π΅ β§ π β π) β (π β LMod β (π = ((1rβπ
) Β· π) β (Β¬ (1rβπ
) = (0gβπ
) β¨
((invgβπ
)βπ΄) β 0 )))) |
71 | 70 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = ((1rβπ
) Β· π) β ((π β π΅ β§ π β π΅ β§ π β π) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 )))) |
72 | 59, 71 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΄ = (1rβπ
) β (π = (π΄ Β· π) β ((π β π΅ β§ π β π΅ β§ π β π) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 ))))) |
73 | 57, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β
{(1rβπ
)}
β (π = (π΄ Β· π) β ((π β π΅ β§ π β π΅ β§ π β π) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 ))))) |
74 | 56, 73 | syl6bi 253 |
. . . . . . . . . . . . . . . . . 18
β’ (π = {(1rβπ
)} β (π΄ β π β (π = (π΄ Β· π) β ((π β π΅ β§ π β π΅ β§ π β π) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 )))))) |
75 | 74 | impd 412 |
. . . . . . . . . . . . . . . . 17
β’ (π = {(1rβπ
)} β ((π΄ β π β§ π = (π΄ Β· π)) β ((π β π΅ β§ π β π΅ β§ π β π) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 ))))) |
76 | 75 | com23 86 |
. . . . . . . . . . . . . . . 16
β’ (π = {(1rβπ
)} β ((π β π΅ β§ π β π΅ β§ π β π) β ((π΄ β π β§ π = (π΄ Β· π)) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 ))))) |
77 | 55, 76 | syl6bi 253 |
. . . . . . . . . . . . . . 15
β’
((0gβπ
) = (1rβπ
) β (π = {(0gβπ
)} β ((π β π΅ β§ π β π΅ β§ π β π) β ((π΄ β π β§ π = (π΄ Β· π)) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 )))))) |
78 | 77 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§
(0gβπ
) =
(1rβπ
))
β (π =
{(0gβπ
)}
β ((π β π΅ β§ π β π΅ β§ π β π) β ((π΄ β π β§ π = (π΄ Β· π)) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 )))))) |
79 | 53, 78 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§
(0gβπ
) =
(1rβπ
))
β ((π β π΅ β§ π β π΅ β§ π β π) β ((π΄ β π β§ π = (π΄ Β· π)) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 ))))) |
80 | 79 | ex 414 |
. . . . . . . . . . . 12
β’ (π
β Ring β
((0gβπ
) =
(1rβπ
)
β ((π β π΅ β§ π β π΅ β§ π β π) β ((π΄ β π β§ π = (π΄ Β· π)) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 )))))) |
81 | 51, 80 | biimtrid 241 |
. . . . . . . . . . 11
β’ (π
β Ring β
((1rβπ
) =
(0gβπ
)
β ((π β π΅ β§ π β π΅ β§ π β π) β ((π΄ β π β§ π = (π΄ Β· π)) β (π β LMod β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 )))))) |
82 | 81 | com25 99 |
. . . . . . . . . 10
β’ (π
β Ring β (π β LMod β ((π β π΅ β§ π β π΅ β§ π β π) β ((π΄ β π β§ π = (π΄ Β· π)) β ((1rβπ
) = (0gβπ
) β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 )))))) |
83 | 50, 82 | mpcom 38 |
. . . . . . . . 9
β’ (π β LMod β ((π β π΅ β§ π β π΅ β§ π β π) β ((π΄ β π β§ π = (π΄ Β· π)) β ((1rβπ
) = (0gβπ
) β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 ))))) |
84 | 83 | imp31 419 |
. . . . . . . 8
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ((1rβπ
) = (0gβπ
) β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 ))) |
85 | | orc 866 |
. . . . . . . 8
β’ (Β¬
(1rβπ
) =
(0gβπ
)
β (Β¬ (1rβπ
) = (0gβπ
) β¨ ((invgβπ
)βπ΄) β 0 )) |
86 | 84, 85 | pm2.61d1 180 |
. . . . . . 7
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (Β¬ (1rβπ
) = (0gβπ
) β¨
((invgβπ
)βπ΄) β 0 )) |
87 | 13 | eqeq2i 2746 |
. . . . . . . . 9
β’
((1rβπ
) = 0 β
(1rβπ
) =
(0gβπ
)) |
88 | 87 | necon3abii 2988 |
. . . . . . . 8
β’
((1rβπ
) β 0 β Β¬
(1rβπ
) =
(0gβπ
)) |
89 | 88 | orbi1i 913 |
. . . . . . 7
β’
(((1rβπ
) β 0 β¨
((invgβπ
)βπ΄) β 0 ) β (Β¬
(1rβπ
) =
(0gβπ
)
β¨ ((invgβπ
)βπ΄) β 0 )) |
90 | 86, 89 | sylibr 233 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ((1rβπ
) β 0 β¨
((invgβπ
)βπ΄) β 0 )) |
91 | | fvexd 6907 |
. . . . . . . . 9
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (1rβπ
) β V) |
92 | | fvpr1g 7188 |
. . . . . . . . 9
β’ ((π β π΅ β§ (1rβπ
) β V β§ π β π) β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) = (1rβπ
)) |
93 | 41, 91, 8, 92 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) = (1rβπ
)) |
94 | 93 | neeq1d 3001 |
. . . . . . 7
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 β
(1rβπ
)
β 0
)) |
95 | | fvexd 6907 |
. . . . . . . . 9
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ((invgβπ
)βπ΄) β V) |
96 | | fvpr2g 7189 |
. . . . . . . . 9
β’ ((π β π΅ β§ ((invgβπ
)βπ΄) β V β§ π β π) β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) = ((invgβπ
)βπ΄)) |
97 | 27, 95, 8, 96 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) = ((invgβπ
)βπ΄)) |
98 | 97 | neeq1d 3001 |
. . . . . . 7
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 β
((invgβπ
)βπ΄) β 0 )) |
99 | 94, 98 | orbi12d 918 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ((({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 β¨ ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 ) β
((1rβπ
)
β 0
β¨ ((invgβπ
)βπ΄) β 0 ))) |
100 | 90, 99 | mpbird 257 |
. . . . 5
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 β¨ ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 )) |
101 | | fveq2 6892 |
. . . . . . . 8
β’ (π£ = π β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) = ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ)) |
102 | 101 | neeq1d 3001 |
. . . . . . 7
β’ (π£ = π β (({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) β 0 β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 )) |
103 | | fveq2 6892 |
. . . . . . . 8
β’ (π£ = π β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) = ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ)) |
104 | 103 | neeq1d 3001 |
. . . . . . 7
β’ (π£ = π β (({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) β 0 β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 )) |
105 | 102, 104 | rexprg 4701 |
. . . . . 6
β’ ((π β π΅ β§ π β π΅) β (βπ£ β {π, π} ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) β 0 β (({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 β¨ ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 ))) |
106 | 2, 105 | syl 17 |
. . . . 5
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (βπ£ β {π, π} ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) β 0 β (({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 β¨ ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ) β 0 ))) |
107 | 100, 106 | mpbird 257 |
. . . 4
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β βπ£ β {π, π} ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) β 0 ) |
108 | 22 | adantr 482 |
. . . . . . 7
β’ ((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β (1rβπ
) β π) |
109 | 108 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (1rβπ
) β π) |
110 | 20 | fvexi 6906 |
. . . . . . 7
β’ π β V |
111 | 8, 110 | jctir 522 |
. . . . . 6
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (π β π β§ π β V)) |
112 | 37 | mapprop 47022 |
. . . . . 6
β’ (((π β π΅ β§ (1rβπ
) β π) β§ (π β π΅ β§ ((invgβπ
)βπ΄) β π) β§ (π β π β§ π β V)) β {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} β (π βm {π, π})) |
113 | 41, 109, 27, 33, 111, 112 | syl221anc 1382 |
. . . . 5
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} β (π βm {π, π})) |
114 | | breq1 5152 |
. . . . . . 7
β’ (π = {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} β (π finSupp 0 β {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} finSupp 0 )) |
115 | | oveq1 7416 |
. . . . . . . 8
β’ (π = {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} β (π( linC βπ){π, π}) = ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} ( linC βπ){π, π})) |
116 | 115 | eqeq1d 2735 |
. . . . . . 7
β’ (π = {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} β ((π( linC βπ){π, π}) = π β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} ( linC βπ){π, π}) = π)) |
117 | | fveq1 6891 |
. . . . . . . . 9
β’ (π = {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} β (πβπ£) = ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£)) |
118 | 117 | neeq1d 3001 |
. . . . . . . 8
β’ (π = {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} β ((πβπ£) β 0 β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) β 0 )) |
119 | 118 | rexbidv 3179 |
. . . . . . 7
β’ (π = {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} β (βπ£ β {π, π} (πβπ£) β 0 β βπ£ β {π, π} ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) β 0 )) |
120 | 114, 116,
119 | 3anbi123d 1437 |
. . . . . 6
β’ (π = {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} β ((π finSupp 0 β§ (π( linC βπ){π, π}) = π β§ βπ£ β {π, π} (πβπ£) β 0 ) β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} finSupp 0 β§ ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} ( linC βπ){π, π}) = π β§ βπ£ β {π, π} ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) β 0 ))) |
121 | 120 | adantl 483 |
. . . . 5
β’ ((((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β§ π = {β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}) β ((π finSupp 0 β§ (π( linC βπ){π, π}) = π β§ βπ£ β {π, π} (πβπ£) β 0 ) β ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} finSupp 0 β§ ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} ( linC βπ){π, π}) = π β§ βπ£ β {π, π} ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) β 0 ))) |
122 | 113, 121 | rspcedv 3606 |
. . . 4
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β (({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} finSupp 0 β§ ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©} ( linC βπ){π, π}) = π β§ βπ£ β {π, π} ({β¨π, (1rβπ
)β©, β¨π, ((invgβπ
)βπ΄)β©}βπ£) β 0 ) β βπ β (π βm {π, π})(π finSupp 0 β§ (π( linC βπ){π, π}) = π β§ βπ£ β {π, π} (πβπ£) β 0 ))) |
123 | 16, 49, 107, 122 | mp3and 1465 |
. . 3
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β βπ β (π βm {π, π})(π finSupp 0 β§ (π( linC βπ){π, π}) = π β§ βπ£ β {π, π} (πβπ£) β 0 )) |
124 | | prelpwi 5448 |
. . . . . 6
β’ ((π β π΅ β§ π β π΅) β {π, π} β π« π΅) |
125 | 124 | 3adant3 1133 |
. . . . 5
β’ ((π β π΅ β§ π β π΅ β§ π β π) β {π, π} β π« π΅) |
126 | 125 | ad2antlr 726 |
. . . 4
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β {π, π} β π« π΅) |
127 | 34, 46, 19, 20, 13 | islindeps 47134 |
. . . 4
β’ ((π β LMod β§ {π, π} β π« π΅) β ({π, π} linDepS π β βπ β (π βm {π, π})(π finSupp 0 β§ (π( linC βπ){π, π}) = π β§ βπ£ β {π, π} (πβπ£) β 0 ))) |
128 | 40, 126, 127 | syl2anc 585 |
. . 3
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β ({π, π} linDepS π β βπ β (π βm {π, π})(π finSupp 0 β§ (π( linC βπ){π, π}) = π β§ βπ£ β {π, π} (πβπ£) β 0 ))) |
129 | 123, 128 | mpbird 257 |
. 2
β’ (((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π΄ β π β§ π = (π΄ Β· π))) β {π, π} linDepS π) |
130 | 129 | ex 414 |
1
β’ ((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π΄ β π β§ π = (π΄ Β· π)) β {π, π} linDepS π)) |