Metamath Proof Explorer

Theorem lincext2

Description: Property 2 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Hypotheses lincext.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
lincext.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
lincext.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
lincext.0 ⊢ 0 = ( 0g ‘ 𝑅 )
lincext.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
lincext.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
lincext.f ⊢ 𝐹 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) )
Assertion lincext2 ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → 𝐹 finSupp 0 )

Proof

Step Hyp Ref Expression
1 lincext.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 lincext.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3 lincext.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
4 lincext.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 lincext.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
6 lincext.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
7 lincext.f ⊢ 𝐹 = ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) )
8 fvex ⊢ ( 𝑁 ‘ 𝑌 ) ∈ V
9 fvex ⊢ ( 𝐺 ‘ 𝑧 ) ∈ V
10 8 9 ifex ⊢ if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) ∈ V
11 10 7 dmmpti ⊢ dom 𝐹 = 𝑆
12 11 difeq1i ⊢ ( dom 𝐹 ∖ ( 𝑆 ∖ { 𝑋 } ) ) = ( 𝑆 ∖ ( 𝑆 ∖ { 𝑋 } ) )
13 snssi ⊢ ( 𝑋 ∈ 𝑆 → { 𝑋 } ⊆ 𝑆 )
14 13 3ad2ant2 ⊢ ( ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) → { 𝑋 } ⊆ 𝑆 )
15 14 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → { 𝑋 } ⊆ 𝑆 )
16 dfss4 ⊢ ( { 𝑋 } ⊆ 𝑆 ↔ ( 𝑆 ∖ ( 𝑆 ∖ { 𝑋 } ) ) = { 𝑋 } )
17 15 16 sylib ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → ( 𝑆 ∖ ( 𝑆 ∖ { 𝑋 } ) ) = { 𝑋 } )
18 snfi ⊢ { 𝑋 } ∈ Fin
19 17 18 eqeltrdi ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → ( 𝑆 ∖ ( 𝑆 ∖ { 𝑋 } ) ) ∈ Fin )
20 12 19 eqeltrid ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → ( dom 𝐹 ∖ ( 𝑆 ∖ { 𝑋 } ) ) ∈ Fin )
21 1 2 3 4 5 6 7 lincext1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) )
22 21 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) )
23 elmapfun ⊢ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) → Fun 𝐹 )
24 22 23 syl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → Fun 𝐹 )
25 elmapi ⊢ ( 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) → 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 )
26 7 fdmdifeqresdif ⊢ ( 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 → 𝐺 = ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) )
27 25 26 syl ⊢ ( 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) → 𝐺 = ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) )
28 27 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) → 𝐺 = ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) )
29 28 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → 𝐺 = ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) )
30 simp3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → 𝐺 finSupp 0 )
31 4 fvexi ⊢ 0 ∈ V
32 31 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → 0 ∈ V )
33 20 22 24 29 30 32 resfsupp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → 𝐹 finSupp 0 )