Metamath Proof Explorer

Theorem lincext1

Description: Property 1 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019) (Revised by AV, 29-Apr-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 lincext1 ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) )

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 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
9 8 lmodfgrp ⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) ∈ Grp )
10 9 ad2antrr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( Scalar ‘ 𝑀 ) ∈ Grp )
11 2 10 eqeltrid ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝑅 ∈ Grp )
12 simpr1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝑌 ∈ 𝐸 )
13 3 6 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑌 ∈ 𝐸 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐸 )
14 11 12 13 syl2anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐸 )
15 14 ad2antrr ⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑧 = 𝑋 ) → ( 𝑁 ‘ 𝑌 ) ∈ 𝐸 )
16 elmapi ⊢ ( 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) → 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 )
17 df-ne ⊢ ( 𝑧 ≠ 𝑋 ↔ ¬ 𝑧 = 𝑋 )
18 17 biimpri ⊢ ( ¬ 𝑧 = 𝑋 → 𝑧 ≠ 𝑋 )
19 18 anim2i ⊢ ( ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 = 𝑋 ) → ( 𝑧 ∈ 𝑆 ∧ 𝑧 ≠ 𝑋 ) )
20 eldifsn ⊢ ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↔ ( 𝑧 ∈ 𝑆 ∧ 𝑧 ≠ 𝑋 ) )
21 19 20 sylibr ⊢ ( ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 = 𝑋 ) → 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) )
22 ffvelrn ⊢ ( ( 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 )
23 21 22 sylan2 ⊢ ( ( 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 = 𝑋 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 )
24 23 ex ⊢ ( 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 → ( ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 = 𝑋 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 ) )
25 16 24 syl ⊢ ( 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 = 𝑋 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 ) )
26 25 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) → ( ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 = 𝑋 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 ) )
27 26 adantl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 = 𝑋 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 ) )
28 27 impl ⊢ ( ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ ¬ 𝑧 = 𝑋 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 )
29 15 28 ifclda ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) ∧ 𝑧 ∈ 𝑆 ) → if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) ∈ 𝐸 )
30 29 fmpttd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) ) : 𝑆 ⟶ 𝐸 )
31 simpr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑆 ∈ 𝒫 𝐵 )
32 3 fvexi ⊢ 𝐸 ∈ V
33 31 32 jctil ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝐸 ∈ V ∧ 𝑆 ∈ 𝒫 𝐵 ) )
34 33 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝐸 ∈ V ∧ 𝑆 ∈ 𝒫 𝐵 ) )
35 elmapg ⊢ ( ( 𝐸 ∈ V ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 𝐸 ↑m 𝑆 ) ↔ ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) ) : 𝑆 ⟶ 𝐸 ) )
36 34 35 syl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 𝐸 ↑m 𝑆 ) ↔ ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) ) : 𝑆 ⟶ 𝐸 ) )
37 30 36 mpbird ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝑧 ∈ 𝑆 ↦ if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 𝐸 ↑m 𝑆 ) )
38 7 37 eqeltrid ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) )