Metamath Proof Explorer


Theorem islindf4

Description: A family is independent iff it has no nontrivial representations of zero. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Hypotheses islindf4.b B = Base W
islindf4.r R = Scalar W
islindf4.t · ˙ = W
islindf4.z 0 ˙ = 0 W
islindf4.y Y = 0 R
islindf4.l L = Base R freeLMod I
Assertion islindf4 W LMod I X F : I B F LIndF W x L W x · ˙ f F = 0 ˙ x = I × Y

Proof

Step Hyp Ref Expression
1 islindf4.b B = Base W
2 islindf4.r R = Scalar W
3 islindf4.t · ˙ = W
4 islindf4.z 0 ˙ = 0 W
5 islindf4.y Y = 0 R
6 islindf4.l L = Base R freeLMod I
7 raldifsni l Base R Y ¬ inv g R l · ˙ F j LSpan W F I j l Base R inv g R l · ˙ F j LSpan W F I j l = Y
8 simpll1 W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W LMod
9 simprll W LMod I X F : I B j I l Base R y Base R I j finSupp Y y l Base R
10 ffvelrn F : I B j I F j B
11 10 3ad2antl3 W LMod I X F : I B j I F j B
12 11 adantr W LMod I X F : I B j I l Base R y Base R I j finSupp Y y F j B
13 eqid inv g W = inv g W
14 eqid inv g R = inv g R
15 eqid Base R = Base R
16 1 2 3 13 14 15 lmodvsinv W LMod l Base R F j B inv g R l · ˙ F j = inv g W l · ˙ F j
17 8 9 12 16 syl3anc W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = inv g W l · ˙ F j
18 17 eqeq1d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j inv g W l · ˙ F j = W y · ˙ f F I j
19 lmodgrp W LMod W Grp
20 8 19 syl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W Grp
21 1 2 3 15 lmodvscl W LMod l Base R F j B l · ˙ F j B
22 8 9 12 21 syl3anc W LMod I X F : I B j I l Base R y Base R I j finSupp Y y l · ˙ F j B
23 lmodcmn W LMod W CMnd
24 8 23 syl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W CMnd
25 simpll2 W LMod I X F : I B j I l Base R y Base R I j finSupp Y y I X
26 difexg I X I j V
27 25 26 syl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y I j V
28 simprlr W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y Base R I j
29 elmapi y Base R I j y : I j Base R
30 28 29 syl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y : I j Base R
31 simpll3 W LMod I X F : I B j I l Base R y Base R I j finSupp Y y F : I B
32 difss I j I
33 fssres F : I B I j I F I j : I j B
34 31 32 33 sylancl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y F I j : I j B
35 2 15 3 1 8 30 34 27 lcomf W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y · ˙ f F I j : I j B
36 simprr W LMod I X F : I B j I l Base R y Base R I j finSupp Y y finSupp Y y
37 2 15 3 1 8 30 34 27 4 5 36 lcomfsupp W LMod I X F : I B j I l Base R y Base R I j finSupp Y y finSupp 0 ˙ y · ˙ f F I j
38 1 4 24 27 35 37 gsumcl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W y · ˙ f F I j B
39 eqid + W = + W
40 1 39 4 13 grpinvid2 W Grp l · ˙ F j B W y · ˙ f F I j B inv g W l · ˙ F j = W y · ˙ f F I j W y · ˙ f F I j + W l · ˙ F j = 0 ˙
41 20 22 38 40 syl3anc W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g W l · ˙ F j = W y · ˙ f F I j W y · ˙ f F I j + W l · ˙ F j = 0 ˙
42 simplr W LMod I X F : I B j I l Base R y Base R I j finSupp Y y j I
43 fsnunf2 y : I j Base R j I l Base R y j l : I Base R
44 30 42 9 43 syl3anc W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l : I Base R
45 2 15 3 1 8 44 31 25 lcomf W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l · ˙ f F : I B
46 simpr W LMod I X F : I B j I j I
47 simpl l Base R y Base R I j l Base R
48 46 47 anim12i W LMod I X F : I B j I l Base R y Base R I j j I l Base R
49 elmapfun y Base R I j Fun y
50 fdm y : I j Base R dom y = I j
51 neldifsnd dom y = I j ¬ j I j
52 df-nel j dom y ¬ j dom y
53 eleq2 dom y = I j j dom y j I j
54 53 notbid dom y = I j ¬ j dom y ¬ j I j
55 52 54 syl5bb dom y = I j j dom y ¬ j I j
56 51 55 mpbird dom y = I j j dom y
57 29 50 56 3syl y Base R I j j dom y
58 49 57 jca y Base R I j Fun y j dom y
59 58 adantl l Base R y Base R I j Fun y j dom y
60 59 adantl W LMod I X F : I B j I l Base R y Base R I j Fun y j dom y
61 48 60 jca W LMod I X F : I B j I l Base R y Base R I j j I l Base R Fun y j dom y
62 funsnfsupp j I l Base R Fun y j dom y finSupp Y y j l finSupp Y y
63 62 bicomd j I l Base R Fun y j dom y finSupp Y y finSupp Y y j l
64 61 63 syl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y finSupp Y y j l
65 64 biimpd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y finSupp Y y j l
66 65 impr W LMod I X F : I B j I l Base R y Base R I j finSupp Y y finSupp Y y j l
67 2 15 3 1 8 44 31 25 4 5 66 lcomfsupp W LMod I X F : I B j I l Base R y Base R I j finSupp Y y finSupp 0 ˙ y j l · ˙ f F
68 incom I j j = j I j
69 disjdif j I j =
70 68 69 eqtri I j j =
71 70 a1i W LMod I X F : I B j I l Base R y Base R I j finSupp Y y I j j =
72 difsnid j I I j j = I
73 72 eqcomd j I I = I j j
74 42 73 syl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y I = I j j
75 1 4 39 24 25 45 67 71 74 gsumsplit W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W y j l · ˙ f F = W y j l · ˙ f F I j + W W y j l · ˙ f F j
76 vex y V
77 snex j l V
78 76 77 unex y j l V
79 simpl3 W LMod I X F : I B j I F : I B
80 simpl2 W LMod I X F : I B j I I X
81 fex F : I B I X F V
82 79 80 81 syl2anc W LMod I X F : I B j I F V
83 82 adantr W LMod I X F : I B j I l Base R y Base R I j finSupp Y y F V
84 offres y j l V F V y j l · ˙ f F I j = y j l I j · ˙ f F I j
85 78 83 84 sylancr W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l · ˙ f F I j = y j l I j · ˙ f F I j
86 30 ffnd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y Fn I j
87 neldifsn ¬ j I j
88 fsnunres y Fn I j ¬ j I j y j l I j = y
89 86 87 88 sylancl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l I j = y
90 89 oveq1d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l I j · ˙ f F I j = y · ˙ f F I j
91 85 90 eqtrd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l · ˙ f F I j = y · ˙ f F I j
92 91 oveq2d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W y j l · ˙ f F I j = W y · ˙ f F I j
93 45 ffnd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l · ˙ f F Fn I
94 fnressn y j l · ˙ f F Fn I j I y j l · ˙ f F j = j y j l · ˙ f F j
95 93 42 94 syl2anc W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l · ˙ f F j = j y j l · ˙ f F j
96 44 ffnd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l Fn I
97 31 ffnd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y F Fn I
98 fnfvof y j l Fn I F Fn I I X j I y j l · ˙ f F j = y j l j · ˙ F j
99 96 97 25 42 98 syl22anc W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l · ˙ f F j = y j l j · ˙ F j
100 fndm y Fn I j dom y = I j
101 100 eleq2d y Fn I j j dom y j I j
102 87 101 mtbiri y Fn I j ¬ j dom y
103 vex j V
104 vex l V
105 fsnunfv j V l V ¬ j dom y y j l j = l
106 103 104 105 mp3an12 ¬ j dom y y j l j = l
107 86 102 106 3syl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l j = l
108 107 oveq1d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l j · ˙ F j = l · ˙ F j
109 99 108 eqtrd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l · ˙ f F j = l · ˙ F j
110 109 opeq2d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y j y j l · ˙ f F j = j l · ˙ F j
111 110 sneqd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y j y j l · ˙ f F j = j l · ˙ F j
112 ovex l · ˙ F j V
113 fmptsn j V l · ˙ F j V j l · ˙ F j = x j l · ˙ F j
114 103 112 113 mp2an j l · ˙ F j = x j l · ˙ F j
115 114 a1i W LMod I X F : I B j I l Base R y Base R I j finSupp Y y j l · ˙ F j = x j l · ˙ F j
116 95 111 115 3eqtrd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y y j l · ˙ f F j = x j l · ˙ F j
117 116 oveq2d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W y j l · ˙ f F j = W x j l · ˙ F j
118 cmnmnd W CMnd W Mnd
119 8 23 118 3syl W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W Mnd
120 103 a1i W LMod I X F : I B j I l Base R y Base R I j finSupp Y y j V
121 eqidd x = j l · ˙ F j = l · ˙ F j
122 1 121 gsumsn W Mnd j V l · ˙ F j B W x j l · ˙ F j = l · ˙ F j
123 119 120 22 122 syl3anc W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W x j l · ˙ F j = l · ˙ F j
124 117 123 eqtrd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W y j l · ˙ f F j = l · ˙ F j
125 92 124 oveq12d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W y j l · ˙ f F I j + W W y j l · ˙ f F j = W y · ˙ f F I j + W l · ˙ F j
126 75 125 eqtr2d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W y · ˙ f F I j + W l · ˙ F j = W y j l · ˙ f F
127 126 eqeq1d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y W y · ˙ f F I j + W l · ˙ F j = 0 ˙ W y j l · ˙ f F = 0 ˙
128 18 41 127 3bitrd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j W y j l · ˙ f F = 0 ˙
129 107 eqcomd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y l = y j l j
130 129 eqeq1d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y l = Y y j l j = Y
131 128 130 imbi12d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y W y j l · ˙ f F = 0 ˙ y j l j = Y
132 131 anassrs W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y W y j l · ˙ f F = 0 ˙ y j l j = Y
133 132 pm5.74da W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y finSupp Y y W y j l · ˙ f F = 0 ˙ y j l j = Y
134 impexp finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y
135 134 a1i W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y
136 64 bicomd W LMod I X F : I B j I l Base R y Base R I j finSupp Y y j l finSupp Y y
137 136 imbi1d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y j l W y j l · ˙ f F = 0 ˙ y j l j = Y finSupp Y y W y j l · ˙ f F = 0 ˙ y j l j = Y
138 133 135 137 3bitr4d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y finSupp Y y j l W y j l · ˙ f F = 0 ˙ y j l j = Y
139 138 2ralbidva W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y l Base R y Base R I j finSupp Y y j l W y j l · ˙ f F = 0 ˙ y j l j = Y
140 breq1 x = y j l finSupp Y x finSupp Y y j l
141 oveq1 x = y j l x · ˙ f F = y j l · ˙ f F
142 141 oveq2d x = y j l W x · ˙ f F = W y j l · ˙ f F
143 142 eqeq1d x = y j l W x · ˙ f F = 0 ˙ W y j l · ˙ f F = 0 ˙
144 fveq1 x = y j l x j = y j l j
145 144 eqeq1d x = y j l x j = Y y j l j = Y
146 143 145 imbi12d x = y j l W x · ˙ f F = 0 ˙ x j = Y W y j l · ˙ f F = 0 ˙ y j l j = Y
147 140 146 imbi12d x = y j l finSupp Y x W x · ˙ f F = 0 ˙ x j = Y finSupp Y y j l W y j l · ˙ f F = 0 ˙ y j l j = Y
148 147 ralxpmap j I x Base R I finSupp Y x W x · ˙ f F = 0 ˙ x j = Y l Base R y Base R I j finSupp Y y j l W y j l · ˙ f F = 0 ˙ y j l j = Y
149 148 adantl W LMod I X F : I B j I x Base R I finSupp Y x W x · ˙ f F = 0 ˙ x j = Y l Base R y Base R I j finSupp Y y j l W y j l · ˙ f F = 0 ˙ y j l j = Y
150 139 149 bitr4d W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y x Base R I finSupp Y x W x · ˙ f F = 0 ˙ x j = Y
151 breq1 z = x finSupp Y z finSupp Y x
152 151 ralrab x z Base R I | finSupp Y z W x · ˙ f F = 0 ˙ x j = Y x Base R I finSupp Y x W x · ˙ f F = 0 ˙ x j = Y
153 150 152 syl6bbr W LMod I X F : I B j I l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y x z Base R I | finSupp Y z W x · ˙ f F = 0 ˙ x j = Y
154 resima F I j I j = F I j
155 154 eqcomi F I j = F I j I j
156 155 fveq2i LSpan W F I j = LSpan W F I j I j
157 156 eleq2i inv g R l · ˙ F j LSpan W F I j inv g R l · ˙ F j LSpan W F I j I j
158 eqid LSpan W = LSpan W
159 79 32 33 sylancl W LMod I X F : I B j I F I j : I j B
160 simpl1 W LMod I X F : I B j I W LMod
161 26 3ad2ant2 W LMod I X F : I B I j V
162 161 adantr W LMod I X F : I B j I I j V
163 158 1 15 2 5 3 159 160 162 ellspd W LMod I X F : I B j I inv g R l · ˙ F j LSpan W F I j I j y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j
164 157 163 syl5bb W LMod I X F : I B j I inv g R l · ˙ F j LSpan W F I j y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j
165 164 imbi1d W LMod I X F : I B j I inv g R l · ˙ F j LSpan W F I j l = Y y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y
166 r19.23v y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y
167 165 166 syl6bbr W LMod I X F : I B j I inv g R l · ˙ F j LSpan W F I j l = Y y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y
168 167 ralbidv W LMod I X F : I B j I l Base R inv g R l · ˙ F j LSpan W F I j l = Y l Base R y Base R I j finSupp Y y inv g R l · ˙ F j = W y · ˙ f F I j l = Y
169 2 fvexi R V
170 eqid R freeLMod I = R freeLMod I
171 eqid z Base R I | finSupp Y z = z Base R I | finSupp Y z
172 170 15 5 171 frlmbas R V I X z Base R I | finSupp Y z = Base R freeLMod I
173 169 172 mpan I X z Base R I | finSupp Y z = Base R freeLMod I
174 173 3ad2ant2 W LMod I X F : I B z Base R I | finSupp Y z = Base R freeLMod I
175 174 adantr W LMod I X F : I B j I z Base R I | finSupp Y z = Base R freeLMod I
176 175 6 syl6reqr W LMod I X F : I B j I L = z Base R I | finSupp Y z
177 176 raleqdv W LMod I X F : I B j I x L W x · ˙ f F = 0 ˙ x j = Y x z Base R I | finSupp Y z W x · ˙ f F = 0 ˙ x j = Y
178 153 168 177 3bitr4d W LMod I X F : I B j I l Base R inv g R l · ˙ F j LSpan W F I j l = Y x L W x · ˙ f F = 0 ˙ x j = Y
179 7 178 syl5bb W LMod I X F : I B j I l Base R Y ¬ inv g R l · ˙ F j LSpan W F I j x L W x · ˙ f F = 0 ˙ x j = Y
180 2 lmodfgrp W LMod R Grp
181 15 5 14 grpinvnzcl R Grp l Base R Y inv g R l Base R Y
182 180 181 sylan W LMod l Base R Y inv g R l Base R Y
183 15 5 14 grpinvnzcl R Grp k Base R Y inv g R k Base R Y
184 180 183 sylan W LMod k Base R Y inv g R k Base R Y
185 eldifi k Base R Y k Base R
186 15 14 grpinvinv R Grp k Base R inv g R inv g R k = k
187 180 185 186 syl2an W LMod k Base R Y inv g R inv g R k = k
188 187 eqcomd W LMod k Base R Y k = inv g R inv g R k
189 fveq2 l = inv g R k inv g R l = inv g R inv g R k
190 189 rspceeqv inv g R k Base R Y k = inv g R inv g R k l Base R Y k = inv g R l
191 184 188 190 syl2anc W LMod k Base R Y l Base R Y k = inv g R l
192 oveq1 k = inv g R l k · ˙ F j = inv g R l · ˙ F j
193 192 eleq1d k = inv g R l k · ˙ F j LSpan W F I j inv g R l · ˙ F j LSpan W F I j
194 193 notbid k = inv g R l ¬ k · ˙ F j LSpan W F I j ¬ inv g R l · ˙ F j LSpan W F I j
195 194 adantl W LMod k = inv g R l ¬ k · ˙ F j LSpan W F I j ¬ inv g R l · ˙ F j LSpan W F I j
196 182 191 195 ralxfrd W LMod k Base R Y ¬ k · ˙ F j LSpan W F I j l Base R Y ¬ inv g R l · ˙ F j LSpan W F I j
197 196 3ad2ant1 W LMod I X F : I B k Base R Y ¬ k · ˙ F j LSpan W F I j l Base R Y ¬ inv g R l · ˙ F j LSpan W F I j
198 197 adantr W LMod I X F : I B j I k Base R Y ¬ k · ˙ F j LSpan W F I j l Base R Y ¬ inv g R l · ˙ F j LSpan W F I j
199 simplr W LMod I X F : I B j I x L j I
200 5 fvexi Y V
201 200 fvconst2 j I I × Y j = Y
202 199 201 syl W LMod I X F : I B j I x L I × Y j = Y
203 202 eqeq2d W LMod I X F : I B j I x L x j = I × Y j x j = Y
204 203 imbi2d W LMod I X F : I B j I x L W x · ˙ f F = 0 ˙ x j = I × Y j W x · ˙ f F = 0 ˙ x j = Y
205 204 ralbidva W LMod I X F : I B j I x L W x · ˙ f F = 0 ˙ x j = I × Y j x L W x · ˙ f F = 0 ˙ x j = Y
206 179 198 205 3bitr4d W LMod I X F : I B j I k Base R Y ¬ k · ˙ F j LSpan W F I j x L W x · ˙ f F = 0 ˙ x j = I × Y j
207 206 ralbidva W LMod I X F : I B j I k Base R Y ¬ k · ˙ F j LSpan W F I j j I x L W x · ˙ f F = 0 ˙ x j = I × Y j
208 1 3 158 2 15 5 islindf2 W LMod I X F : I B F LIndF W j I k Base R Y ¬ k · ˙ F j LSpan W F I j
209 170 15 6 frlmbasf I X x L x : I Base R
210 209 3ad2antl2 W LMod I X F : I B x L x : I Base R
211 210 ffnd W LMod I X F : I B x L x Fn I
212 fnconstg Y V I × Y Fn I
213 200 212 ax-mp I × Y Fn I
214 eqfnfv x Fn I I × Y Fn I x = I × Y j I x j = I × Y j
215 211 213 214 sylancl W LMod I X F : I B x L x = I × Y j I x j = I × Y j
216 215 imbi2d W LMod I X F : I B x L W x · ˙ f F = 0 ˙ x = I × Y W x · ˙ f F = 0 ˙ j I x j = I × Y j
217 216 ralbidva W LMod I X F : I B x L W x · ˙ f F = 0 ˙ x = I × Y x L W x · ˙ f F = 0 ˙ j I x j = I × Y j
218 r19.21v j I W x · ˙ f F = 0 ˙ x j = I × Y j W x · ˙ f F = 0 ˙ j I x j = I × Y j
219 218 ralbii x L j I W x · ˙ f F = 0 ˙ x j = I × Y j x L W x · ˙ f F = 0 ˙ j I x j = I × Y j
220 ralcom x L j I W x · ˙ f F = 0 ˙ x j = I × Y j j I x L W x · ˙ f F = 0 ˙ x j = I × Y j
221 219 220 bitr3i x L W x · ˙ f F = 0 ˙ j I x j = I × Y j j I x L W x · ˙ f F = 0 ˙ x j = I × Y j
222 217 221 syl6bb W LMod I X F : I B x L W x · ˙ f F = 0 ˙ x = I × Y j I x L W x · ˙ f F = 0 ˙ x j = I × Y j
223 207 208 222 3bitr4d W LMod I X F : I B F LIndF W x L W x · ˙ f F = 0 ˙ x = I × Y