lincdifsn

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)

	Ref	Expression
Hypotheses	lincdifsn.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	lincdifsn.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
	lincdifsn.s	⊢ 𝑆 = ( Base ‘ 𝑅 )
	lincdifsn.t	⊢ · = ( ·_𝑠 ‘ 𝑀 )
	lincdifsn.p	⊢ + = ( +_g ‘ 𝑀 )
	lincdifsn.0	⊢ 0 = ( 0_g ‘ 𝑅 )
Assertion	lincdifsn	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑉 ∖ { 𝑋 } ) ) + ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lincdifsn.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		lincdifsn.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3		lincdifsn.s	⊢ 𝑆 = ( Base ‘ 𝑅 )
4		lincdifsn.t	⊢ · = ( ·_𝑠 ‘ 𝑀 )
5		lincdifsn.p	⊢ + = ( +_g ‘ 𝑀 )
6		lincdifsn.0	⊢ 0 = ( 0_g ‘ 𝑅 )
7		simp11	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝑀 ∈ LMod )
8	2	fveq2i	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
9	3 8	eqtri	⊢ 𝑆 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
10	9	oveq1i	⊢ ( 𝑆 ↑_m 𝑉 ) = ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 )
11	10	eleq2i	⊢ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ↔ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) )
12	11	biimpi	⊢ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) )
13	12	adantr	⊢ ( ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) )
14	13	3ad2ant2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) )
15	1	pweqi	⊢ 𝒫 𝐵 = 𝒫 ( Base ‘ 𝑀 )
16	15	eleq2i	⊢ ( 𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
17	16	biimpi	⊢ ( 𝑉 ∈ 𝒫 𝐵 → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
18	17	3ad2ant2	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
19	18	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
20		lincval	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
21	7 14 19 20	syl3anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
22		lmodcmn	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ CMnd )
23	22	3ad2ant1	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑀 ∈ CMnd )
24	23	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝑀 ∈ CMnd )
25		simp12	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝑉 ∈ 𝒫 𝐵 )
26	17	anim2i	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
27	26	3adant3	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
28	27	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
29		simp2l	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) )
30	6	breq2i	⊢ ( 𝐹 finSupp 0 ↔ 𝐹 finSupp ( 0_g ‘ 𝑅 ) )
31	30	biimpi	⊢ ( 𝐹 finSupp 0 → 𝐹 finSupp ( 0_g ‘ 𝑅 ) )
32	31	adantl	⊢ ( ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) → 𝐹 finSupp ( 0_g ‘ 𝑅 ) )
33	32	3ad2ant2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝐹 finSupp ( 0_g ‘ 𝑅 ) )
34	2 3	scmfsupp	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp ( 0_g ‘ 𝑅 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) finSupp ( 0_g ‘ 𝑀 ) )
35	28 29 33 34	syl3anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) finSupp ( 0_g ‘ 𝑀 ) )
36		simpl1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝑀 ∈ LMod )
37	36	adantr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑀 ∈ LMod )
38		elmapi	⊢ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) → 𝐹 : 𝑉 ⟶ 𝑆 )
39		ffvelcdm	⊢ ( ( 𝐹 : 𝑉 ⟶ 𝑆 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
40	39	ex	⊢ ( 𝐹 : 𝑉 ⟶ 𝑆 → ( 𝑥 ∈ 𝑉 → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ) )
41	40	a1d	⊢ ( 𝐹 : 𝑉 ⟶ 𝑆 → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ) ) )
42	38 41	syl	⊢ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ) ) )
43	42	adantr	⊢ ( ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ) ) )
44	43	impcom	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ) )
45	44	imp	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
46		elelpwi	⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑥 ∈ 𝐵 )
47	46	expcom	⊢ ( 𝑉 ∈ 𝒫 𝐵 → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ 𝐵 ) )
48	47	3ad2ant2	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ 𝐵 ) )
49	48	adantr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ 𝐵 ) )
50	49	imp	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝐵 )
51		eqid	⊢ ( ·_𝑠 ‘ 𝑀 ) = ( ·_𝑠 ‘ 𝑀 )
52	1 2 51 3	lmodvscl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ∈ 𝐵 )
53	37 45 50 52	syl3anc	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ∈ 𝐵 )
54	53	3adantl3	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ∈ 𝐵 )
55		simp13	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝑋 ∈ 𝑉 )
56		ffvelcdm	⊢ ( ( 𝐹 : 𝑉 ⟶ 𝑆 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 )
57	56	expcom	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 : 𝑉 ⟶ 𝑆 → ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 ) )
58	57	3ad2ant3	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 : 𝑉 ⟶ 𝑆 → ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 ) )
59	38 58	syl5com	⊢ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 ) )
60	59	adantr	⊢ ( ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 ) )
61	60	impcom	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 )
62		elelpwi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑋 ∈ 𝐵 )
63	62	ancoms	⊢ ( ( 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝐵 )
64	63	3adant1	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝐵 )
65	64	adantr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → 𝑋 ∈ 𝐵 )
66	1 2 4 3	lmodvscl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ∈ 𝐵 )
67	36 61 65 66	syl3anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ) → ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ∈ 𝐵 )
68	67	3adant3	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ∈ 𝐵 )
69	4	eqcomi	⊢ ( ·_𝑠 ‘ 𝑀 ) = ·
70	69	a1i	⊢ ( 𝑥 = 𝑋 → ( ·_𝑠 ‘ 𝑀 ) = · )
71		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
72		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
73	70 71 72	oveq123d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) )
74	73	adantl	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) ∧ 𝑥 = 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) )
75	1 5 24 25 35 54 55 68 74	gsumdifsnd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( ( 𝑀 Σ_g ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ) )
76		fveq1	⊢ ( 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) → ( 𝐺 ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ‘ 𝑥 ) )
77	76	3ad2ant3	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ‘ 𝑥 ) )
78		fvres	⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) → ( ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
79	77 78	sylan9eq	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
80	79	oveq1d	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ) → ( ( 𝐺 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) )
81	80	mpteq2dva	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) )
82	81	eqcomd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) )
83	82	oveq2d	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑀 Σ_g ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( 𝑀 Σ_g ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
84	83	oveq1d	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( ( 𝑀 Σ_g ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ) = ( ( 𝑀 Σ_g ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ) )
85	75 84	eqtrd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( ( 𝑀 Σ_g ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ) )
86		eqid	⊢ 𝑉 = 𝑉
87	86 9	feq23i	⊢ ( 𝐹 : 𝑉 ⟶ 𝑆 ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
88	38 87	sylib	⊢ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
89	88	adantr	⊢ ( ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
90	89	3ad2ant2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
91		difssd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑉 ∖ { 𝑋 } ) ⊆ 𝑉 )
92	90 91	fssresd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) : ( 𝑉 ∖ { 𝑋 } ) ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
93		feq1	⊢ ( 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) → ( 𝐺 : ( 𝑉 ∖ { 𝑋 } ) ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) : ( 𝑉 ∖ { 𝑋 } ) ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
94	93	3ad2ant3	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝐺 : ( 𝑉 ∖ { 𝑋 } ) ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) : ( 𝑉 ∖ { 𝑋 } ) ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
95	92 94	mpbird	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝐺 : ( 𝑉 ∖ { 𝑋 } ) ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
96		fvex	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
97		difexg	⊢ ( 𝑉 ∈ 𝒫 𝐵 → ( 𝑉 ∖ { 𝑋 } ) ∈ V )
98	97	3ad2ant2	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑉 ∖ { 𝑋 } ) ∈ V )
99	98	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑉 ∖ { 𝑋 } ) ∈ V )
100		elmapg	⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ∧ ( 𝑉 ∖ { 𝑋 } ) ∈ V ) → ( 𝐺 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m ( 𝑉 ∖ { 𝑋 } ) ) ↔ 𝐺 : ( 𝑉 ∖ { 𝑋 } ) ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
101	96 99 100	sylancr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝐺 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m ( 𝑉 ∖ { 𝑋 } ) ) ↔ 𝐺 : ( 𝑉 ∖ { 𝑋 } ) ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
102	95 101	mpbird	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → 𝐺 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m ( 𝑉 ∖ { 𝑋 } ) ) )
103		elpwi	⊢ ( 𝑉 ∈ 𝒫 𝐵 → 𝑉 ⊆ 𝐵 )
104	1	sseq2i	⊢ ( 𝑉 ⊆ 𝐵 ↔ 𝑉 ⊆ ( Base ‘ 𝑀 ) )
105	104	biimpi	⊢ ( 𝑉 ⊆ 𝐵 → 𝑉 ⊆ ( Base ‘ 𝑀 ) )
106	105	ssdifssd	⊢ ( 𝑉 ⊆ 𝐵 → ( 𝑉 ∖ { 𝑋 } ) ⊆ ( Base ‘ 𝑀 ) )
107	103 106	syl	⊢ ( 𝑉 ∈ 𝒫 𝐵 → ( 𝑉 ∖ { 𝑋 } ) ⊆ ( Base ‘ 𝑀 ) )
108	107	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑉 ∖ { 𝑋 } ) ⊆ ( Base ‘ 𝑀 ) )
109	97	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑉 ∖ { 𝑋 } ) ∈ V )
110		elpwg	⊢ ( ( 𝑉 ∖ { 𝑋 } ) ∈ V → ( ( 𝑉 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ ( 𝑉 ∖ { 𝑋 } ) ⊆ ( Base ‘ 𝑀 ) ) )
111	109 110	syl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( ( 𝑉 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ ( 𝑉 ∖ { 𝑋 } ) ⊆ ( Base ‘ 𝑀 ) ) )
112	108 111	mpbird	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑉 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
113	112	3adant3	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑉 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
114	113	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑉 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
115		lincval	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐺 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m ( 𝑉 ∖ { 𝑋 } ) ) ∧ ( 𝑉 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑉 ∖ { 𝑋 } ) ) = ( 𝑀 Σ_g ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
116	7 102 114 115	syl3anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑉 ∖ { 𝑋 } ) ) = ( 𝑀 Σ_g ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
117	116	eqcomd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝑀 Σ_g ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑉 ∖ { 𝑋 } ) ) )
118	117	oveq1d	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( ( 𝑀 Σ_g ( 𝑥 ∈ ( 𝑉 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ) = ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑉 ∖ { 𝑋 } ) ) + ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ) )
119	21 85 118	3eqtrd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 ∈ ( 𝑆 ↑_m 𝑉 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑉 ∖ { 𝑋 } ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑉 ∖ { 𝑋 } ) ) + ( ( 𝐹 ‘ 𝑋 ) · 𝑋 ) ) )

Metamath Proof Explorer

Theorem lincdifsn

Proof