Theorem islindf4 20984

Description: A family is independent iff it has no nontrivial representations of zero. (Contributed by Stefan O'Rear, 28-Feb-2015.)

Hypotheses

Ref	Expression
islindf4.b	⊢ 𝐵 = (Base‘𝑊)
islindf4.r	⊢ 𝑅 = (Scalar‘𝑊)
islindf4.t	⊢ · = ( ·𝑠 ‘𝑊)
islindf4.z	⊢ 0 = (0g‘𝑊)
islindf4.y	⊢ 𝑌 = (0g‘𝑅)
islindf4.l	⊢ 𝐿 = (Base‘(𝑅 freeLMod 𝐼))

Assertion

Ref	Expression
islindf4	⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌}))))

Distinct variable groups:   𝑥,𝐵   𝑥,𝐹   𝑥,𝐼   𝑥,𝐿   𝑥,𝑅   𝑥, ·   𝑥,𝑊   𝑥,𝑋   𝑥,𝑌   𝑥, 0

Proof of Theorem islindf4

Dummy variables 𝑗 𝑘 𝑙 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		raldifsni 4730	. . . . 5 ⊢ (∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌))
2		simpll1 1208	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ LMod)
3		simprll 777	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 ∈ (Base‘𝑅))
4		ffvelrn 6851	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐼⟶𝐵 ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑗) ∈ 𝐵)
5	4	3ad2antl3 1183	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑗) ∈ 𝐵)
6	5	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹‘𝑗) ∈ 𝐵)
7		islindf4.b	. . . . . . . . . . . . . . . . 17 ⊢ 𝐵 = (Base‘𝑊)
8		islindf4.r	. . . . . . . . . . . . . . . . 17 ⊢ 𝑅 = (Scalar‘𝑊)
9		islindf4.t	. . . . . . . . . . . . . . . . 17 ⊢ · = ( ·𝑠 ‘𝑊)
10		eqid 2823	. . . . . . . . . . . . . . . . 17 ⊢ (invg‘𝑊) = (invg‘𝑊)
11		eqid 2823	. . . . . . . . . . . . . . . . 17 ⊢ (invg‘𝑅) = (invg‘𝑅)
12		eqid 2823	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝑅)
13	7, 8, 9, 10, 11, 12	lmodvsinv 19810	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))))
14	2, 3, 6, 13	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))))
15	14	eqeq1d 2825	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))))
16		lmodgrp 19643	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
17	2, 16	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Grp)
18	7, 8, 9, 12	lmodvscl 19653	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵)
19	2, 3, 6, 18	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵)
20		islindf4.z	. . . . . . . . . . . . . . . 16 ⊢ 0 = (0g‘𝑊)
21		lmodcmn 19684	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd)
22	2, 21	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ CMnd)
23		simpll2 1209	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 ∈ 𝑋)
24		difexg 5233	. . . . . . . . . . . . . . . . 17 ⊢ (𝐼 ∈ 𝑋 → (𝐼 ∖ {𝑗}) ∈ V)
25	23, 24	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐼 ∖ {𝑗}) ∈ V)
26		simprlr 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))
27		elmapi 8430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅))
28	26, 27	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅))
29		simpll3 1210	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹:𝐼⟶𝐵)
30		difss 4110	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∖ {𝑗}) ⊆ 𝐼
31		fssres 6546	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐼⟶𝐵 ∧ (𝐼 ∖ {𝑗}) ⊆ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵)
32	29, 30, 31	sylancl 588	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵)
33	8, 12, 9, 7, 2, 28, 32, 25	lcomf 19675	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))):(𝐼 ∖ {𝑗})⟶𝐵)
34		islindf4.y	. . . . . . . . . . . . . . . . 17 ⊢ 𝑌 = (0g‘𝑅)
35		simprr 771	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 finSupp 𝑌)
36	8, 12, 9, 7, 2, 28, 32, 25, 20, 34, 35	lcomfsupp 19676	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) finSupp 0 )
37	7, 20, 22, 25, 33, 36	gsumcl 19037	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵)
38		eqid 2823	. . . . . . . . . . . . . . . 16 ⊢ (+g‘𝑊) = (+g‘𝑊)
39	7, 38, 20, 10	grpinvid2 18157	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Grp ∧ (𝑙 · (𝐹‘𝑗)) ∈ 𝐵 ∧ (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵) → (((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 ))
40	17, 19, 37, 39	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 ))
41		simplr 767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑗 ∈ 𝐼)
42		fsnunf2 6950	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) ∧ 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) → (𝑦 ∪ {⟨𝑗, 𝑙⟩}):𝐼⟶(Base‘𝑅))
43	28, 41, 3, 42	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {⟨𝑗, 𝑙⟩}):𝐼⟶(Base‘𝑅))
44	8, 12, 9, 7, 2, 43, 29, 23	lcomf 19675	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹):𝐼⟶𝐵)
45		simpr 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼)
46		simpl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) → 𝑙 ∈ (Base‘𝑅))
47	45, 46	anim12i 614	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)))
48		elmapfun 8432	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → Fun 𝑦)
49		fdm 6524	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) → dom 𝑦 = (𝐼 ∖ {𝑗}))
50		neldifsnd 4728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (dom 𝑦 = (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ (𝐼 ∖ {𝑗}))
51		df-nel 3126	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ dom 𝑦)
52		eleq2 2903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (dom 𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗})))
53	52	notbid 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (dom 𝑦 = (𝐼 ∖ {𝑗}) → (¬ 𝑗 ∈ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})))
54	51, 53	syl5bb 285	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (dom 𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})))
55	50, 54	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑦 = (𝐼 ∖ {𝑗}) → 𝑗 ∉ dom 𝑦)
56	27, 49, 55	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → 𝑗 ∉ dom 𝑦)
57	48, 56	jca 514	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦))
58	57	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦))
59	58	adantl 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦))
60	47, 59	jca 514	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)))
61		funsnfsupp 8859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌))
62	61	bicomd 225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌))
63	60, 62	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌))
64	63	biimpd 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 → (𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌))
65	64	impr 457	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌)
66	8, 12, 9, 7, 2, 43, 29, 23, 20, 34, 65	lcomfsupp 19676	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) finSupp 0 )
67		incom 4180	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ({𝑗} ∩ (𝐼 ∖ {𝑗}))
68		disjdif 4423	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑗} ∩ (𝐼 ∖ {𝑗})) = ∅
69	67, 68	eqtri 2846	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅
70	69	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅)
71		difsnid 4745	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ 𝐼 → ((𝐼 ∖ {𝑗}) ∪ {𝑗}) = 𝐼)
72	71	eqcomd 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ 𝐼 → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗}))
73	41, 72	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗}))
74	7, 20, 38, 22, 23, 44, 66, 70, 73	gsumsplit 19050	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = ((𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗}))))
75		vex 3499	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
76		snex 5334	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {⟨𝑗, 𝑙⟩} ∈ V
77	75, 76	unex 7471	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∈ V
78		simpl3 1189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹:𝐼⟶𝐵)
79		simpl2 1188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ 𝑋)
80		fex 6991	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:𝐼⟶𝐵 ∧ 𝐼 ∈ 𝑋) → 𝐹 ∈ V)
81	78, 79, 80	syl2anc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹 ∈ V)
82	81	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 ∈ V)
83		offres 7686	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∈ V ∧ 𝐹 ∈ V) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))
84	77, 82, 83	sylancr 589	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))
85	28	ffnd 6517	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 Fn (𝐼 ∖ {𝑗}))
86		neldifsn 4727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})
87		fsnunres 6952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 Fn (𝐼 ∖ {𝑗}) ∧ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ↾ (𝐼 ∖ {𝑗})) = 𝑦)
88	85, 86, 87	sylancl 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ↾ (𝐼 ∖ {𝑗})) = 𝑦)
89	88	oveq1d 7173	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) = (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))
90	84, 89	eqtrd 2858	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))
91	90	oveq2d 7174	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗}))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))))
92	44	ffnd 6517	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) Fn 𝐼)
93		fnressn 6922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) Fn 𝐼 ∧ 𝑗 ∈ 𝐼) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗}) = {⟨𝑗, (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗)⟩})
94	92, 41, 93	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗}) = {⟨𝑗, (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗)⟩})
95	43	ffnd 6517	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {⟨𝑗, 𝑙⟩}) Fn 𝐼)
96	29	ffnd 6517	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 Fn 𝐼)
97		fnfvof 7425	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∪ {⟨𝑗, 𝑙⟩}) Fn 𝐼 ∧ 𝐹 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑗 ∈ 𝐼)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) · (𝐹‘𝑗)))
98	95, 96, 23, 41, 97	syl22anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) · (𝐹‘𝑗)))
99		fndm 6457	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → dom 𝑦 = (𝐼 ∖ {𝑗}))
100	99	eleq2d 2900	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗})))
101	86, 100	mtbiri 329	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ dom 𝑦)
102		vex 3499	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑗 ∈ V
103		vex 3499	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑙 ∈ V
104		fsnunfv 6951	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ V ∧ 𝑙 ∈ V ∧ ¬ 𝑗 ∈ dom 𝑦) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑙)
105	102, 103, 104	mp3an12 1447	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑗 ∈ dom 𝑦 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑙)
106	85, 101, 105	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑙)
107	106	oveq1d 7173	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗)))
108	98, 107	eqtrd 2858	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗) = (𝑙 · (𝐹‘𝑗)))
109	108	opeq2d 4812	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ⟨𝑗, (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗)⟩ = ⟨𝑗, (𝑙 · (𝐹‘𝑗))⟩)
110	109	sneqd 4581	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {⟨𝑗, (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗)⟩} = {⟨𝑗, (𝑙 · (𝐹‘𝑗))⟩})
111		ovex 7191	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑙 · (𝐹‘𝑗)) ∈ V
112		fmptsn 6931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ V ∧ (𝑙 · (𝐹‘𝑗)) ∈ V) → {⟨𝑗, (𝑙 · (𝐹‘𝑗))⟩} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))))
113	102, 111, 112	mp2an 690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {⟨𝑗, (𝑙 · (𝐹‘𝑗))⟩} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {⟨𝑗, (𝑙 · (𝐹‘𝑗))⟩} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))))
115	94, 110, 114	3eqtrd 2862	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗}) = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))))
116	115	oveq2d 7174	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗})) = (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))))
117		cmnmnd 18924	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
118	2, 21, 117	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Mnd)
119	102	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑗 ∈ V)
120		eqidd 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑗 → (𝑙 · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗)))
121	7, 120	gsumsn 19076	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Mnd ∧ 𝑗 ∈ V ∧ (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗)))
122	118, 119, 19, 121	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗)))
123	116, 122	eqtrd 2858	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗})) = (𝑙 · (𝐹‘𝑗)))
124	91, 123	oveq12d 7176	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗}))) = ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))))
125	74, 124	eqtr2d 2859	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)))
126	125	eqeq1d 2825	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 ))
127	15, 40, 126	3bitrd 307	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 ))
128	106	eqcomd 2829	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 = ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗))
129	128	eqeq1d 2825	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 = 𝑌 ↔ ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))
130	127, 129	imbi12d 347	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌)))
131	130	anassrs 470	. . . . . . . . . . 11 ⊢ (((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) ∧ 𝑦 finSupp 𝑌) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌)))
132	131	pm5.74da 802	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌)) ↔ (𝑦 finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
133		impexp 453	. . . . . . . . . . 11 ⊢ (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌)))
134	133	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌))))
135	63	bicomd 225	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌))
136	135	imbi1d 344	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌)) ↔ (𝑦 finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
137	132, 134, 136	3bitr4d 313	. . . . . . . . 9 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
138	137	2ralbidva 3200	. . . . . . . 8 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
139		breq1 5071	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → (𝑥 finSupp 𝑌 ↔ (𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌))
140		oveq1 7165	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → (𝑥 ∘f · 𝐹) = ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹))
141	140	oveq2d 7174	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → (𝑊 Σg (𝑥 ∘f · 𝐹)) = (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)))
142	141	eqeq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 ))
143		fveq1 6671	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → (𝑥‘𝑗) = ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗))
144	143	eqeq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → ((𝑥‘𝑗) = 𝑌 ↔ ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))
145	142, 144	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌)))
146	139, 145	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → ((𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
147	146	ralxpmap 8462	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝐼 → (∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
148	147	adantl 484	. . . . . . . 8 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
149	138, 148	bitr4d 284	. . . . . . 7 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))))
150		breq1 5071	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 finSupp 𝑌 ↔ 𝑥 finSupp 𝑌))
151	150	ralrab 3687	. . . . . . 7 ⊢ (∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))
152	149, 151	syl6bbr 291	. . . . . 6 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))
153		resima 5889	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) = (𝐹 “ (𝐼 ∖ {𝑗}))
154	153	eqcomi 2832	. . . . . . . . . . . 12 ⊢ (𝐹 “ (𝐼 ∖ {𝑗})) = ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))
155	154	fveq2i 6675	. . . . . . . . . . 11 ⊢ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) = ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})))
156	155	eleq2i 2906	. . . . . . . . . 10 ⊢ ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))))
157		eqid 2823	. . . . . . . . . . 11 ⊢ (LSpan‘𝑊) = (LSpan‘𝑊)
158	78, 30, 31	sylancl 588	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵)
159		simpl1 1187	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝑊 ∈ LMod)
160	24	3ad2ant2 1130	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐼 ∖ {𝑗}) ∈ V)
161	160	adantr 483	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐼 ∖ {𝑗}) ∈ V)
162	157, 7, 12, 8, 34, 9, 158, 159, 161	ellspd 20948	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))))))
163	156, 162	syl5bb 285	. . . . . . . . 9 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))))))
164	163	imbi1d 344	. . . . . . . 8 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌)))
165		r19.23v 3281	. . . . . . . 8 ⊢ (∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))
166	164, 165	syl6bbr 291	. . . . . . 7 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌)))
167	166	ralbidv 3199	. . . . . 6 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌)))
168	8	fvexi 6686	. . . . . . . . . . 11 ⊢ 𝑅 ∈ V
169		eqid 2823	. . . . . . . . . . . 12 ⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼)
170		eqid 2823	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌}
171	169, 12, 34, 170	frlmbas 20901	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ V ∧ 𝐼 ∈ 𝑋) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼)))
172	168, 171	mpan 688	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑋 → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼)))
173	172	3ad2ant2 1130	. . . . . . . . 9 ⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼)))
174	173	adantr 483	. . . . . . . 8 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼)))
175		islindf4.l	. . . . . . . 8 ⊢ 𝐿 = (Base‘(𝑅 freeLMod 𝐼))
176	174, 175	syl6reqr 2877	. . . . . . 7 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐿 = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌})
177	176	raleqdv 3417	. . . . . 6 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))
178	152, 167, 177	3bitr4d 313	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))
179	1, 178	syl5bb 285	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))
180	8	lmodfgrp 19645	. . . . . . . 8 ⊢ (𝑊 ∈ LMod → 𝑅 ∈ Grp)
181	12, 34, 11	grpinvnzcl 18173	. . . . . . . 8 ⊢ ((𝑅 ∈ Grp ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌}))
182	180, 181	sylan 582	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌}))
183	12, 34, 11	grpinvnzcl 18173	. . . . . . . . 9 ⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}))
184	180, 183	sylan 582	. . . . . . . 8 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}))
185		eldifi 4105	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) → 𝑘 ∈ (Base‘𝑅))
186	12, 11	grpinvinv 18168	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ (Base‘𝑅)) → ((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘)
187	180, 185, 186	syl2an 597	. . . . . . . . 9 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘)
188	187	eqcomd 2829	. . . . . . . 8 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘)))
189		fveq2 6672	. . . . . . . . 9 ⊢ (𝑙 = ((invg‘𝑅)‘𝑘) → ((invg‘𝑅)‘𝑙) = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘)))
190	189	rspceeqv 3640	. . . . . . . 8 ⊢ ((((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}) ∧ 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙))
191	184, 188, 190	syl2anc 586	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙))
192		oveq1 7165	. . . . . . . . . 10 ⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (𝑘 · (𝐹‘𝑗)) = (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)))
193	192	eleq1d 2899	. . . . . . . . 9 ⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → ((𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
194	193	notbid 320	. . . . . . . 8 ⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
195	194	adantl 484	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 = ((invg‘𝑅)‘𝑙)) → (¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
196	182, 191, 195	ralxfrd 5311	. . . . . 6 ⊢ (𝑊 ∈ LMod → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
197	196	3ad2ant1 1129	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
198	197	adantr 483	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
199		simplr 767	. . . . . . . 8 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → 𝑗 ∈ 𝐼)
200	34	fvexi 6686	. . . . . . . . 9 ⊢ 𝑌 ∈ V
201	200	fvconst2 6968	. . . . . . . 8 ⊢ (𝑗 ∈ 𝐼 → ((𝐼 × {𝑌})‘𝑗) = 𝑌)
202	199, 201	syl 17	. . . . . . 7 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝐼 × {𝑌})‘𝑗) = 𝑌)
203	202	eqeq2d 2834	. . . . . 6 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗) ↔ (𝑥‘𝑗) = 𝑌))
204	203	imbi2d 343	. . . . 5 ⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))
205	204	ralbidva 3198	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))
206	179, 198, 205	3bitr4d 313	. . 3 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))))
207	206	ralbidva 3198	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))))
208	7, 9, 157, 8, 12, 34	islindf2 20960	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
209	169, 12, 175	frlmbasf 20906	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅))
210	209	3ad2antl2 1182	. . . . . . 7 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅))
211	210	ffnd 6517	. . . . . 6 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥 Fn 𝐼)
212		fnconstg 6569	. . . . . . 7 ⊢ (𝑌 ∈ V → (𝐼 × {𝑌}) Fn 𝐼)
213	200, 212	ax-mp 5	. . . . . 6 ⊢ (𝐼 × {𝑌}) Fn 𝐼
214		eqfnfv 6804	. . . . . 6 ⊢ ((𝑥 Fn 𝐼 ∧ (𝐼 × {𝑌}) Fn 𝐼) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))
215	211, 213, 214	sylancl 588	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))
216	215	imbi2d 343	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))))
217	216	ralbidva 3198	. . 3 ⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))))
218		r19.21v 3177	. . . . 5 ⊢ (∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))
219	218	ralbii 3167	. . . 4 ⊢ (∀𝑥 ∈ 𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))
220		ralcom 3356	. . . 4 ⊢ (∀𝑥 ∈ 𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))
221	219, 220	bitr3i 279	. . 3 ⊢ (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))
222	217, 221	syl6bb 289	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))))
223	207, 208, 222	3bitr4d 313	1 ⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌}))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ∉ wnel 3125  ∀wral 3140  ∃wrex 3141  {crab 3144  Vcvv 3496   ∖ cdif 3935   ∪ cun 3936   ∩ cin 3937   ⊆ wss 3938  ∅c0 4293  {csn 4569  ⟨cop 4575   class class class wbr 5068   ↦ cmpt 5148   × cxp 5555  dom cdm 5557   ↾ cres 5559   “ cima 5560  Fun wfun 6351   Fn wfn 6352  ⟶wf 6353  ‘cfv 6357  (class class class)co 7158   ∘_f cof 7409   ↑_m cmap 8408   finSupp cfsupp 8835  Basecbs 16485  +_gcplusg 16567  Scalarcsca 16570   ·_𝑠 cvsca 16571  0_gc0g 16715   Σ_g cgsu 16716  Mndcmnd 17913  Grpcgrp 18105  inv_gcminusg 18106  CMndccmn 18908  LModclmod 19636  LSpanclspn 19745   freeLMod cfrlm 20892   LIndF clindf 20950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-iin 4924  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-se 5517  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-isom 6366  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-of 7411  df-om 7583  df-1st 7691  df-2nd 7692  df-supp 7833  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-oadd 8108  df-er 8291  df-map 8410  df-ixp 8464  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-fsupp 8836  df-sup 8908  df-oi 8976  df-card 9370  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-z 11985  df-dec 12102  df-uz 12247  df-fz 12896  df-fzo 13037  df-seq 13373  df-hash 13694  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-sca 16583  df-vsca 16584  df-ip 16585  df-tset 16586  df-ple 16587  df-ds 16589  df-hom 16591  df-cco 16592  df-0g 16717  df-gsum 16718  df-prds 16723  df-pws 16725  df-mre 16859  df-mrc 16860  df-acs 16862  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-mhm 17958  df-submnd 17959  df-grp 18108  df-minusg 18109  df-sbg 18110  df-mulg 18227  df-subg 18278  df-ghm 18358  df-cntz 18449  df-cmn 18910  df-abl 18911  df-mgp 19242  df-ur 19254  df-ring 19301  df-subrg 19535  df-lmod 19638  df-lss 19706  df-lsp 19746  df-lmhm 19796  df-lbs 19849  df-sra 19946  df-rgmod 19947  df-nzr 20033  df-dsmm 20878  df-frlm 20893  df-uvc 20929  df-lindf 20952

This theorem is referenced by:  islindf5  20985  islinds5  30934  fedgmul  31029  matunitlindflem1  34890  aacllem  44909