Metamath Proof Explorer


Theorem lincresunit3

Description: Property 3 of a specially modified restriction of a linear combination in a vector space. (Contributed by AV, 18-May-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Hypotheses lincresunit.b B = Base M
lincresunit.r R = Scalar M
lincresunit.e E = Base R
lincresunit.u U = Unit R
lincresunit.0 0 ˙ = 0 R
lincresunit.z Z = 0 M
lincresunit.n N = inv g R
lincresunit.i I = inv r R
lincresunit.t · ˙ = R
lincresunit.g G = s S X I N F X · ˙ F s
Assertion lincresunit3 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z G linC M S X = X

Proof

Step Hyp Ref Expression
1 lincresunit.b B = Base M
2 lincresunit.r R = Scalar M
3 lincresunit.e E = Base R
4 lincresunit.u U = Unit R
5 lincresunit.0 0 ˙ = 0 R
6 lincresunit.z Z = 0 M
7 lincresunit.n N = inv g R
8 lincresunit.i I = inv r R
9 lincresunit.t · ˙ = R
10 lincresunit.g G = s S X I N F X · ˙ F s
11 simp2 S 𝒫 B M LMod X S M LMod
12 11 3ad2ant1 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z M LMod
13 simp1 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z S 𝒫 B M LMod X S
14 3simpa F E S F X U finSupp 0 ˙ F F E S F X U
15 14 3ad2ant2 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z F E S F X U
16 13 15 jca S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z S 𝒫 B M LMod X S F E S F X U
17 eldifi s S X s S
18 1 2 3 4 5 6 7 8 9 10 lincresunitlem2 S 𝒫 B M LMod X S F E S F X U s S I N F X · ˙ F s E
19 16 17 18 syl2an S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z s S X I N F X · ˙ F s E
20 2 fveq2i Base R = Base Scalar M
21 3 20 eqtri E = Base Scalar M
22 19 21 eleqtrdi S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z s S X I N F X · ˙ F s Base Scalar M
23 22 10 fmptd S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z G : S X Base Scalar M
24 fvex Base Scalar M V
25 difexg S 𝒫 B S X V
26 25 3ad2ant1 S 𝒫 B M LMod X S S X V
27 26 3ad2ant1 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z S X V
28 elmapg Base Scalar M V S X V G Base Scalar M S X G : S X Base Scalar M
29 24 27 28 sylancr S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z G Base Scalar M S X G : S X Base Scalar M
30 23 29 mpbird S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z G Base Scalar M S X
31 difexg S 𝒫 Base M S X V
32 31 adantl X S S 𝒫 Base M S X V
33 ssdifss S Base M S X Base M
34 33 a1i X S S Base M S X Base M
35 elpwi S 𝒫 Base M S Base M
36 34 35 impel X S S 𝒫 Base M S X Base M
37 32 36 elpwd X S S 𝒫 Base M S X 𝒫 Base M
38 37 expcom S 𝒫 Base M X S S X 𝒫 Base M
39 1 pweqi 𝒫 B = 𝒫 Base M
40 38 39 eleq2s S 𝒫 B X S S X 𝒫 Base M
41 40 imp S 𝒫 B X S S X 𝒫 Base M
42 41 3adant2 S 𝒫 B M LMod X S S X 𝒫 Base M
43 42 3ad2ant1 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z S X 𝒫 Base M
44 lincval M LMod G Base Scalar M S X S X 𝒫 Base M G linC M S X = M s S X G s M s
45 12 30 43 44 syl3anc S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z G linC M S X = M s S X G s M s
46 simp1 S 𝒫 B M LMod X S S 𝒫 B
47 simp3 S 𝒫 B M LMod X S X S
48 11 46 47 3jca S 𝒫 B M LMod X S M LMod S 𝒫 B X S
49 48 adantr S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F M LMod S 𝒫 B X S
50 3simpb F E S F X U finSupp 0 ˙ F F E S finSupp 0 ˙ F
51 50 adantl S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F E S finSupp 0 ˙ F
52 eqidd S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F S X = F S X
53 eqid M = M
54 eqid + M = + M
55 1 2 3 53 54 5 lincdifsn M LMod S 𝒫 B X S F E S finSupp 0 ˙ F F S X = F S X F linC M S = F S X linC M S X + M F X M X
56 49 51 52 55 syl3anc S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = F S X linC M S X + M F X M X
57 56 eqeq1d S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z F S X linC M S X + M F X M X = Z
58 fveq2 s = z G s = G z
59 id s = z s = z
60 58 59 oveq12d s = z G s M s = G z M z
61 60 cbvmptv s S X G s M s = z S X G z M z
62 61 a1i S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F s S X G s M s = z S X G z M z
63 62 oveq2d S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F M s S X G s M s = M z S X G z M z
64 63 oveq2d S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F N F X M M s S X G s M s = N F X M M z S X G z M z
65 1 2 3 4 5 6 7 8 9 10 lincresunit3lem2 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F N F X M M z S X G z M z = F S X linC M S X
66 64 65 eqtr2d S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F S X linC M S X = N F X M M s S X G s M s
67 66 oveq1d S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F S X linC M S X + M F X M X = N F X M M s S X G s M s + M F X M X
68 67 eqeq1d S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F S X linC M S X + M F X M X = Z N F X M M s S X G s M s + M F X M X = Z
69 lmodgrp M LMod M Grp
70 69 3ad2ant2 S 𝒫 B M LMod X S M Grp
71 70 adantr S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F M Grp
72 11 adantr S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F M LMod
73 elmapi F E S F : S E
74 73 3ad2ant1 F E S F X U finSupp 0 ˙ F F : S E
75 ffvelrn F : S E X S F X E
76 74 47 75 syl2anr S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F X E
77 elpwi S 𝒫 B S B
78 77 sselda S 𝒫 B X S X B
79 78 3adant2 S 𝒫 B M LMod X S X B
80 79 adantr S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F X B
81 1 2 53 3 lmodvscl M LMod F X E X B F X M X B
82 72 76 80 81 syl3anc S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F X M X B
83 2 lmodfgrp M LMod R Grp
84 83 3ad2ant2 S 𝒫 B M LMod X S R Grp
85 3 7 grpinvcl R Grp F X E N F X E
86 84 76 85 syl2an2r S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F N F X E
87 lmodcmn M LMod M CMnd
88 87 3ad2ant2 S 𝒫 B M LMod X S M CMnd
89 88 adantr S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F M CMnd
90 26 adantr S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F S X V
91 simpll2 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F s S X M LMod
92 1 2 3 4 5 6 7 8 9 10 lincresunit1 S 𝒫 B M LMod X S F E S F X U G E S X
93 92 3adantr3 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F G E S X
94 elmapi G E S X G : S X E
95 93 94 syl S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F G : S X E
96 95 ffvelrnda S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F s S X G s E
97 ssel2 S B s S s B
98 97 expcom s S S B s B
99 17 77 98 syl2imc S 𝒫 B s S X s B
100 99 3ad2ant1 S 𝒫 B M LMod X S s S X s B
101 100 adantr S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F s S X s B
102 101 imp S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F s S X s B
103 1 2 53 3 lmodvscl M LMod G s E s B G s M s B
104 91 96 102 103 syl3anc S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F s S X G s M s B
105 104 fmpttd S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F s S X G s M s : S X B
106 25 adantr S 𝒫 B X S S X V
107 ssdifss S B S X B
108 77 107 syl S 𝒫 B S X B
109 108 adantr S 𝒫 B X S S X B
110 109 1 sseqtrdi S 𝒫 B X S S X Base M
111 106 110 elpwd S 𝒫 B X S S X 𝒫 Base M
112 111 3adant2 S 𝒫 B M LMod X S S X 𝒫 Base M
113 11 112 jca S 𝒫 B M LMod X S M LMod S X 𝒫 Base M
114 113 adantr S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F M LMod S X 𝒫 Base M
115 1 2 3 4 5 6 7 8 9 10 lincresunit2 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F finSupp 0 ˙ G
116 115 5 breqtrdi S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F finSupp 0 R G
117 2 3 scmfsupp M LMod S X 𝒫 Base M G E S X finSupp 0 R G finSupp 0 M s S X G s M s
118 114 93 116 117 syl3anc S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F finSupp 0 M s S X G s M s
119 118 6 breqtrrdi S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F finSupp Z s S X G s M s
120 1 6 89 90 105 119 gsumcl S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F M s S X G s M s B
121 1 2 53 3 lmodvscl M LMod N F X E M s S X G s M s B N F X M M s S X G s M s B
122 72 86 120 121 syl3anc S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F N F X M M s S X G s M s B
123 eqid inv g M = inv g M
124 1 54 6 123 grpinvid2 M Grp F X M X B N F X M M s S X G s M s B inv g M F X M X = N F X M M s S X G s M s N F X M M s S X G s M s + M F X M X = Z
125 71 82 122 124 syl3anc S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F inv g M F X M X = N F X M M s S X G s M s N F X M M s S X G s M s + M F X M X = Z
126 1 2 53 123 3 7 72 80 76 lmodvsneg S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F inv g M F X M X = N F X M X
127 126 eqeq1d S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F inv g M F X M X = N F X M M s S X G s M s N F X M X = N F X M M s S X G s M s
128 simpr2 S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F X U
129 1 2 3 4 7 53 lincresunit3lem3 M LMod X B M s S X G s M s B F X U N F X M X = N F X M M s S X G s M s X = M s S X G s M s
130 eqcom X = M s S X G s M s M s S X G s M s = X
131 129 130 bitrdi M LMod X B M s S X G s M s B F X U N F X M X = N F X M M s S X G s M s M s S X G s M s = X
132 72 80 120 128 131 syl31anc S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F N F X M X = N F X M M s S X G s M s M s S X G s M s = X
133 132 biimpd S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F N F X M X = N F X M M s S X G s M s M s S X G s M s = X
134 127 133 sylbid S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F inv g M F X M X = N F X M M s S X G s M s M s S X G s M s = X
135 125 134 sylbird S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F N F X M M s S X G s M s + M F X M X = Z M s S X G s M s = X
136 68 135 sylbid S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F S X linC M S X + M F X M X = Z M s S X G s M s = X
137 57 136 sylbid S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z M s S X G s M s = X
138 137 3impia S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z M s S X G s M s = X
139 45 138 eqtrd S 𝒫 B M LMod X S F E S F X U finSupp 0 ˙ F F linC M S = Z G linC M S X = X