Theorem lindslinindimp2lem4 48466

Description: Lemma 4 for lindslinindsimp2 48468. (Contributed by AV, 25-Apr-2019.) (Revised by AV, 30-Jul-2019.) (Proof shortened by II, 16-Feb-2023.)

Hypotheses

Ref	Expression
lindslinind.r	⊢ 𝑅 = (Scalar‘𝑀)
lindslinind.b	⊢ 𝐵 = (Base‘𝑅)
lindslinind.0	⊢ 0 = (0g‘𝑅)
lindslinind.z	⊢ 𝑍 = (0g‘𝑀)
lindslinind.y	⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥))
lindslinind.g	⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥}))

Assertion

Ref	Expression
lindslinindimp2lem4	⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥))

Distinct variable groups:   𝐵,𝑓,𝑦   𝑓,𝑀,𝑦   𝑅,𝑓,𝑥   𝑆,𝑓,𝑥,𝑦   𝑦,𝑉   𝑓,𝑍,𝑦   0 ,𝑓,𝑥,𝑦   𝑦,𝐺

Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑦)   𝐺(𝑥,𝑓)   𝑀(𝑥)   𝑉(𝑥,𝑓)   𝑌(𝑥,𝑦,𝑓)   𝑍(𝑥)

Proof of Theorem lindslinindimp2lem4

