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 ‘ 𝑀 ) 𝑆 ) = 𝑍 )