Theorem lindslinindimp2lem4 48336

Description: Lemma 4 for lindslinindsimp2 48338. (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 4583	. . . . . . . . . . . . . 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 2734	. . . . . . . . . . 11 ⊢ (Base‘𝑀) = (Base‘𝑀)
15		lindslinind.r	. . . . . . . . . . 11 ⊢ 𝑅 = (Scalar‘𝑀)
16		lindslinind.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝑅)
17		eqid 2734	. . . . . . . . . . 11 ⊢ ( ·𝑠 ‘𝑀) = ( ·𝑠 ‘𝑀)
18		eqid 2734	. . . . . . . . . . 11 ⊢ (+g‘𝑀) = (+g‘𝑀)
19		lindslinind.0	. . . . . . . . . . 11 ⊢ 0 = (0g‘𝑅)
20	14, 15, 16, 17, 18, 19	lincdifsn 48299	. . . . . . . . . 10 ⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥}))) → (𝑓( linC ‘𝑀)𝑆) = ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)))
21	10, 11, 13, 20	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑓( linC ‘𝑀)𝑆) = ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)))
22	21	eqeq1d 2736	. . . . . . . 8 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 ↔ ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = 𝑍))
23		lmodgrp 20833	. . . . . . . . . . 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 8871	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ (𝐵 ↑m 𝑆) → 𝑓:𝑆⟶𝐵)
28		ffvelcdm 7081	. . . . . . . . . . . . . . 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 3958	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑀))
35	34	ad2antll 729	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑥 ∈ (Base‘𝑀))
36	14, 15, 17, 16	lmodvscl 20844	. . . . . . . . . 10 ⊢ ((𝑀 ∈ LMod ∧ (𝑓‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥) ∈ (Base‘𝑀))
37	26, 33, 35, 36	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥) ∈ (Base‘𝑀))
38		difexg 5309	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑉 → (𝑆 ∖ {𝑥}) ∈ V)
39	38	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ∈ V)
40		ssdifss 4120	. . . . . . . . . . . . 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 48334	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑m 𝑆))) → 𝐺 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥})))
53	44, 46, 47, 49, 52	syl13anc 1373	. . . . . . . . . . 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 48335	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 )) → 𝐺 finSupp 0 )
57	44, 55, 11, 56	syl3anc 1372	. . . . . . . . . . 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 48288	. . . . . . . . . 10 ⊢ ((𝑀 ∈ LMod ∧ ((𝑆 ∖ {𝑥}) ∈ V ∧ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀)) ∧ (𝐺 ∈ (𝐵 ↑m (𝑆 ∖ {𝑥})) ∧ 𝐺 finSupp 0 )) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ∈ (Base‘𝑀))
60	26, 43, 58, 59	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ∈ (Base‘𝑀))
61		eqid 2734	. . . . . . . . . 10 ⊢ (invg‘𝑀) = (invg‘𝑀)
62	14, 18, 50, 61	grpinvid2 18979	. . . . . . . . 9 ⊢ ((𝑀 ∈ Grp ∧ ((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥) ∈ (Base‘𝑀) ∧ (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ∈ (Base‘𝑀)) → (((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = 𝑍))
63	25, 37, 60, 62	syl3anc 1372	. . . . . . . 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 2741	. . . . . . . 8 ⊢ (((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)))
66	15	fveq2i 6889	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑅) = (Base‘(Scalar‘𝑀))
67	16, 66	eqtri 2757	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘(Scalar‘𝑀))
68	67	oveq1i 7423	. . . . . . . . . . . 12 ⊢ (𝐵 ↑m (𝑆 ∖ {𝑥})) = ((Base‘(Scalar‘𝑀)) ↑m (𝑆 ∖ {𝑥}))
69	53, 68	eleqtrdi 2843	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝐺 ∈ ((Base‘(Scalar‘𝑀)) ↑m (𝑆 ∖ {𝑥})))
70	39, 41	elpwd 4586	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀))
71	70	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀))
72		lincval 48284	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ LMod ∧ 𝐺 ∈ ((Base‘(Scalar‘𝑀)) ↑m (𝑆 ∖ {𝑥})) ∧ (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀)) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦))))
73	26, 69, 71, 72	syl3anc 1372	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦))))
74	73	eqeq1d 2736	. . . . . . . . 9 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) ↔ (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥))))
75	12	fveq1i 6887	. . . . . . . . . . . . . . . 16 ⊢ (𝐺‘𝑦) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦)
76	75	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → (𝐺‘𝑦) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦))
77		fvres 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (𝑆 ∖ {𝑥}) → ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦) = (𝑓‘𝑦))
78	77	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦) = (𝑓‘𝑦))
79	76, 78	eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ ((((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → (𝐺‘𝑦) = (𝑓‘𝑦))
80	79	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦) = ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))
81	80	mpteq2dva 5222	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦)) = (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦)))
82	81	oveq2d 7429	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠 ‘𝑀)𝑦))) = (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠 ‘𝑀)𝑦))))
83		eqid 2734	. . . . . . . . . . . . 13 ⊢ (invg‘𝑅) = (invg‘𝑅)
84	14, 15, 17, 61, 16, 83, 26, 35, 33	lmodvsneg 20872	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠 ‘𝑀)𝑥))
85	51	eqcomi 2743	. . . . . . . . . . . . . 14 ⊢ ((invg‘𝑅)‘(𝑓‘𝑥)) = 𝑌
86	85	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((invg‘𝑅)‘(𝑓‘𝑥)) = 𝑌)
87	86	oveq1d 7428	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠 ‘𝑀)𝑥) = (𝑌( ·𝑠 ‘𝑀)𝑥))
88	84, 87	eqtrd 2769	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ (𝐵 ↑m 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠 ‘𝑀)𝑥)) = (𝑌( ·𝑠 ‘𝑀)𝑥))
89	82, 88	eqeq12d 2750	. . . . . . . . . 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 1539   ∈ wcel 2107  Vcvv 3463   ∖ cdif 3928   ⊆ wss 3931  𝒫 cpw 4580  {csn 4606   class class class wbr 5123   ↦ cmpt 5205   ↾ cres 5667  ⟶wf 6537  ‘cfv 6541  (class class class)co 7413   ↑_m cmap 8848   finSupp cfsupp 9383  Basecbs 17229  +_gcplusg 17273  Scalarcsca 17276   ·_𝑠 cvsca 17277  0_gc0g 17455   Σ_g cgsu 17456  Grpcgrp 18920  inv_gcminusg 18921  LModclmod 20826   linC clinc 48279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-int 4927  df-iun 4973  df-iin 4974  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-se 5618  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-om 7870  df-1st 7996  df-2nd 7997  df-supp 8168  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-er 8727  df-map 8850  df-en 8968  df-dom 8969  df-sdom 8970  df-fin 8971  df-fsupp 9384  df-oi 9532  df-card 9961  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-nn 12249  df-2 12311  df-n0 12510  df-z 12597  df-uz 12861  df-fz 13530  df-fzo 13677  df-seq 14025  df-hash 14352  df-sets 17183  df-slot 17201  df-ndx 17213  df-base 17230  df-ress 17253  df-plusg 17286  df-0g 17457  df-gsum 17458  df-mre 17600  df-mrc 17601  df-acs 17603  df-mgm 18622  df-sgrp 18701  df-mnd 18717  df-submnd 18766  df-grp 18923  df-minusg 18924  df-mulg 19055  df-cntz 19304  df-cmn 19768  df-abl 19769  df-mgp 20106  df-rng 20118  df-ur 20147  df-ring 20200  df-lmod 20828  df-linc 48281

This theorem is referenced by:  lindslinindsimp2lem5  48337