Step	Hyp	Ref	Expression
1		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → 𝑀 ∈ LMod)
2	1	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → 𝑀 ∈ LMod)
3		simprl 770	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → 𝑆 ⊆ (Base‘𝑀))
4		elpwg 4556	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ 𝒫 (Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀)))
5	4	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∈ 𝒫 (Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀)))
6	3, 5	mpbird 257	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → 𝑆 ∈ 𝒫 (Base‘𝑀))
7		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
8	7	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → 𝑥 ∈ 𝑆)
9	2, 6, 8	3jca 1128	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))
10	9	adantl 481	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))
11		simpl 482	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ))
12		lindslinind.g	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥}))
13	12	a1i 11	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥})))
14		eqid 2729	. . . . . . . . . . 11 ⊢ (Base‘𝑀) = (Base‘𝑀)
15		lindslinind.r	. . . . . . . . . . 11 ⊢ 𝑅 = (Scalar‘𝑀)
16		lindslinind.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝑅)
17		eqid 2729	. . . . . . . . . . 11 ⊢ ( ·𝑠 ‘𝑀) = ( ·𝑠 ‘𝑀)
18		eqid 2729	. . . . . . . . . . 11 ⊢ (+g‘𝑀) = (+g‘𝑀)
19		lindslinind.0	. . . . . . . . . . 11 ⊢ 0 = (0g‘𝑅)
20	14, 15, 16, 17, 18, 19	lincdifsn 48429	. . . . . . . . . 10 ⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥}))) → (𝑓( linC ‘𝑀)𝑆) = ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)))
21	10, 11, 13, 20	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑓( linC ‘𝑀)𝑆) = ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)))
22	21	eqeq1d 2731	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 ↔ ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = 𝑍))
23		lmodgrp 20789	. . . . . . . . . . 11 ⊢ (𝑀 ∈ LMod → 𝑀 ∈ Grp)
24	23	adantl 481	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → 𝑀 ∈ Grp)
25	24	ad2antrl 728	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑀 ∈ Grp)
26	1	ad2antrl 728	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑀 ∈ LMod)
27		elmapi 8783	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ (𝐵 ↑m 𝑆) → 𝑓:𝑆⟶𝐵)
28		ffvelcdm 7019	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:𝑆⟶𝐵 ∧ 𝑥 ∈ 𝑆) → (𝑓‘𝑥) ∈ 𝐵)
29	28	expcom 413	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑆 → (𝑓:𝑆⟶𝐵 → (𝑓‘𝑥) ∈ 𝐵))
30	29	ad2antll 729	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓:𝑆⟶𝐵 → (𝑓‘𝑥) ∈ 𝐵))
31	27, 30	syl5com 31	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (𝐵 ↑m 𝑆) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓‘𝑥) ∈ 𝐵))
32	31	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓‘𝑥) ∈ 𝐵))
33	32	imp 406	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑓‘𝑥) ∈ 𝐵)
34		ssel2 3932	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑀))
35	34	ad2antll 729	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑥 ∈ (Base‘𝑀))
36	14, 15, 17, 16	lmodvscl 20800	. . . . . . . . . 10 ⊢ ((𝑀 ∈ LMod ∧ (𝑓‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥) ∈ (Base‘𝑀))
37	26, 33, 35, 36	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥) ∈ (Base‘𝑀))
38		difexg 5271	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑉 → (𝑆 ∖ {𝑥}) ∈ V)
39	38	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ∈ V)
40		ssdifss 4093	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ (Base‘𝑀) → (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀))
41	40	ad2antrl 728	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀))
42	39, 41	jca 511	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑆 ∖ {𝑥}) ∈ V ∧ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀)))
43	42	adantl 481	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑆 ∖ {𝑥}) ∈ V ∧ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀)))
44		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod))
45		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ (Base‘𝑀))
46	45	ad2antll 729	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑆 ⊆ (Base‘𝑀))
47	7	ad2antll 729	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑥 ∈ 𝑆)
48		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) → 𝑓 ∈ (𝐵 ↑m 𝑆))
49	48	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑓 ∈ (𝐵 ↑m 𝑆))
50		lindslinind.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (0g‘𝑀)
51		lindslinind.y	. . . . . . . . . . . . 13 ⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥))
52	15, 16, 19, 50, 51, 12	lindslinindimp2lem2 48464	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑m 𝑆))) → 𝐺 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥})))
53	44, 46, 47, 49, 52	syl13anc 1374	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝐺 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥})))
54		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))
55	54	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))
56	15, 16, 19, 50, 51, 12	lindslinindimp2lem3 48465	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 )) → 𝐺 finSupp 0 )
57	44, 55, 11, 56	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝐺 finSupp 0 )
58	53, 57	jca 511	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝐺 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥})) ∧ 𝐺 finSupp 0 ))
59	14, 15, 16, 19	lincfsuppcl 48418	. . . . . . . . . 10 ⊢ ((𝑀 ∈ LMod ∧ ((𝑆 ∖ {𝑥}) ∈ V ∧ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀)) ∧ (𝐺 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥})) ∧ 𝐺 finSupp 0 )) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ∈ (Base‘𝑀))
60	26, 43, 58, 59	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ∈ (Base‘𝑀))
61		eqid 2729	. . . . . . . . . 10 ⊢ (invg‘𝑀) = (invg‘𝑀)
62	14, 18, 50, 61	grpinvid2 18890	. . . . . . . . 9 ⊢ ((𝑀 ∈ Grp ∧ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥) ∈ (Base‘𝑀) ∧ (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ∈ (Base‘𝑀)) → (((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = 𝑍))
63	25, 37, 60, 62	syl3anc 1373	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = 𝑍))
64	22, 63	bitr4d 282	. . . . . . 7 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 ↔ ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))))
65		eqcom 2736	. . . . . . . 8 ⊢ (((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)))
66	15	fveq2i 6829	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑅) = (Base‘(Scalar‘𝑀))
67	16, 66	eqtri 2752	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘(Scalar‘𝑀))
68	67	oveq1i 7363	. . . . . . . . . . . 12 ⊢ (𝐵 ↑m (𝑆 ∖ {𝑥})) = ((Base‘(Scalar‘𝑀)) ↑m (𝑆 ∖ {𝑥}))
69	53, 68	eleqtrdi 2838	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝐺 ∈ ((Base‘(Scalar‘𝑀)) ↑m (𝑆 ∖ {𝑥})))
70	39, 41	elpwd 4559	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀))
71	70	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀))
72		lincval 48414	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ LMod ∧ 𝐺 ∈ ((Base‘(Scalar‘𝑀)) ↑m (𝑆 ∖ {𝑥})) ∧ (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀)) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦))))
73	26, 69, 71, 72	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦))))
74	73	eqeq1d 2731	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) ↔ (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))))
75	12	fveq1i 6827	. . . . . . . . . . . . . . . 16 ⊢ (𝐺‘𝑦) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦)
76	75	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → (𝐺‘𝑦) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦))
77		fvres 6845	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (𝑆 ∖ {𝑥}) → ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦) = (𝑓‘𝑦))
78	77	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦) = (𝑓‘𝑦))
79	76, 78	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ ((((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → (𝐺‘𝑦) = (𝑓‘𝑦))
80	79	oveq1d 7368	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦) = ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))
81	80	mpteq2dva 5188	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦)) = (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦)))
82	81	oveq2d 7369	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))))
83		eqid 2729	. . . . . . . . . . . . 13 ⊢ (invg‘𝑅) = (invg‘𝑅)
84	14, 15, 17, 61, 16, 83, 26, 35, 33	lmodvsneg 20828	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠 ‘𝑀)𝑥))
85	51	eqcomi 2738	. . . . . . . . . . . . . 14 ⊢ ((invg‘𝑅)‘(𝑓‘𝑥)) = 𝑌
86	85	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((invg‘𝑅)‘(𝑓‘𝑥)) = 𝑌)
87	86	oveq1d 7368	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠 ‘𝑀)𝑥) = (𝑌( ·𝑠 ‘𝑀)𝑥))
88	84, 87	eqtrd 2764	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (𝑌( ·𝑠 ‘𝑀)𝑥))
89	82, 88	eqeq12d 2745	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) ↔ (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥)))
90	89	biimpd 229	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥)))
91	74, 90	sylbid 240	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥)))
92	65, 91	biimtrid 242	. . . . . . 7 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥)))
93	64, 92	sylbid 240	. . . . . 6 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥)))
94	93	ex 412	. . . . 5 ⊢ ((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥))))
95	94	com23 86	. . . 4 ⊢ ((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥))))
96	95	3impia 1117	. . 3 ⊢ ((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥)))
97	96	com12 32	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥)))
98	97	3impia 1117	1 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑌( ·𝑠 ‘𝑀)𝑥))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  Vcvv 3438   ∖ cdif 3902   ⊆ wss 3905  𝒫 cpw 4553  {csn 4579   class class class wbr 5095   ↦ cmpt 5176   ↾ cres 5625  ⟶wf 6482  ‘cfv 6486  (class class class)co 7353   ↑_m cmap 8760   finSupp cfsupp 9270  Basecbs 17139  +_gcplusg 17180  Scalarcsca 17183   ·_𝑠 cvsca 17184  0_gc0g 17362   Σ_g cgsu 17363  Grpcgrp 18831  inv_gcminusg 18832  LModclmod 20782   linC clinc 48409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-iin 4947  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7617  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8632  df-map 8762  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9271  df-oi 9421  df-card 9854  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-nn 12148  df-2 12210  df-n0 12404  df-z 12491  df-uz 12755  df-fz 13430  df-fzo 13577  df-seq 13928  df-hash 14257  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17140  df-ress 17161  df-plusg 17193  df-0g 17364  df-gsum 17365  df-mre 17507  df-mrc 17508  df-acs 17510  df-mgm 18533  df-sgrp 18612  df-mnd 18628  df-submnd 18677  df-grp 18834  df-minusg 18835  df-mulg 18966  df-cntz 19215  df-cmn 19680  df-abl 19681  df-mgp 20045  df-rng 20057  df-ur 20086  df-ring 20139  df-lmod 20784  df-linc 48411

This theorem is referenced by:  lindslinindsimp2lem5  48467