Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lincdifsn Structured version   Visualization version   GIF version

Theorem lincdifsn 41498
Description: A vector is a linear combination of a set containing this vector. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.)
Hypotheses
Ref Expression
lincdifsn.b 𝐵 = (Base‘𝑀)
lincdifsn.r 𝑅 = (Scalar‘𝑀)
lincdifsn.s 𝑆 = (Base‘𝑅)
lincdifsn.t · = ( ·𝑠𝑀)
lincdifsn.p + = (+g𝑀)
lincdifsn.0 0 = (0g𝑅)
Assertion
Ref Expression
lincdifsn (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝐹( linC ‘𝑀)𝑉) = ((𝐺( linC ‘𝑀)(𝑉 ∖ {𝑋})) + ((𝐹𝑋) · 𝑋)))

Proof of Theorem lincdifsn
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simp11 1089 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝑀 ∈ LMod)
2 lincdifsn.s . . . . . . . . 9 𝑆 = (Base‘𝑅)
3 lincdifsn.r . . . . . . . . . 10 𝑅 = (Scalar‘𝑀)
43fveq2i 6151 . . . . . . . . 9 (Base‘𝑅) = (Base‘(Scalar‘𝑀))
52, 4eqtri 2643 . . . . . . . 8 𝑆 = (Base‘(Scalar‘𝑀))
65oveq1i 6614 . . . . . . 7 (𝑆𝑚 𝑉) = ((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)
76eleq2i 2690 . . . . . 6 (𝐹 ∈ (𝑆𝑚 𝑉) ↔ 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉))
87biimpi 206 . . . . 5 (𝐹 ∈ (𝑆𝑚 𝑉) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉))
98adantr 481 . . . 4 ((𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉))
1093ad2ant2 1081 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉))
11 lincdifsn.b . . . . . . . 8 𝐵 = (Base‘𝑀)
1211pweqi 4134 . . . . . . 7 𝒫 𝐵 = 𝒫 (Base‘𝑀)
1312eleq2i 2690 . . . . . 6 (𝑉 ∈ 𝒫 𝐵𝑉 ∈ 𝒫 (Base‘𝑀))
1413biimpi 206 . . . . 5 (𝑉 ∈ 𝒫 𝐵𝑉 ∈ 𝒫 (Base‘𝑀))
15143ad2ant2 1081 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → 𝑉 ∈ 𝒫 (Base‘𝑀))
16153ad2ant1 1080 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝑉 ∈ 𝒫 (Base‘𝑀))
17 lincval 41483 . . 3 ((𝑀 ∈ LMod ∧ 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥𝑉 ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥))))
181, 10, 16, 17syl3anc 1323 . 2 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥𝑉 ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥))))
19 lincdifsn.p . . . 4 + = (+g𝑀)
20 lmodcmn 18832 . . . . . 6 (𝑀 ∈ LMod → 𝑀 ∈ CMnd)
21203ad2ant1 1080 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → 𝑀 ∈ CMnd)
22213ad2ant1 1080 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝑀 ∈ CMnd)
23 simp12 1090 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝑉 ∈ 𝒫 𝐵)
2414anim2i 592 . . . . . . 7 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)))
25243adant3 1079 . . . . . 6 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)))
26253ad2ant1 1080 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)))
27 simp2l 1085 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝐹 ∈ (𝑆𝑚 𝑉))
28 lincdifsn.0 . . . . . . . . 9 0 = (0g𝑅)
2928breq2i 4621 . . . . . . . 8 (𝐹 finSupp 0𝐹 finSupp (0g𝑅))
3029biimpi 206 . . . . . . 7 (𝐹 finSupp 0𝐹 finSupp (0g𝑅))
3130adantl 482 . . . . . 6 ((𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) → 𝐹 finSupp (0g𝑅))
32313ad2ant2 1081 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝐹 finSupp (0g𝑅))
333, 2scmfsupp 41444 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp (0g𝑅)) → (𝑥𝑉 ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥)) finSupp (0g𝑀))
3426, 27, 32, 33syl3anc 1323 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑥𝑉 ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥)) finSupp (0g𝑀))
35 simpl1 1062 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 )) → 𝑀 ∈ LMod)
3635adantr 481 . . . . . 6 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 )) ∧ 𝑥𝑉) → 𝑀 ∈ LMod)
37 elmapi 7823 . . . . . . . . . 10 (𝐹 ∈ (𝑆𝑚 𝑉) → 𝐹:𝑉𝑆)
38 ffvelrn 6313 . . . . . . . . . . . 12 ((𝐹:𝑉𝑆𝑥𝑉) → (𝐹𝑥) ∈ 𝑆)
3938ex 450 . . . . . . . . . . 11 (𝐹:𝑉𝑆 → (𝑥𝑉 → (𝐹𝑥) ∈ 𝑆))
4039a1d 25 . . . . . . . . . 10 (𝐹:𝑉𝑆 → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → (𝑥𝑉 → (𝐹𝑥) ∈ 𝑆)))
4137, 40syl 17 . . . . . . . . 9 (𝐹 ∈ (𝑆𝑚 𝑉) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → (𝑥𝑉 → (𝐹𝑥) ∈ 𝑆)))
4241adantr 481 . . . . . . . 8 ((𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → (𝑥𝑉 → (𝐹𝑥) ∈ 𝑆)))
4342impcom 446 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 )) → (𝑥𝑉 → (𝐹𝑥) ∈ 𝑆))
4443imp 445 . . . . . 6 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 )) ∧ 𝑥𝑉) → (𝐹𝑥) ∈ 𝑆)
45 elelpwi 4142 . . . . . . . . . 10 ((𝑥𝑉𝑉 ∈ 𝒫 𝐵) → 𝑥𝐵)
4645expcom 451 . . . . . . . . 9 (𝑉 ∈ 𝒫 𝐵 → (𝑥𝑉𝑥𝐵))
47463ad2ant2 1081 . . . . . . . 8 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → (𝑥𝑉𝑥𝐵))
4847adantr 481 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 )) → (𝑥𝑉𝑥𝐵))
4948imp 445 . . . . . 6 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 )) ∧ 𝑥𝑉) → 𝑥𝐵)
50 eqid 2621 . . . . . . 7 ( ·𝑠𝑀) = ( ·𝑠𝑀)
5111, 3, 50, 2lmodvscl 18801 . . . . . 6 ((𝑀 ∈ LMod ∧ (𝐹𝑥) ∈ 𝑆𝑥𝐵) → ((𝐹𝑥)( ·𝑠𝑀)𝑥) ∈ 𝐵)
5236, 44, 49, 51syl3anc 1323 . . . . 5 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 )) ∧ 𝑥𝑉) → ((𝐹𝑥)( ·𝑠𝑀)𝑥) ∈ 𝐵)
53523adantl3 1217 . . . 4 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) ∧ 𝑥𝑉) → ((𝐹𝑥)( ·𝑠𝑀)𝑥) ∈ 𝐵)
54 simp13 1091 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝑋𝑉)
55 ffvelrn 6313 . . . . . . . . . . 11 ((𝐹:𝑉𝑆𝑋𝑉) → (𝐹𝑋) ∈ 𝑆)
5655expcom 451 . . . . . . . . . 10 (𝑋𝑉 → (𝐹:𝑉𝑆 → (𝐹𝑋) ∈ 𝑆))
57563ad2ant3 1082 . . . . . . . . 9 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → (𝐹:𝑉𝑆 → (𝐹𝑋) ∈ 𝑆))
5837, 57syl5com 31 . . . . . . . 8 (𝐹 ∈ (𝑆𝑚 𝑉) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → (𝐹𝑋) ∈ 𝑆))
5958adantr 481 . . . . . . 7 ((𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → (𝐹𝑋) ∈ 𝑆))
6059impcom 446 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 )) → (𝐹𝑋) ∈ 𝑆)
61 elelpwi 4142 . . . . . . . . 9 ((𝑋𝑉𝑉 ∈ 𝒫 𝐵) → 𝑋𝐵)
6261ancoms 469 . . . . . . . 8 ((𝑉 ∈ 𝒫 𝐵𝑋𝑉) → 𝑋𝐵)
63623adant1 1077 . . . . . . 7 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → 𝑋𝐵)
6463adantr 481 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 )) → 𝑋𝐵)
65 lincdifsn.t . . . . . . 7 · = ( ·𝑠𝑀)
6611, 3, 65, 2lmodvscl 18801 . . . . . 6 ((𝑀 ∈ LMod ∧ (𝐹𝑋) ∈ 𝑆𝑋𝐵) → ((𝐹𝑋) · 𝑋) ∈ 𝐵)
6735, 60, 64, 66syl3anc 1323 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 )) → ((𝐹𝑋) · 𝑋) ∈ 𝐵)
68673adant3 1079 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → ((𝐹𝑋) · 𝑋) ∈ 𝐵)
6965eqcomi 2630 . . . . . . 7 ( ·𝑠𝑀) = ·
7069a1i 11 . . . . . 6 (𝑥 = 𝑋 → ( ·𝑠𝑀) = · )
71 fveq2 6148 . . . . . 6 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
72 id 22 . . . . . 6 (𝑥 = 𝑋𝑥 = 𝑋)
7370, 71, 72oveq123d 6625 . . . . 5 (𝑥 = 𝑋 → ((𝐹𝑥)( ·𝑠𝑀)𝑥) = ((𝐹𝑋) · 𝑋))
7473adantl 482 . . . 4 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) ∧ 𝑥 = 𝑋) → ((𝐹𝑥)( ·𝑠𝑀)𝑥) = ((𝐹𝑋) · 𝑋))
7511, 19, 22, 23, 34, 53, 54, 68, 74gsumdifsnd 18281 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑀 Σg (𝑥𝑉 ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥))) = ((𝑀 Σg (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥))) + ((𝐹𝑋) · 𝑋)))
76 fveq1 6147 . . . . . . . . . 10 (𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋})) → (𝐺𝑥) = ((𝐹 ↾ (𝑉 ∖ {𝑋}))‘𝑥))
77763ad2ant3 1082 . . . . . . . . 9 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝐺𝑥) = ((𝐹 ↾ (𝑉 ∖ {𝑋}))‘𝑥))
78 fvres 6164 . . . . . . . . 9 (𝑥 ∈ (𝑉 ∖ {𝑋}) → ((𝐹 ↾ (𝑉 ∖ {𝑋}))‘𝑥) = (𝐹𝑥))
7977, 78sylan9eq 2675 . . . . . . . 8 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) ∧ 𝑥 ∈ (𝑉 ∖ {𝑋})) → (𝐺𝑥) = (𝐹𝑥))
8079oveq1d 6619 . . . . . . 7 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) ∧ 𝑥 ∈ (𝑉 ∖ {𝑋})) → ((𝐺𝑥)( ·𝑠𝑀)𝑥) = ((𝐹𝑥)( ·𝑠𝑀)𝑥))
8180mpteq2dva 4704 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐺𝑥)( ·𝑠𝑀)𝑥)) = (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥)))
8281eqcomd 2627 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥)) = (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐺𝑥)( ·𝑠𝑀)𝑥)))
8382oveq2d 6620 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑀 Σg (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥))) = (𝑀 Σg (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐺𝑥)( ·𝑠𝑀)𝑥))))
8483oveq1d 6619 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → ((𝑀 Σg (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥))) + ((𝐹𝑋) · 𝑋)) = ((𝑀 Σg (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐺𝑥)( ·𝑠𝑀)𝑥))) + ((𝐹𝑋) · 𝑋)))
8575, 84eqtrd 2655 . 2 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑀 Σg (𝑥𝑉 ↦ ((𝐹𝑥)( ·𝑠𝑀)𝑥))) = ((𝑀 Σg (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐺𝑥)( ·𝑠𝑀)𝑥))) + ((𝐹𝑋) · 𝑋)))
86 eqid 2621 . . . . . . . . . . . 12 𝑉 = 𝑉
8786, 5feq23i 5996 . . . . . . . . . . 11 (𝐹:𝑉𝑆𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))
8837, 87sylib 208 . . . . . . . . . 10 (𝐹 ∈ (𝑆𝑚 𝑉) → 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))
8988adantr 481 . . . . . . . . 9 ((𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) → 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))
90893ad2ant2 1081 . . . . . . . 8 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))
91 difssd 3716 . . . . . . . 8 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑉 ∖ {𝑋}) ⊆ 𝑉)
9290, 91fssresd 6028 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝐹 ↾ (𝑉 ∖ {𝑋})):(𝑉 ∖ {𝑋})⟶(Base‘(Scalar‘𝑀)))
93 feq1 5983 . . . . . . . 8 (𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋})) → (𝐺:(𝑉 ∖ {𝑋})⟶(Base‘(Scalar‘𝑀)) ↔ (𝐹 ↾ (𝑉 ∖ {𝑋})):(𝑉 ∖ {𝑋})⟶(Base‘(Scalar‘𝑀))))
94933ad2ant3 1082 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝐺:(𝑉 ∖ {𝑋})⟶(Base‘(Scalar‘𝑀)) ↔ (𝐹 ↾ (𝑉 ∖ {𝑋})):(𝑉 ∖ {𝑋})⟶(Base‘(Scalar‘𝑀))))
9592, 94mpbird 247 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝐺:(𝑉 ∖ {𝑋})⟶(Base‘(Scalar‘𝑀)))
96 fvex 6158 . . . . . . 7 (Base‘(Scalar‘𝑀)) ∈ V
97 difexg 4768 . . . . . . . . 9 (𝑉 ∈ 𝒫 𝐵 → (𝑉 ∖ {𝑋}) ∈ V)
98973ad2ant2 1081 . . . . . . . 8 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → (𝑉 ∖ {𝑋}) ∈ V)
99983ad2ant1 1080 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑉 ∖ {𝑋}) ∈ V)
100 elmapg 7815 . . . . . . 7 (((Base‘(Scalar‘𝑀)) ∈ V ∧ (𝑉 ∖ {𝑋}) ∈ V) → (𝐺 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 (𝑉 ∖ {𝑋})) ↔ 𝐺:(𝑉 ∖ {𝑋})⟶(Base‘(Scalar‘𝑀))))
10196, 99, 100sylancr 694 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝐺 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 (𝑉 ∖ {𝑋})) ↔ 𝐺:(𝑉 ∖ {𝑋})⟶(Base‘(Scalar‘𝑀))))
10295, 101mpbird 247 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → 𝐺 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 (𝑉 ∖ {𝑋})))
103 elpwi 4140 . . . . . . . . . 10 (𝑉 ∈ 𝒫 𝐵𝑉𝐵)
10411sseq2i 3609 . . . . . . . . . . . 12 (𝑉𝐵𝑉 ⊆ (Base‘𝑀))
105104biimpi 206 . . . . . . . . . . 11 (𝑉𝐵𝑉 ⊆ (Base‘𝑀))
106105ssdifssd 3726 . . . . . . . . . 10 (𝑉𝐵 → (𝑉 ∖ {𝑋}) ⊆ (Base‘𝑀))
107103, 106syl 17 . . . . . . . . 9 (𝑉 ∈ 𝒫 𝐵 → (𝑉 ∖ {𝑋}) ⊆ (Base‘𝑀))
108107adantl 482 . . . . . . . 8 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑉 ∖ {𝑋}) ⊆ (Base‘𝑀))
10997adantl 482 . . . . . . . . 9 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑉 ∖ {𝑋}) ∈ V)
110 elpwg 4138 . . . . . . . . 9 ((𝑉 ∖ {𝑋}) ∈ V → ((𝑉 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑉 ∖ {𝑋}) ⊆ (Base‘𝑀)))
111109, 110syl 17 . . . . . . . 8 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → ((𝑉 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑉 ∖ {𝑋}) ⊆ (Base‘𝑀)))
112108, 111mpbird 247 . . . . . . 7 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑉 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀))
1131123adant3 1079 . . . . . 6 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) → (𝑉 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀))
1141133ad2ant1 1080 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑉 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀))
115 lincval 41483 . . . . 5 ((𝑀 ∈ LMod ∧ 𝐺 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚 (𝑉 ∖ {𝑋})) ∧ (𝑉 ∖ {𝑋}) ∈ 𝒫 (Base‘𝑀)) → (𝐺( linC ‘𝑀)(𝑉 ∖ {𝑋})) = (𝑀 Σg (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐺𝑥)( ·𝑠𝑀)𝑥))))
1161, 102, 114, 115syl3anc 1323 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝐺( linC ‘𝑀)(𝑉 ∖ {𝑋})) = (𝑀 Σg (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐺𝑥)( ·𝑠𝑀)𝑥))))
117116eqcomd 2627 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝑀 Σg (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐺𝑥)( ·𝑠𝑀)𝑥))) = (𝐺( linC ‘𝑀)(𝑉 ∖ {𝑋})))
118117oveq1d 6619 . 2 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → ((𝑀 Σg (𝑥 ∈ (𝑉 ∖ {𝑋}) ↦ ((𝐺𝑥)( ·𝑠𝑀)𝑥))) + ((𝐹𝑋) · 𝑋)) = ((𝐺( linC ‘𝑀)(𝑉 ∖ {𝑋})) + ((𝐹𝑋) · 𝑋)))
11918, 85, 1183eqtrd 2659 1 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵𝑋𝑉) ∧ (𝐹 ∈ (𝑆𝑚 𝑉) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑉 ∖ {𝑋}))) → (𝐹( linC ‘𝑀)𝑉) = ((𝐺( linC ‘𝑀)(𝑉 ∖ {𝑋})) + ((𝐹𝑋) · 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  Vcvv 3186  cdif 3552  wss 3555  𝒫 cpw 4130  {csn 4148   class class class wbr 4613  cmpt 4673  cres 5076  wf 5843  cfv 5847  (class class class)co 6604  𝑚 cmap 7802   finSupp cfsupp 8219  Basecbs 15781  +gcplusg 15862  Scalarcsca 15865   ·𝑠 cvsca 15866  0gc0g 16021   Σg cgsu 16022  CMndccmn 18114  LModclmod 18784   linC clinc 41478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-oi 8359  df-card 8709  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-n0 11237  df-z 11322  df-uz 11632  df-fz 12269  df-fzo 12407  df-seq 12742  df-hash 13058  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-0g 16023  df-gsum 16024  df-mre 16167  df-mrc 16168  df-acs 16170  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-grp 17346  df-minusg 17347  df-mulg 17462  df-cntz 17671  df-cmn 18116  df-abl 18117  df-mgp 18411  df-ur 18423  df-ring 18470  df-lmod 18786  df-linc 41480
This theorem is referenced by:  lincext3  41530  lindslinindimp2lem4  41535  lincresunit3  41555
  Copyright terms: Public domain W3C validator