MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islindf4 Structured version   Visualization version   GIF version

Theorem islindf4 21191
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.
StepHypRef Expression
1 raldifsni 4753 . . . . 5 (∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ (Base‘𝑅)((((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌))
2 simpll1 1212 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ LMod)
3 simprll 777 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 ∈ (Base‘𝑅))
4 ffvelcdm 7029 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐼𝐵𝑗𝐼) → (𝐹𝑗) ∈ 𝐵)
543ad2antl3 1187 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (𝐹𝑗) ∈ 𝐵)
65adantr 481 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹𝑗) ∈ 𝐵)
7 islindf4.b . . . . . . . . . . . . . . . . 17 𝐵 = (Base‘𝑊)
8 islindf4.r . . . . . . . . . . . . . . . . 17 𝑅 = (Scalar‘𝑊)
9 islindf4.t . . . . . . . . . . . . . . . . 17 · = ( ·𝑠𝑊)
10 eqid 2736 . . . . . . . . . . . . . . . . 17 (invg𝑊) = (invg𝑊)
11 eqid 2736 . . . . . . . . . . . . . . . . 17 (invg𝑅) = (invg𝑅)
12 eqid 2736 . . . . . . . . . . . . . . . . 17 (Base‘𝑅) = (Base‘𝑅)
137, 8, 9, 10, 11, 12lmodvsinv 20444 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹𝑗) ∈ 𝐵) → (((invg𝑅)‘𝑙) · (𝐹𝑗)) = ((invg𝑊)‘(𝑙 · (𝐹𝑗))))
142, 3, 6, 13syl3anc 1371 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg𝑅)‘𝑙) · (𝐹𝑗)) = ((invg𝑊)‘(𝑙 · (𝐹𝑗))))
1514eqeq1d 2738 . . . . . . . . . . . . . 14 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((invg𝑊)‘(𝑙 · (𝐹𝑗))) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))))
16 lmodgrp 20276 . . . . . . . . . . . . . . . 16 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
172, 16syl 17 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Grp)
187, 8, 9, 12lmodvscl 20286 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹𝑗) ∈ 𝐵) → (𝑙 · (𝐹𝑗)) ∈ 𝐵)
192, 3, 6, 18syl3anc 1371 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 · (𝐹𝑗)) ∈ 𝐵)
20 islindf4.z . . . . . . . . . . . . . . . 16 0 = (0g𝑊)
21 lmodcmn 20317 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ LMod → 𝑊 ∈ CMnd)
222, 21syl 17 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ CMnd)
23 simpll2 1213 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼𝑋)
24 difexg 5282 . . . . . . . . . . . . . . . . 17 (𝐼𝑋 → (𝐼 ∖ {𝑗}) ∈ V)
2523, 24syl 17 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐼 ∖ {𝑗}) ∈ V)
26 simprlr 778 . . . . . . . . . . . . . . . . . 18 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))
27 elmapi 8745 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅))
2826, 27syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅))
29 simpll3 1214 . . . . . . . . . . . . . . . . . 18 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹:𝐼𝐵)
30 difss 4089 . . . . . . . . . . . . . . . . . 18 (𝐼 ∖ {𝑗}) ⊆ 𝐼
31 fssres 6705 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐼𝐵 ∧ (𝐼 ∖ {𝑗}) ⊆ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵)
3229, 30, 31sylancl 586 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵)
338, 12, 9, 7, 2, 28, 32, 25lcomf 20308 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))):(𝐼 ∖ {𝑗})⟶𝐵)
34 islindf4.y . . . . . . . . . . . . . . . . 17 𝑌 = (0g𝑅)
35 simprr 771 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 finSupp 𝑌)
368, 12, 9, 7, 2, 28, 32, 25, 20, 34, 35lcomfsupp 20309 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) finSupp 0 )
377, 20, 22, 25, 33, 36gsumcl 19645 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵)
38 eqid 2736 . . . . . . . . . . . . . . . 16 (+g𝑊) = (+g𝑊)
397, 38, 20, 10grpinvid2 18756 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Grp ∧ (𝑙 · (𝐹𝑗)) ∈ 𝐵 ∧ (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵) → (((invg𝑊)‘(𝑙 · (𝐹𝑗))) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g𝑊)(𝑙 · (𝐹𝑗))) = 0 ))
4017, 19, 37, 39syl3anc 1371 . . . . . . . . . . . . . 14 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg𝑊)‘(𝑙 · (𝐹𝑗))) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g𝑊)(𝑙 · (𝐹𝑗))) = 0 ))
41 simplr 767 . . . . . . . . . . . . . . . . . . 19 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑗𝐼)
42 fsnunf2 7128 . . . . . . . . . . . . . . . . . . 19 ((𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) ∧ 𝑗𝐼𝑙 ∈ (Base‘𝑅)) → (𝑦 ∪ {⟨𝑗, 𝑙⟩}):𝐼⟶(Base‘𝑅))
4328, 41, 3, 42syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {⟨𝑗, 𝑙⟩}):𝐼⟶(Base‘𝑅))
448, 12, 9, 7, 2, 43, 29, 23lcomf 20308 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹):𝐼𝐵)
45 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → 𝑗𝐼)
46 simpl 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) → 𝑙 ∈ (Base‘𝑅))
4745, 46anim12i 613 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑗𝐼𝑙 ∈ (Base‘𝑅)))
48 elmapfun 8762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → Fun 𝑦)
49 fdm 6674 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) → dom 𝑦 = (𝐼 ∖ {𝑗}))
50 neldifsnd 4751 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (dom 𝑦 = (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ (𝐼 ∖ {𝑗}))
51 df-nel 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ dom 𝑦)
52 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦𝑗 ∈ (𝐼 ∖ {𝑗})))
5352notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (dom 𝑦 = (𝐼 ∖ {𝑗}) → (¬ 𝑗 ∈ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})))
5451, 53bitrid 282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (dom 𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})))
5550, 54mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑦 = (𝐼 ∖ {𝑗}) → 𝑗 ∉ dom 𝑦)
5627, 49, 553syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → 𝑗 ∉ dom 𝑦)
5748, 56jca 512 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → (Fun 𝑦𝑗 ∉ dom 𝑦))
5857adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) → (Fun 𝑦𝑗 ∉ dom 𝑦))
5958adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (Fun 𝑦𝑗 ∉ dom 𝑦))
6047, 59jca 512 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑗𝐼𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦𝑗 ∉ dom 𝑦)))
61 funsnfsupp 9287 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗𝐼𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦𝑗 ∉ dom 𝑦)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌𝑦 finSupp 𝑌))
6261bicomd 222 . . . . . . . . . . . . . . . . . . . . 21 (((𝑗𝐼𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦𝑗 ∉ dom 𝑦)) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌))
6360, 62syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌))
6463biimpd 228 . . . . . . . . . . . . . . . . . . 19 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 → (𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌))
6564impr 455 . . . . . . . . . . . . . . . . . 18 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌)
668, 12, 9, 7, 2, 43, 29, 23, 20, 34, 65lcomfsupp 20309 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) finSupp 0 )
67 disjdifr 4430 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅
6867a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅)
69 difsnid 4768 . . . . . . . . . . . . . . . . . . 19 (𝑗𝐼 → ((𝐼 ∖ {𝑗}) ∪ {𝑗}) = 𝐼)
7069eqcomd 2742 . . . . . . . . . . . . . . . . . 18 (𝑗𝐼𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗}))
7141, 70syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗}))
727, 20, 38, 22, 23, 44, 66, 68, 71gsumsplit 19658 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = ((𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g𝑊)(𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗}))))
73 vex 3447 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
74 snex 5386 . . . . . . . . . . . . . . . . . . . . 21 {⟨𝑗, 𝑙⟩} ∈ V
7573, 74unex 7672 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∈ V
76 simpl3 1193 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → 𝐹:𝐼𝐵)
77 simpl2 1192 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → 𝐼𝑋)
7876, 77fexd 7173 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → 𝐹 ∈ V)
7978adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 ∈ V)
80 offres 7908 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∈ V ∧ 𝐹 ∈ V) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))
8175, 79, 80sylancr 587 . . . . . . . . . . . . . . . . . . 19 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))
8228ffnd 6666 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 Fn (𝐼 ∖ {𝑗}))
83 neldifsn 4750 . . . . . . . . . . . . . . . . . . . . 21 ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})
84 fsnunres 7130 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 Fn (𝐼 ∖ {𝑗}) ∧ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ↾ (𝐼 ∖ {𝑗})) = 𝑦)
8582, 83, 84sylancl 586 . . . . . . . . . . . . . . . . . . . 20 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ↾ (𝐼 ∖ {𝑗})) = 𝑦)
8685oveq1d 7366 . . . . . . . . . . . . . . . . . . 19 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) = (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))
8781, 86eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))
8887oveq2d 7367 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗}))) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))))
8944ffnd 6666 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) Fn 𝐼)
90 fnressn 7100 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) Fn 𝐼𝑗𝐼) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗}) = {⟨𝑗, (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗)⟩})
9189, 41, 90syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗}) = {⟨𝑗, (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗)⟩})
9243ffnd 6666 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {⟨𝑗, 𝑙⟩}) Fn 𝐼)
9329ffnd 6666 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 Fn 𝐼)
94 fnfvof 7626 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑦 ∪ {⟨𝑗, 𝑙⟩}) Fn 𝐼𝐹 Fn 𝐼) ∧ (𝐼𝑋𝑗𝐼)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) · (𝐹𝑗)))
9592, 93, 23, 41, 94syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) · (𝐹𝑗)))
96 fndm 6602 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 Fn (𝐼 ∖ {𝑗}) → dom 𝑦 = (𝐼 ∖ {𝑗}))
9796eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 Fn (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦𝑗 ∈ (𝐼 ∖ {𝑗})))
9883, 97mtbiri 326 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 Fn (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ dom 𝑦)
99 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑗 ∈ V
100 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑙 ∈ V
101 fsnunfv 7129 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ V ∧ 𝑙 ∈ V ∧ ¬ 𝑗 ∈ dom 𝑦) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑙)
10299, 100, 101mp3an12 1451 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗 ∈ dom 𝑦 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑙)
10382, 98, 1023syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑙)
104103oveq1d 7366 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) · (𝐹𝑗)) = (𝑙 · (𝐹𝑗)))
10595, 104eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗) = (𝑙 · (𝐹𝑗)))
106105opeq2d 4835 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ⟨𝑗, (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗)⟩ = ⟨𝑗, (𝑙 · (𝐹𝑗))⟩)
107106sneqd 4596 . . . . . . . . . . . . . . . . . . . 20 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {⟨𝑗, (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)‘𝑗)⟩} = {⟨𝑗, (𝑙 · (𝐹𝑗))⟩})
108 ovex 7384 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 · (𝐹𝑗)) ∈ V
109 fmptsn 7109 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ V ∧ (𝑙 · (𝐹𝑗)) ∈ V) → {⟨𝑗, (𝑙 · (𝐹𝑗))⟩} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹𝑗))))
11099, 108, 109mp2an 690 . . . . . . . . . . . . . . . . . . . . 21 {⟨𝑗, (𝑙 · (𝐹𝑗))⟩} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹𝑗)))
111110a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {⟨𝑗, (𝑙 · (𝐹𝑗))⟩} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹𝑗))))
11291, 107, 1113eqtrd 2780 . . . . . . . . . . . . . . . . . . 19 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗}) = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹𝑗))))
113112oveq2d 7367 . . . . . . . . . . . . . . . . . 18 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗})) = (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹𝑗)))))
114 cmnmnd 19532 . . . . . . . . . . . . . . . . . . . 20 (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
1152, 21, 1143syl 18 . . . . . . . . . . . . . . . . . . 19 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Mnd)
11699a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑗 ∈ V)
117 eqidd 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑗 → (𝑙 · (𝐹𝑗)) = (𝑙 · (𝐹𝑗)))
1187, 117gsumsn 19684 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Mnd ∧ 𝑗 ∈ V ∧ (𝑙 · (𝐹𝑗)) ∈ 𝐵) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹𝑗)))) = (𝑙 · (𝐹𝑗)))
119115, 116, 19, 118syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹𝑗)))) = (𝑙 · (𝐹𝑗)))
120113, 119eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗})) = (𝑙 · (𝐹𝑗)))
12188, 120oveq12d 7369 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g𝑊)(𝑊 Σg (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹) ↾ {𝑗}))) = ((𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g𝑊)(𝑙 · (𝐹𝑗))))
12272, 121eqtr2d 2777 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g𝑊)(𝑙 · (𝐹𝑗))) = (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)))
123122eqeq1d 2738 . . . . . . . . . . . . . 14 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g𝑊)(𝑙 · (𝐹𝑗))) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 ))
12415, 40, 1233bitrd 304 . . . . . . . . . . . . 13 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 ))
125103eqcomd 2742 . . . . . . . . . . . . . 14 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 = ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗))
126125eqeq1d 2738 . . . . . . . . . . . . 13 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 = 𝑌 ↔ ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))
127124, 126imbi12d 344 . . . . . . . . . . . 12 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌)))
128127anassrs 468 . . . . . . . . . . 11 (((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) ∧ 𝑦 finSupp 𝑌) → (((((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌)))
129128pm5.74da 802 . . . . . . . . . 10 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑦 finSupp 𝑌 → ((((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌)) ↔ (𝑦 finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
130 impexp 451 . . . . . . . . . . 11 (((𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (𝑦 finSupp 𝑌 → ((((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌)))
131130a1i 11 . . . . . . . . . 10 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (𝑦 finSupp 𝑌 → ((((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌))))
13263bicomd 222 . . . . . . . . . . 11 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌𝑦 finSupp 𝑌))
133132imbi1d 341 . . . . . . . . . 10 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌)) ↔ (𝑦 finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
134129, 131, 1333bitr4d 310 . . . . . . . . 9 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
1351342ralbidva 3208 . . . . . . . 8 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
136 breq1 5106 . . . . . . . . . . 11 (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → (𝑥 finSupp 𝑌 ↔ (𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌))
137 oveq1 7358 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → (𝑥f · 𝐹) = ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹))
138137oveq2d 7367 . . . . . . . . . . . . 13 (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → (𝑊 Σg (𝑥f · 𝐹)) = (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)))
139138eqeq1d 2738 . . . . . . . . . . . 12 (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → ((𝑊 Σg (𝑥f · 𝐹)) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 ))
140 fveq1 6838 . . . . . . . . . . . . 13 (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → (𝑥𝑗) = ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗))
141140eqeq1d 2738 . . . . . . . . . . . 12 (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → ((𝑥𝑗) = 𝑌 ↔ ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))
142139, 141imbi12d 344 . . . . . . . . . . 11 (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → (((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌)))
143136, 142imbi12d 344 . . . . . . . . . 10 (𝑥 = (𝑦 ∪ {⟨𝑗, 𝑙⟩}) → ((𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌)) ↔ ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
144143ralxpmap 8792 . . . . . . . . 9 (𝑗𝐼 → (∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
145144adantl 482 . . . . . . . 8 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {⟨𝑗, 𝑙⟩}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {⟨𝑗, 𝑙⟩}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {⟨𝑗, 𝑙⟩})‘𝑗) = 𝑌))))
146135, 145bitr4d 281 . . . . . . 7 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌))))
147 breq1 5106 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 finSupp 𝑌𝑥 finSupp 𝑌))
148147ralrab 3649 . . . . . . 7 (∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌)))
149146, 148bitr4di 288 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌)))
150 resima 5969 . . . . . . . . . . . . 13 ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) = (𝐹 “ (𝐼 ∖ {𝑗}))
151150eqcomi 2745 . . . . . . . . . . . 12 (𝐹 “ (𝐼 ∖ {𝑗})) = ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))
152151fveq2i 6842 . . . . . . . . . . 11 ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) = ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})))
153152eleq2i 2829 . . . . . . . . . 10 ((((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))))
154 eqid 2736 . . . . . . . . . . 11 (LSpan‘𝑊) = (LSpan‘𝑊)
15576, 30, 31sylancl 586 . . . . . . . . . . 11 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵)
156 simpl1 1191 . . . . . . . . . . 11 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → 𝑊 ∈ LMod)
157243ad2ant2 1134 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) → (𝐼 ∖ {𝑗}) ∈ V)
158157adantr 481 . . . . . . . . . . 11 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (𝐼 ∖ {𝑗}) ∈ V)
159154, 7, 12, 8, 34, 9, 155, 156, 158ellspd 21155 . . . . . . . . . 10 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → ((((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))))))
160153, 159bitrid 282 . . . . . . . . 9 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → ((((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗})))))))
161160imbi1d 341 . . . . . . . 8 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (((((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌)))
162 r19.23v 3177 . . . . . . . 8 (∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))
163161, 162bitr4di 288 . . . . . . 7 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (((((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌)))
164163ralbidv 3172 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg𝑅)‘𝑙) · (𝐹𝑗)) = (𝑊 Σg (𝑦f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌)))
165 islindf4.l . . . . . . . 8 𝐿 = (Base‘(𝑅 freeLMod 𝐼))
1668fvexi 6853 . . . . . . . . . . 11 𝑅 ∈ V
167 eqid 2736 . . . . . . . . . . . 12 (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼)
168 eqid 2736 . . . . . . . . . . . 12 {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌}
169167, 12, 34, 168frlmbas 21108 . . . . . . . . . . 11 ((𝑅 ∈ V ∧ 𝐼𝑋) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼)))
170166, 169mpan 688 . . . . . . . . . 10 (𝐼𝑋 → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼)))
1711703ad2ant2 1134 . . . . . . . . 9 ((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼)))
172171adantr 481 . . . . . . . 8 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼)))
173165, 172eqtr4id 2795 . . . . . . 7 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → 𝐿 = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌})
174173raleqdv 3311 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌) ↔ ∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌)))
175149, 164, 1743bitr4d 310 . . . . 5 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌)))
1761, 175bitrid 282 . . . 4 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌)))
1778lmodfgrp 20278 . . . . . . . 8 (𝑊 ∈ LMod → 𝑅 ∈ Grp)
17812, 34, 11grpinvnzcl 18772 . . . . . . . 8 ((𝑅 ∈ Grp ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌}))
179177, 178sylan 580 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌}))
18012, 34, 11grpinvnzcl 18772 . . . . . . . . 9 ((𝑅 ∈ Grp ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}))
181177, 180sylan 580 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}))
182 eldifi 4084 . . . . . . . . . 10 (𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) → 𝑘 ∈ (Base‘𝑅))
18312, 11grpinvinv 18767 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ 𝑘 ∈ (Base‘𝑅)) → ((invg𝑅)‘((invg𝑅)‘𝑘)) = 𝑘)
184177, 182, 183syl2an 596 . . . . . . . . 9 ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg𝑅)‘((invg𝑅)‘𝑘)) = 𝑘)
185184eqcomd 2742 . . . . . . . 8 ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → 𝑘 = ((invg𝑅)‘((invg𝑅)‘𝑘)))
186 fveq2 6839 . . . . . . . . 9 (𝑙 = ((invg𝑅)‘𝑘) → ((invg𝑅)‘𝑙) = ((invg𝑅)‘((invg𝑅)‘𝑘)))
187186rspceeqv 3593 . . . . . . . 8 ((((invg𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}) ∧ 𝑘 = ((invg𝑅)‘((invg𝑅)‘𝑘))) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg𝑅)‘𝑙))
188181, 185, 187syl2anc 584 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg𝑅)‘𝑙))
189 oveq1 7358 . . . . . . . . . 10 (𝑘 = ((invg𝑅)‘𝑙) → (𝑘 · (𝐹𝑗)) = (((invg𝑅)‘𝑙) · (𝐹𝑗)))
190189eleq1d 2822 . . . . . . . . 9 (𝑘 = ((invg𝑅)‘𝑙) → ((𝑘 · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
191190notbid 317 . . . . . . . 8 (𝑘 = ((invg𝑅)‘𝑙) → (¬ (𝑘 · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬ (((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
192191adantl 482 . . . . . . 7 ((𝑊 ∈ LMod ∧ 𝑘 = ((invg𝑅)‘𝑙)) → (¬ (𝑘 · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬ (((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
193179, 188, 192ralxfrd 5361 . . . . . 6 (𝑊 ∈ LMod → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
1941933ad2ant1 1133 . . . . 5 ((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
195194adantr 481 . . . 4 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg𝑅)‘𝑙) · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
196 simplr 767 . . . . . . . 8 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ 𝑥𝐿) → 𝑗𝐼)
19734fvexi 6853 . . . . . . . . 9 𝑌 ∈ V
198197fvconst2 7149 . . . . . . . 8 (𝑗𝐼 → ((𝐼 × {𝑌})‘𝑗) = 𝑌)
199196, 198syl 17 . . . . . . 7 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ 𝑥𝐿) → ((𝐼 × {𝑌})‘𝑗) = 𝑌)
200199eqeq2d 2747 . . . . . 6 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ 𝑥𝐿) → ((𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗) ↔ (𝑥𝑗) = 𝑌))
201200imbi2d 340 . . . . 5 ((((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) ∧ 𝑥𝐿) → (((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌)))
202201ralbidva 3170 . . . 4 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = 𝑌)))
203176, 195, 2023bitr4d 310 . . 3 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑗𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗))))
204203ralbidva 3170 . 2 ((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) → (∀𝑗𝐼𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑗𝐼𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗))))
2057, 9, 154, 8, 12, 34islindf2 21167 . 2 ((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑗𝐼𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗})))))
206167, 12, 165frlmbasf 21113 . . . . . . . 8 ((𝐼𝑋𝑥𝐿) → 𝑥:𝐼⟶(Base‘𝑅))
2072063ad2antl2 1186 . . . . . . 7 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑥𝐿) → 𝑥:𝐼⟶(Base‘𝑅))
208207ffnd 6666 . . . . . 6 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑥𝐿) → 𝑥 Fn 𝐼)
209 fnconstg 6727 . . . . . . 7 (𝑌 ∈ V → (𝐼 × {𝑌}) Fn 𝐼)
210197, 209ax-mp 5 . . . . . 6 (𝐼 × {𝑌}) Fn 𝐼
211 eqfnfv 6979 . . . . . 6 ((𝑥 Fn 𝐼 ∧ (𝐼 × {𝑌}) Fn 𝐼) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗𝐼 (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)))
212208, 210, 211sylancl 586 . . . . 5 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑥𝐿) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗𝐼 (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)))
213212imbi2d 340 . . . 4 (((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) ∧ 𝑥𝐿) → (((𝑊 Σg (𝑥f · 𝐹)) = 0𝑥 = (𝐼 × {𝑌})) ↔ ((𝑊 Σg (𝑥f · 𝐹)) = 0 → ∀𝑗𝐼 (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗))))
214213ralbidva 3170 . . 3 ((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) → (∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → ∀𝑗𝐼 (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗))))
215 r19.21v 3174 . . . . 5 (∀𝑗𝐼 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥f · 𝐹)) = 0 → ∀𝑗𝐼 (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)))
216215ralbii 3094 . . . 4 (∀𝑥𝐿𝑗𝐼 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → ∀𝑗𝐼 (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)))
217 ralcom 3270 . . . 4 (∀𝑥𝐿𝑗𝐼 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗𝐼𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)))
218216, 217bitr3i 276 . . 3 (∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → ∀𝑗𝐼 (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗𝐼𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗)))
219214, 218bitrdi 286 . 2 ((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) → (∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑗𝐼𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0 → (𝑥𝑗) = ((𝐼 × {𝑌})‘𝑗))))
220204, 205, 2193bitr4d 310 1 ((𝑊 ∈ LMod ∧ 𝐼𝑋𝐹:𝐼𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑥𝐿 ((𝑊 Σg (𝑥f · 𝐹)) = 0𝑥 = (𝐼 × {𝑌}))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wnel 3047  wral 3062  wrex 3071  {crab 3405  Vcvv 3443  cdif 3905  cun 3906  cin 3907  wss 3908  c0 4280  {csn 4584  cop 4590   class class class wbr 5103  cmpt 5186   × cxp 5629  dom cdm 5631  cres 5633  cima 5634  Fun wfun 6487   Fn wfn 6488  wf 6489  cfv 6493  (class class class)co 7351  f cof 7607  m cmap 8723   finSupp cfsupp 9263  Basecbs 17037  +gcplusg 17087  Scalarcsca 17090   ·𝑠 cvsca 17091  0gc0g 17275   Σg cgsu 17276  Mndcmnd 18510  Grpcgrp 18702  invgcminusg 18703  CMndccmn 19515  LModclmod 20269  LSpanclspn 20379   freeLMod cfrlm 21099   LIndF clindf 21157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-iin 4955  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-of 7609  df-om 7795  df-1st 7913  df-2nd 7914  df-supp 8085  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-1o 8404  df-er 8606  df-map 8725  df-ixp 8794  df-en 8842  df-dom 8843  df-sdom 8844  df-fin 8845  df-fsupp 9264  df-sup 9336  df-oi 9404  df-card 9833  df-pnf 11149  df-mnf 11150  df-xr 11151  df-ltxr 11152  df-le 11153  df-sub 11345  df-neg 11346  df-nn 12112  df-2 12174  df-3 12175  df-4 12176  df-5 12177  df-6 12178  df-7 12179  df-8 12180  df-9 12181  df-n0 12372  df-z 12458  df-dec 12577  df-uz 12722  df-fz 13379  df-fzo 13522  df-seq 13861  df-hash 14185  df-struct 16973  df-sets 16990  df-slot 17008  df-ndx 17020  df-base 17038  df-ress 17067  df-plusg 17100  df-mulr 17101  df-sca 17103  df-vsca 17104  df-ip 17105  df-tset 17106  df-ple 17107  df-ds 17109  df-hom 17111  df-cco 17112  df-0g 17277  df-gsum 17278  df-prds 17283  df-pws 17285  df-mre 17420  df-mrc 17421  df-acs 17423  df-mgm 18451  df-sgrp 18500  df-mnd 18511  df-mhm 18555  df-submnd 18556  df-grp 18705  df-minusg 18706  df-sbg 18707  df-mulg 18826  df-subg 18878  df-ghm 18959  df-cntz 19050  df-cmn 19517  df-abl 19518  df-mgp 19850  df-ur 19867  df-ring 19914  df-subrg 20167  df-lmod 20271  df-lss 20340  df-lsp 20380  df-lmhm 20430  df-lbs 20483  df-sra 20580  df-rgmod 20581  df-nzr 20675  df-dsmm 21085  df-frlm 21100  df-uvc 21136  df-lindf 21159
This theorem is referenced by:  islindf5  21192  islinds5  31998  fedgmul  32162  matunitlindflem1  36006  aacllem  47143
  Copyright terms: Public domain W3C validator