| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | raldifsni 4794 | . . . . 5
⊢
(∀𝑙 ∈
((Base‘𝑅) ∖
{𝑌}) ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌)) | 
| 2 |  | simpll1 1212 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ LMod) | 
| 3 |  | simprll 778 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 ∈ (Base‘𝑅)) | 
| 4 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐼⟶𝐵 ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑗) ∈ 𝐵) | 
| 5 | 4 | 3ad2antl3 1187 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑗) ∈ 𝐵) | 
| 6 | 5 | adantr 480 | . . . . . . . . . . . . . . . 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‘𝑅) | 
| 13 | 7, 8, 9, 10, 11, 12 | lmodvsinv 21036 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗)))) | 
| 14 | 2, 3, 6, 13 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗)))) | 
| 15 | 14 | eqeq1d 2738 | . . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))))) | 
| 16 |  | lmodgrp 20866 | . . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | 
| 17 | 2, 16 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Grp) | 
| 18 | 7, 8, 9, 12 | lmodvscl 20877 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) | 
| 19 | 2, 3, 6, 18 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) | 
| 20 |  | islindf4.z | . . . . . . . . . . . . . . . 16
⊢  0 =
(0g‘𝑊) | 
| 21 |  | lmodcmn 20909 | . . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd) | 
| 22 | 2, 21 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ CMnd) | 
| 23 |  | simpll2 1213 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 ∈ 𝑋) | 
| 24 |  | difexg 5328 | . . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑋 → (𝐼 ∖ {𝑗}) ∈ V) | 
| 25 | 23, 24 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐼 ∖ {𝑗}) ∈ V) | 
| 26 |  | simprlr 779 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) | 
| 27 |  | elmapi 8890 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅)) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅)) | 
| 29 |  | simpll3 1214 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹:𝐼⟶𝐵) | 
| 30 |  | difss 4135 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∖ {𝑗}) ⊆ 𝐼 | 
| 31 |  | fssres 6773 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐼⟶𝐵 ∧ (𝐼 ∖ {𝑗}) ⊆ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) | 
| 32 | 29, 30, 31 | sylancl 586 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) | 
| 33 | 8, 12, 9, 7, 2, 28,
32, 25 | lcomf 20900 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))):(𝐼 ∖ {𝑗})⟶𝐵) | 
| 34 |  | islindf4.y | . . . . . . . . . . . . . . . . 17
⊢ 𝑌 = (0g‘𝑅) | 
| 35 |  | simprr 772 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 finSupp 𝑌) | 
| 36 | 8, 12, 9, 7, 2, 28,
32, 25, 20, 34, 35 | lcomfsupp 20901 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) finSupp 0 ) | 
| 37 | 7, 20, 22, 25, 33, 36 | gsumcl 19934 | . . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵) | 
| 38 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(+g‘𝑊) = (+g‘𝑊) | 
| 39 | 7, 38, 20, 10 | grpinvid2 19011 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Grp ∧ (𝑙 · (𝐹‘𝑗)) ∈ 𝐵 ∧ (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵) → (((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 )) | 
| 40 | 17, 19, 37, 39 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 )) | 
| 41 |  | simplr 768 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑗 ∈ 𝐼) | 
| 42 |  | fsnunf2 7207 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) ∧ 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) → (𝑦 ∪ {〈𝑗, 𝑙〉}):𝐼⟶(Base‘𝑅)) | 
| 43 | 28, 41, 3, 42 | syl3anc 1372 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}):𝐼⟶(Base‘𝑅)) | 
| 44 | 8, 12, 9, 7, 2, 43,
29, 23 | lcomf 20900 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹):𝐼⟶𝐵) | 
| 45 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼) | 
| 46 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) → 𝑙 ∈ (Base‘𝑅)) | 
| 47 | 45, 46 | anim12i 613 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅))) | 
| 48 |  | elmapfun 8907 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → Fun 𝑦) | 
| 49 |  | fdm 6744 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) → dom 𝑦 = (𝐼 ∖ {𝑗})) | 
| 50 |  | neldifsnd 4792 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) | 
| 51 |  | df-nel 3046 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ dom 𝑦) | 
| 52 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗}))) | 
| 53 | 52 | notbid 318 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (¬ 𝑗 ∈ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗}))) | 
| 54 | 51, 53 | bitrid 283 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗}))) | 
| 55 | 50, 54 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → 𝑗 ∉ dom 𝑦) | 
| 56 | 27, 49, 55 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → 𝑗 ∉ dom 𝑦) | 
| 57 | 48, 56 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) | 
| 58 | 57 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) | 
| 59 | 58 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) | 
| 60 | 47, 59 | jca 511 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦))) | 
| 61 |  | funsnfsupp 9433 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌)) | 
| 62 | 61 | bicomd 223 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) | 
| 63 | 60, 62 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) | 
| 64 | 63 | biimpd 229 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 → (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) | 
| 65 | 64 | impr 454 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌) | 
| 66 | 8, 12, 9, 7, 2, 43,
29, 23, 20, 34, 65 | lcomfsupp 20901 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) finSupp 0 ) | 
| 67 |  | disjdifr 4472 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅ | 
| 68 | 67 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅) | 
| 69 |  | difsnid 4809 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ 𝐼 → ((𝐼 ∖ {𝑗}) ∪ {𝑗}) = 𝐼) | 
| 70 | 69 | eqcomd 2742 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ 𝐼 → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗})) | 
| 71 | 41, 70 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗})) | 
| 72 | 7, 20, 38, 22, 23, 44, 66, 68, 71 | gsumsplit 19947 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = ((𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})))) | 
| 73 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V | 
| 74 |  | snex 5435 | . . . . . . . . . . . . . . . . . . . . 21
⊢
{〈𝑗, 𝑙〉} ∈
V | 
| 75 | 73, 74 | unex 7765 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∪ {〈𝑗, 𝑙〉}) ∈ V | 
| 76 |  | simpl3 1193 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹:𝐼⟶𝐵) | 
| 77 |  | simpl2 1192 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ 𝑋) | 
| 78 | 76, 77 | fexd 7248 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹 ∈ V) | 
| 79 | 78 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 ∈ V) | 
| 80 |  | offres 8009 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∈ V ∧ 𝐹 ∈ V) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) | 
| 81 | 75, 79, 80 | sylancr 587 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) | 
| 82 | 28 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 Fn (𝐼 ∖ {𝑗})) | 
| 83 |  | neldifsn 4791 | . . . . . . . . . . . . . . . . . . . . 21
⊢  ¬
𝑗 ∈ (𝐼 ∖ {𝑗}) | 
| 84 |  | fsnunres 7209 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 Fn (𝐼 ∖ {𝑗}) ∧ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) = 𝑦) | 
| 85 | 82, 83, 84 | sylancl 586 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) = 𝑦) | 
| 86 | 85 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) = (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) | 
| 87 | 81, 86 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) | 
| 88 | 87 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗}))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) | 
| 89 | 44 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) Fn 𝐼) | 
| 90 |  | fnressn 7177 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) Fn 𝐼 ∧ 𝑗 ∈ 𝐼) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉}) | 
| 91 | 89, 41, 90 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉}) | 
| 92 | 43 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼) | 
| 93 | 29 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 Fn 𝐼) | 
| 94 |  | fnfvof 7715 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼 ∧ 𝐹 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑗 ∈ 𝐼)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗))) | 
| 95 | 92, 93, 23, 41, 94 | syl22anc 838 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗))) | 
| 96 |  | fndm 6670 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → dom 𝑦 = (𝐼 ∖ {𝑗})) | 
| 97 | 96 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗}))) | 
| 98 | 83, 97 | mtbiri 327 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ dom 𝑦) | 
| 99 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑗 ∈ V | 
| 100 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑙 ∈ V | 
| 101 |  | fsnunfv 7208 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ V ∧ 𝑙 ∈ V ∧ ¬ 𝑗 ∈ dom 𝑦) → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑙) | 
| 102 | 99, 100, 101 | mp3an12 1452 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑗 ∈ dom 𝑦 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑙) | 
| 103 | 82, 98, 102 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑙) | 
| 104 | 103 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗))) | 
| 105 | 95, 104 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (𝑙 · (𝐹‘𝑗))) | 
| 106 | 105 | opeq2d 4879 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉 = 〈𝑗, (𝑙 · (𝐹‘𝑗))〉) | 
| 107 | 106 | sneqd 4637 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉} = {〈𝑗, (𝑙 · (𝐹‘𝑗))〉}) | 
| 108 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 · (𝐹‘𝑗)) ∈ V | 
| 109 |  | fmptsn 7188 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ V ∧ (𝑙 · (𝐹‘𝑗)) ∈ V) → {〈𝑗, (𝑙 · (𝐹‘𝑗))〉} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) | 
| 110 | 99, 108, 109 | mp2an 692 | . . . . . . . . . . . . . . . . . . . . 21
⊢
{〈𝑗, (𝑙 · (𝐹‘𝑗))〉} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))) | 
| 111 | 110 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {〈𝑗, (𝑙 · (𝐹‘𝑗))〉} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) | 
| 112 | 91, 107, 111 | 3eqtrd 2780 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) | 
| 113 | 112 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})) = (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))))) | 
| 114 |  | cmnmnd 19816 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ CMnd → 𝑊 ∈ Mnd) | 
| 115 | 2, 21, 114 | 3syl 18 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Mnd) | 
| 116 | 99 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑗 ∈ V) | 
| 117 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑗 → (𝑙 · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗))) | 
| 118 | 7, 117 | gsumsn 19973 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Mnd ∧ 𝑗 ∈ V ∧ (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗))) | 
| 119 | 115, 116,
19, 118 | syl3anc 1372 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗))) | 
| 120 | 113, 119 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})) = (𝑙 · (𝐹‘𝑗))) | 
| 121 | 88, 120 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}))) = ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗)))) | 
| 122 | 72, 121 | eqtr2d 2777 | . . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹))) | 
| 123 | 122 | eqeq1d 2738 | . . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 )) | 
| 124 | 15, 40, 123 | 3bitrd 305 | . . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 )) | 
| 125 | 103 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 = ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗)) | 
| 126 | 125 | eqeq1d 2738 | . . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 = 𝑌 ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) | 
| 127 | 124, 126 | imbi12d 344 | . . . . . . . . . . . 12
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) | 
| 128 | 127 | anassrs 467 | . . . . . . . . . . 11
⊢
(((((𝑊 ∈ LMod
∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) ∧ 𝑦 finSupp 𝑌) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) | 
| 129 | 128 | pm5.74da 803 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌)) ↔ (𝑦 finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) | 
| 130 |  | impexp 450 | . . . . . . . . . . 11
⊢ (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌))) | 
| 131 | 130 | a1i 11 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌)))) | 
| 132 | 63 | bicomd 223 | . . . . . . . . . . 11
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌)) | 
| 133 | 132 | imbi1d 341 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) ↔ (𝑦 finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) | 
| 134 | 129, 131,
133 | 3bitr4d 311 | . . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) | 
| 135 | 134 | 2ralbidva 3218 | . . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) | 
| 136 |  | breq1 5145 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) | 
| 137 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥 ∘f · 𝐹) = ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) | 
| 138 | 137 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑊 Σg (𝑥 ∘f · 𝐹)) = (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹))) | 
| 139 | 138 | eqeq1d 2738 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 )) | 
| 140 |  | fveq1 6904 | . . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥‘𝑗) = ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗)) | 
| 141 | 140 | eqeq1d 2738 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑥‘𝑗) = 𝑌 ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) | 
| 142 | 139, 141 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) | 
| 143 | 136, 142 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) | 
| 144 | 143 | ralxpmap 8937 | . . . . . . . . 9
⊢ (𝑗 ∈ 𝐼 → (∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) | 
| 145 | 144 | adantl 481 | . . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) | 
| 146 | 135, 145 | bitr4d 282 | . . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))) | 
| 147 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 finSupp 𝑌 ↔ 𝑥 finSupp 𝑌)) | 
| 148 | 147 | ralrab 3698 | . . . . . . 7
⊢
(∀𝑥 ∈
{𝑧 ∈
((Base‘𝑅)
↑m 𝐼)
∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) | 
| 149 | 146, 148 | bitr4di 289 | . . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) | 
| 150 |  | resima 6032 | . . . . . . . . . . . . 13
⊢ ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) = (𝐹 “ (𝐼 ∖ {𝑗})) | 
| 151 | 150 | eqcomi 2745 | . . . . . . . . . . . 12
⊢ (𝐹 “ (𝐼 ∖ {𝑗})) = ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) | 
| 152 | 151 | fveq2i 6908 | . . . . . . . . . . 11
⊢
((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) = ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) | 
| 153 | 152 | eleq2i 2832 | . . . . . . . . . 10
⊢
((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})))) | 
| 154 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) | 
| 155 | 76, 30, 31 | sylancl 586 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) | 
| 156 |  | simpl1 1191 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝑊 ∈ LMod) | 
| 157 | 24 | 3ad2ant2 1134 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐼 ∖ {𝑗}) ∈ V) | 
| 158 | 157 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐼 ∖ {𝑗}) ∈ V) | 
| 159 | 154, 7, 12, 8, 34, 9, 155, 156, 158 | ellspd 21823 | . . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))))) | 
| 160 | 153, 159 | bitrid 283 | . . . . . . . . 9
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))))) | 
| 161 | 160 | imbi1d 341 | . . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) | 
| 162 |  | r19.23v 3182 | . . . . . . . 8
⊢
(∀𝑦 ∈
((Base‘𝑅)
↑m (𝐼
∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌)) | 
| 163 | 161, 162 | bitr4di 289 | . . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) | 
| 164 | 163 | ralbidv 3177 | . . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) | 
| 165 |  | islindf4.l | . . . . . . . 8
⊢ 𝐿 = (Base‘(𝑅 freeLMod 𝐼)) | 
| 166 | 8 | fvexi 6919 | . . . . . . . . . . 11
⊢ 𝑅 ∈ V | 
| 167 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼) | 
| 168 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} | 
| 169 | 167, 12, 34, 168 | frlmbas 21776 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ V ∧ 𝐼 ∈ 𝑋) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) | 
| 170 | 166, 169 | mpan 690 | . . . . . . . . . 10
⊢ (𝐼 ∈ 𝑋 → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) | 
| 171 | 170 | 3ad2ant2 1134 | . . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) | 
| 172 | 171 | adantr 480 | . . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) | 
| 173 | 165, 172 | eqtr4id 2795 | . . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐿 = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌}) | 
| 174 | 173 | raleqdv 3325 | . . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) | 
| 175 | 149, 164,
174 | 3bitr4d 311 | . . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) | 
| 176 | 1, 175 | bitrid 283 | . . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) | 
| 177 | 8 | lmodfgrp 20868 | . . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑅 ∈ Grp) | 
| 178 | 12, 34, 11 | grpinvnzcl 19030 | . . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌})) | 
| 179 | 177, 178 | sylan 580 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌})) | 
| 180 | 12, 34, 11 | grpinvnzcl 19030 | . . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌})) | 
| 181 | 177, 180 | sylan 580 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌})) | 
| 182 |  | eldifi 4130 | . . . . . . . . . 10
⊢ (𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) → 𝑘 ∈ (Base‘𝑅)) | 
| 183 | 12, 11 | grpinvinv 19024 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ (Base‘𝑅)) →
((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘) | 
| 184 | 177, 182,
183 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘) | 
| 185 | 184 | eqcomd 2742 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) | 
| 186 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑙 = ((invg‘𝑅)‘𝑘) → ((invg‘𝑅)‘𝑙) = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) | 
| 187 | 186 | rspceeqv 3644 | . . . . . . . 8
⊢
((((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}) ∧ 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙)) | 
| 188 | 181, 185,
187 | syl2anc 584 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙)) | 
| 189 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (𝑘 · (𝐹‘𝑗)) = (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗))) | 
| 190 | 189 | eleq1d 2825 | . . . . . . . . 9
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → ((𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) | 
| 191 | 190 | notbid 318 | . . . . . . . 8
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) | 
| 192 | 191 | adantl 481 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 = ((invg‘𝑅)‘𝑙)) → (¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) | 
| 193 | 179, 188,
192 | ralxfrd 5407 | . . . . . 6
⊢ (𝑊 ∈ LMod →
(∀𝑘 ∈
((Base‘𝑅) ∖
{𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) | 
| 194 | 193 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) | 
| 195 | 194 | adantr 480 | . . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) | 
| 196 |  | simplr 768 | . . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → 𝑗 ∈ 𝐼) | 
| 197 | 34 | fvexi 6919 | . . . . . . . . 9
⊢ 𝑌 ∈ V | 
| 198 | 197 | fvconst2 7225 | . . . . . . . 8
⊢ (𝑗 ∈ 𝐼 → ((𝐼 × {𝑌})‘𝑗) = 𝑌) | 
| 199 | 196, 198 | syl 17 | . . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝐼 × {𝑌})‘𝑗) = 𝑌) | 
| 200 | 199 | eqeq2d 2747 | . . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗) ↔ (𝑥‘𝑗) = 𝑌)) | 
| 201 | 200 | imbi2d 340 | . . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) | 
| 202 | 201 | ralbidva 3175 | . . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) | 
| 203 | 176, 195,
202 | 3bitr4d 311 | . . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) | 
| 204 | 203 | ralbidva 3175 | . 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) | 
| 205 | 7, 9, 154, 8, 12, 34 | islindf2 21835 | . 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) | 
| 206 | 167, 12, 165 | frlmbasf 21781 | . . . . . . . 8
⊢ ((𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅)) | 
| 207 | 206 | 3ad2antl2 1186 | . . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅)) | 
| 208 | 207 | ffnd 6736 | . . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥 Fn 𝐼) | 
| 209 |  | fnconstg 6795 | . . . . . . 7
⊢ (𝑌 ∈ V → (𝐼 × {𝑌}) Fn 𝐼) | 
| 210 | 197, 209 | ax-mp 5 | . . . . . 6
⊢ (𝐼 × {𝑌}) Fn 𝐼 | 
| 211 |  | eqfnfv 7050 | . . . . . 6
⊢ ((𝑥 Fn 𝐼 ∧ (𝐼 × {𝑌}) Fn 𝐼) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) | 
| 212 | 208, 210,
211 | sylancl 586 | . . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) | 
| 213 | 212 | imbi2d 340 | . . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) | 
| 214 | 213 | ralbidva 3175 | . . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) | 
| 215 |  | r19.21v 3179 | . . . . 5
⊢
(∀𝑗 ∈
𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) | 
| 216 | 215 | ralbii 3092 | . . . 4
⊢
(∀𝑥 ∈
𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) | 
| 217 |  | ralcom 3288 | . . . 4
⊢
(∀𝑥 ∈
𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) | 
| 218 | 216, 217 | bitr3i 277 | . . 3
⊢
(∀𝑥 ∈
𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) | 
| 219 | 214, 218 | bitrdi 287 | . 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) | 
| 220 | 204, 205,
219 | 3bitr4d 311 | 1
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})))) |