Metamath Proof Explorer

Theorem lincext3

Description: Property 3 of an extension of a linear combination. (Contributed by AV, 23-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 lincext3 ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 )

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 simp1l ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝑀 ∈ LMod )
9 simp1r ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝑆 ∈ 𝒫 𝐵 )
10 simp2 ⊢ ( ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) → 𝑋 ∈ 𝑆 )
11 10 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝑋 ∈ 𝑆 )
12 1 2 3 4 5 6 7 lincext1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) )
13 12 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) )
14 1 2 3 4 5 6 7 lincext2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ 𝐺 finSupp 0 ) → 𝐹 finSupp 0 )
15 14 3adant3r ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝐹 finSupp 0 )
16 elmapi ⊢ ( 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) → 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 )
17 7 fdmdifeqresdif ⊢ ( 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 → 𝐺 = ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) )
18 16 17 syl ⊢ ( 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) → 𝐺 = ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) )
19 18 3ad2ant3 ⊢ ( ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) → 𝐺 = ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) )
20 19 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝐺 = ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) )
21 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
22 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
23 1 2 3 21 22 4 lincdifsn ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) )
24 8 9 11 13 15 20 23 syl321anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) )
25 oveq1 ⊢ ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) → ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) = ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) )
26 25 eqcoms ⊢ ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) = ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) )
27 26 adantl ⊢ ( ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) → ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) = ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) )
28 27 3ad2ant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) = ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) )
29 eqid ⊢ ( invg ‘ 𝑀 ) = ( invg ‘ 𝑀 )
30 simpll ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝑀 ∈ LMod )
31 elelpwi ⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑋 ∈ 𝐵 )
32 31 expcom ⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( 𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐵 ) )
33 32 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐵 ) )
34 33 com12 ⊢ ( 𝑋 ∈ 𝑆 → ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑋 ∈ 𝐵 ) )
35 34 3ad2ant2 ⊢ ( ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) → ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑋 ∈ 𝐵 ) )
36 35 impcom ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝑋 ∈ 𝐵 )
37 simpr1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝑌 ∈ 𝐸 )
38 1 2 21 29 3 6 30 36 37 lmodvsneg ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( invg ‘ 𝑀 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) = ( ( 𝑁 ‘ 𝑌 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) )
39 iftrue ⊢ ( 𝑧 = 𝑋 → if ( 𝑧 = 𝑋 , ( 𝑁 ‘ 𝑌 ) , ( 𝐺 ‘ 𝑧 ) ) = ( 𝑁 ‘ 𝑌 ) )
40 10 adantl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → 𝑋 ∈ 𝑆 )
41 fvexd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝑁 ‘ 𝑌 ) ∈ V )
42 7 39 40 41 fvmptd3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑁 ‘ 𝑌 ) )
43 42 eqcomd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝑁 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) )
44 43 oveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( 𝑁 ‘ 𝑌 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) )
45 38 44 eqtr2d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( ( invg ‘ 𝑀 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) )
46 45 oveq2d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) = ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) ) )
47 1 2 21 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ 𝐵 )
48 30 37 36 47 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ 𝐵 )
49 1 22 5 29 lmodvnegid ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ 𝐵 ) → ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) ) = 𝑍 )
50 30 48 49 syl2anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) ) = 𝑍 )
51 46 50 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) = 𝑍 )
52 51 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) = 𝑍 )
53 28 52 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ( +g ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ) = 𝑍 )
54 24 53 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 finSupp 0 ∧ ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 𝐺 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 )