Theorem lincresunit3lem2

Description: Lemma 2 for lincresunit3 . (Contributed by AV, 18-May-2019) (Proof shortened by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	lincresunit.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	lincresunit.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
	lincresunit.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
	lincresunit.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	lincresunit.0	⊢ 0 = ( 0g ‘ 𝑅 )
	lincresunit.z	⊢ 𝑍 = ( 0g ‘ 𝑀 )
	lincresunit.n	⊢ 𝑁 = ( invg ‘ 𝑅 )
	lincresunit.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
	lincresunit.t	⊢ · = ( .r ‘ 𝑅 )
	lincresunit.g	⊢ 𝐺 = ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑠 ) ) )
Assertion	lincresunit3lem2	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ( ·𝑠 ‘ 𝑀 ) ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) ) = ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lincresunit.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		lincresunit.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3		lincresunit.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
4		lincresunit.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
5		lincresunit.0	⊢ 0 = ( 0g ‘ 𝑅 )
6		lincresunit.z	⊢ 𝑍 = ( 0g ‘ 𝑀 )
7		lincresunit.n	⊢ 𝑁 = ( invg ‘ 𝑅 )
8		lincresunit.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
9		lincresunit.t	⊢ · = ( .r ‘ 𝑅 )
10		lincresunit.g	⊢ 𝐺 = ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑠 ) ) )
11		simpl2	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → 𝑀 ∈ LMod )
12	2	fveq2i	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
13	3 12	eqtri	⊢ 𝐸 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
14	13	oveq1i	⊢ ( 𝐸 ↑m 𝑆 ) = ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 )
15	14	eleq2i	⊢ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ↔ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 ) )
16	15	biimpi	⊢ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 ) )
17	16	3ad2ant1	⊢ ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 ) )
18	17	adantl	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 ) )
19		difssd	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑆 ∖ { 𝑋 } ) ⊆ 𝑆 )
20		elmapssres	⊢ ( ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 ) ∧ ( 𝑆 ∖ { 𝑋 } ) ⊆ 𝑆 ) → ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ( 𝑆 ∖ { 𝑋 } ) ) )
21	18 19 20	syl2anc	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ( 𝑆 ∖ { 𝑋 } ) ) )
22		elpwi	⊢ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
23	22	ssdifssd	⊢ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∖ { 𝑋 } ) ⊆ ( Base ‘ 𝑀 ) )
24		difexg	⊢ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
25		elpwg	⊢ ( ( 𝑆 ∖ { 𝑋 } ) ∈ V → ( ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ ( 𝑆 ∖ { 𝑋 } ) ⊆ ( Base ‘ 𝑀 ) ) )
26	24 25	syl	⊢ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ ( 𝑆 ∖ { 𝑋 } ) ⊆ ( Base ‘ 𝑀 ) ) )
27	23 26	mpbird	⊢ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
28	1	pweqi	⊢ 𝒫 𝐵 = 𝒫 ( Base ‘ 𝑀 )
29	27 28	eleq2s	⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
30	29	3ad2ant1	⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
31	30	adantr	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) )
32		lincval	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) = ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) )
33	11 21 31 32	syl3anc	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) = ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) )
34		simpll	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) )
35		simplr1	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) )
36		simplr2	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
37		simpr	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) )
38	1 2 3 4 5 6 7 8 9 10	lincresunit3lem1	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) ) → ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ( ·𝑠 ‘ 𝑀 ) ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) )
39	34 35 36 37 38	syl13anc	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ( ·𝑠 ‘ 𝑀 ) ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) )
40		fvres	⊢ ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) → ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
41	40	adantl	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
42	41	eqcomd	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( 𝐹 ‘ 𝑧 ) = ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ‘ 𝑧 ) )
43	42	oveq1d	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝐹 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) = ( ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) )
44	39 43	eqtrd	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ( ·𝑠 ‘ 𝑀 ) ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) = ( ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) )
45	44	mpteq2dva	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ( ·𝑠 ‘ 𝑀 ) ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) )
46	45	oveq2d	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ( ·𝑠 ‘ 𝑀 ) ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) ) = ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) )
47		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
48		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
49		difexg	⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
50	49	3ad2ant1	⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
51	50	adantr	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
52	2	lmodfgrp	⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Grp )
53	52	3ad2ant2	⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → 𝑅 ∈ Grp )
54	53	adantr	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ) → 𝑅 ∈ Grp )
55		elmapi	⊢ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) → 𝐹 : 𝑆 ⟶ 𝐸 )
56		ffvelcdm	⊢ ( ( 𝐹 : 𝑆 ⟶ 𝐸 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐸 )
57	56	expcom	⊢ ( 𝑋 ∈ 𝑆 → ( 𝐹 : 𝑆 ⟶ 𝐸 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐸 ) )
58	57	3ad2ant3	⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 : 𝑆 ⟶ 𝐸 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐸 ) )
59	55 58	syl5com	⊢ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) → ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐸 ) )
60	59	impcom	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐸 )
61	3 7	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐸 ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ 𝐸 )
62	54 60 61	syl2anc	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ 𝐸 )
63	62	3ad2antr1	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ 𝐸 )
64	11	adantr	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → 𝑀 ∈ LMod )
65	1 2 3 4 5 6 7 8 9 10	lincresunit1	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ) → 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) )
66	65	3adantr3	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) )
67		elmapi	⊢ ( 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) → 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 )
68		ffvelcdm	⊢ ( ( 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 )
69	68	ex	⊢ ( 𝐺 : ( 𝑆 ∖ { 𝑋 } ) ⟶ 𝐸 → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 ) )
70	66 67 69	3syl	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 ) )
71	70	imp	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 )
72		elpwi	⊢ ( 𝑆 ∈ 𝒫 𝐵 → 𝑆 ⊆ 𝐵 )
73		eldifi	⊢ ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) → 𝑧 ∈ 𝑆 )
74		ssel2	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝐵 )
75	74	expcom	⊢ ( 𝑧 ∈ 𝑆 → ( 𝑆 ⊆ 𝐵 → 𝑧 ∈ 𝐵 ) )
76	73 75	syl	⊢ ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) → ( 𝑆 ⊆ 𝐵 → 𝑧 ∈ 𝐵 ) )
77	72 76	syl5com	⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) → 𝑧 ∈ 𝐵 ) )
78	77	3ad2ant1	⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) → 𝑧 ∈ 𝐵 ) )
79	78	adantr	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) → 𝑧 ∈ 𝐵 ) )
80	79	imp	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → 𝑧 ∈ 𝐵 )
81	1 2 48 3	lmodvscl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐺 ‘ 𝑧 ) ∈ 𝐸 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 )
82	64 71 80 81	syl3anc	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) ∧ 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 )
83		simp2	⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → 𝑀 ∈ LMod )
84	83 30	jca	⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
85	84	adantr	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
86	1 2 3 4 5 6 7 8 9 10	lincresunit2	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → 𝐺 finSupp 0 )
87	86 5	breqtrdi	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → 𝐺 finSupp ( 0g ‘ 𝑅 ) )
88	2 3	scmfsupp	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ∧ 𝐺 finSupp ( 0g ‘ 𝑅 ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) finSupp ( 0g ‘ 𝑀 ) )
89	88 6	breqtrrdi	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( 𝑆 ∖ { 𝑋 } ) ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐺 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑋 } ) ) ∧ 𝐺 finSupp ( 0g ‘ 𝑅 ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) finSupp 𝑍 )
90	85 66 87 89	syl3anc	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) finSupp 𝑍 )
91	1 2 3 6 47 48 11 51 63 82 90	gsumvsmul	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ( ·𝑠 ‘ 𝑀 ) ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) ) = ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ( ·𝑠 ‘ 𝑀 ) ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) ) )
92	33 46 91	3eqtr2rd	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ( ·𝑠 ‘ 𝑀 ) ( 𝑀 Σg ( 𝑧 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐺 ‘ 𝑧 ) ( ·𝑠 ‘ 𝑀 ) 𝑧 ) ) ) ) = ( ( 𝐹 ↾ ( 𝑆 ∖ { 𝑋 } ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑋 } ) ) )