Theorem lincresunit2

Description: Property 2 of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-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	lincresunit2	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → 𝐺 finSupp 0 )

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		difexg	⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
12	11	3ad2ant1	⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
13	12	adantl	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
14	13	adantr	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐹 finSupp 0 ) → ( 𝑆 ∖ { 𝑋 } ) ∈ V )
15		mptexg	⊢ ( ( 𝑆 ∖ { 𝑋 } ) ∈ V → ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ↦ ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑠 ) ) ) ∈ V )
16	10 15	eqeltrid	⊢ ( ( 𝑆 ∖ { 𝑋 } ) ∈ V → 𝐺 ∈ V )
17	14 16	syl	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐹 finSupp 0 ) → 𝐺 ∈ V )
18	10	funmpt2	⊢ Fun 𝐺
19	18	a1i	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐹 finSupp 0 ) → Fun 𝐺 )
20	5	fvexi	⊢ 0 ∈ V
21	20	a1i	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐹 finSupp 0 ) → 0 ∈ V )
22		simpr	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐹 finSupp 0 ) → 𝐹 finSupp 0 )
23	22	fsuppimpd	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐹 finSupp 0 ) → ( 𝐹 supp 0 ) ∈ Fin )
24		simplr	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) )
25		simpll	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) )
26		eldifi	⊢ ( 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) → 𝑠 ∈ 𝑆 )
27	26	adantl	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → 𝑠 ∈ 𝑆 )
28	1 2 3 4 5 6 7 8 9 10	lincresunitlem2	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ) ∧ 𝑠 ∈ 𝑆 ) → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑠 ) ) ∈ 𝐸 )
29	24 25 27 28	syl21anc	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑠 ) ) ∈ 𝐸 )
30	29	ralrimiva	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → ∀ 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑠 ) ) ∈ 𝐸 )
31	10	fnmpt	⊢ ( ∀ 𝑠 ∈ ( 𝑆 ∖ { 𝑋 } ) ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑠 ) ) ∈ 𝐸 → 𝐺 Fn ( 𝑆 ∖ { 𝑋 } ) )
32	30 31	syl	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → 𝐺 Fn ( 𝑆 ∖ { 𝑋 } ) )
33		elmapfn	⊢ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) → 𝐹 Fn 𝑆 )
34	33	adantr	⊢ ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) → 𝐹 Fn 𝑆 )
35	34	adantr	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → 𝐹 Fn 𝑆 )
36	32 35	jca	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → ( 𝐺 Fn ( 𝑆 ∖ { 𝑋 } ) ∧ 𝐹 Fn 𝑆 ) )
37		difssd	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → ( 𝑆 ∖ { 𝑋 } ) ⊆ 𝑆 )
38		simpr1	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → 𝑆 ∈ 𝒫 𝐵 )
39	20	a1i	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → 0 ∈ V )
40	37 38 39	3jca	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → ( ( 𝑆 ∖ { 𝑋 } ) ⊆ 𝑆 ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 0 ∈ V ) )
41		fveq2	⊢ ( 𝑠 = 𝑥 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑥 ) )
42	41	oveq2d	⊢ ( 𝑠 = 𝑥 → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑠 ) ) = ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑥 ) ) )
43		simplr	⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) → 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) )
44		simpllr	⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) → ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) )
45		simpll	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) )
46	45	adantr	⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) → ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) )
47		eldifi	⊢ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) → 𝑥 ∈ 𝑆 )
48	47	adantl	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → 𝑥 ∈ 𝑆 )
49	48	adantr	⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) → 𝑥 ∈ 𝑆 )
50	1 2 3 4 5 6 7 8 9 10	lincresunitlem2	⊢ ( ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐸 )
51	44 46 49 50	syl21anc	⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐸 )
52	10 42 43 51	fvmptd3	⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) → ( 𝐺 ‘ 𝑥 ) = ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑥 ) ) )
53		oveq2	⊢ ( ( 𝐹 ‘ 𝑥 ) = 0 → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · 0 ) )
54	2	lmodring	⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Ring )
55	54	3ad2ant2	⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → 𝑅 ∈ Ring )
56	55	adantl	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → 𝑅 ∈ Ring )
57	1 2 3 4 5 6 7 8 9 10	lincresunitlem1	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ) → ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ 𝐸 )
58	57	ancoms	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ 𝐸 )
59	3 9 5	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ 𝐸 ) → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · 0 ) = 0 )
60	56 58 59	syl2anc	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · 0 ) = 0 )
61	60	adantr	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · 0 ) = 0 )
62	53 61	sylan9eqr	⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) → ( ( 𝐼 ‘ ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) ) · ( 𝐹 ‘ 𝑥 ) ) = 0 )
63	52 62	eqtrd	⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) → ( 𝐺 ‘ 𝑥 ) = 0 )
64	63	ex	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ( 𝐹 ‘ 𝑥 ) = 0 → ( 𝐺 ‘ 𝑥 ) = 0 ) )
65	64	ralrimiva	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → ∀ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ( ( 𝐹 ‘ 𝑥 ) = 0 → ( 𝐺 ‘ 𝑥 ) = 0 ) )
66		suppfnss	⊢ ( ( ( 𝐺 Fn ( 𝑆 ∖ { 𝑋 } ) ∧ 𝐹 Fn 𝑆 ) ∧ ( ( 𝑆 ∖ { 𝑋 } ) ⊆ 𝑆 ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 0 ∈ V ) ) → ( ∀ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ( ( 𝐹 ‘ 𝑥 ) = 0 → ( 𝐺 ‘ 𝑥 ) = 0 ) → ( 𝐺 supp 0 ) ⊆ ( 𝐹 supp 0 ) ) )
67	66	imp	⊢ ( ( ( ( 𝐺 Fn ( 𝑆 ∖ { 𝑋 } ) ∧ 𝐹 Fn 𝑆 ) ∧ ( ( 𝑆 ∖ { 𝑋 } ) ⊆ 𝑆 ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 0 ∈ V ) ) ∧ ∀ 𝑥 ∈ ( 𝑆 ∖ { 𝑋 } ) ( ( 𝐹 ‘ 𝑥 ) = 0 → ( 𝐺 ‘ 𝑥 ) = 0 ) ) → ( 𝐺 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
68	36 40 65 67	syl21anc	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → ( 𝐺 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
69	68	adantr	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐹 finSupp 0 ) → ( 𝐺 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
70		suppssfifsupp	⊢ ( ( ( 𝐺 ∈ V ∧ Fun 𝐺 ∧ 0 ∈ V ) ∧ ( ( 𝐹 supp 0 ) ∈ Fin ∧ ( 𝐺 supp 0 ) ⊆ ( 𝐹 supp 0 ) ) ) → 𝐺 finSupp 0 )
71	17 19 21 23 69 70	syl32anc	⊢ ( ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) ∧ 𝐹 finSupp 0 ) → 𝐺 finSupp 0 )
72	71	ex	⊢ ( ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) ∧ ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ) → ( 𝐹 finSupp 0 → 𝐺 finSupp 0 ) )
73	72	ex	⊢ ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) → ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 finSupp 0 → 𝐺 finSupp 0 ) ) )
74	73	com23	⊢ ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) → ( 𝐹 finSupp 0 → ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → 𝐺 finSupp 0 ) ) )
75	74	3impia	⊢ ( ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) → ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) → 𝐺 finSupp 0 ) )
76	75	impcom	⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝐹 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ∧ 𝐹 finSupp 0 ) ) → 𝐺 finSupp 0 )