Step | Hyp | Ref
| Expression |
1 | | raldifsni 4721 |
. . . . 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 6843 |
. . . . . . . . . . . . . . . . . 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 2821 |
. . . . . . . . . . . . . . . . 17
⊢
(invg‘𝑊) = (invg‘𝑊) |
11 | | eqid 2821 |
. . . . . . . . . . . . . . . . 17
⊢
(invg‘𝑅) = (invg‘𝑅) |
12 | | eqid 2821 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑅) =
(Base‘𝑅) |
13 | 7, 8, 9, 10, 11, 12 | lmodvsinv 19802 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗)))) |
14 | 2, 3, 6, 13 | syl3anc 1367 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗)))) |
15 | 14 | eqeq1d 2823 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))))) |
16 | | lmodgrp 19635 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
17 | 2, 16 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Grp) |
18 | 7, 8, 9, 12 | lmodvscl 19645 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) |
19 | 2, 3, 6, 18 | syl3anc 1367 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) |
20 | | islindf4.z |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝑊) |
21 | | lmodcmn 19676 |
. . . . . . . . . . . . . . . . 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 5223 |
. . . . . . . . . . . . . . . . 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 8422 |
. . . . . . . . . . . . . . . . . 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 4107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∖ {𝑗}) ⊆ 𝐼 |
31 | | fssres 6538 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐼⟶𝐵 ∧ (𝐼 ∖ {𝑗}) ⊆ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
32 | 29, 30, 31 | sylancl 588 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
33 | 8, 12, 9, 7, 2, 28,
32, 25 | lcomf 19667 |
. . . . . . . . . . . . . . . 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 19668 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) finSupp 0 ) |
37 | 7, 20, 22, 25, 33, 36 | gsumcl 19029 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵) |
38 | | eqid 2821 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘𝑊) = (+g‘𝑊) |
39 | 7, 38, 20, 10 | grpinvid2 18149 |
. . . . . . . . . . . . . . 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 6942 |
. . . . . . . . . . . . . . . . . . 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 19667 |
. . . . . . . . . . . . . . . . 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 8424 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → Fun 𝑦) |
49 | | fdm 6516 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) → dom 𝑦 = (𝐼 ∖ {𝑗})) |
50 | | neldifsnd 4719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) |
51 | | df-nel 3124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ dom 𝑦) |
52 | | eleq2 2901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8851 |
. . . . . . . . . . . . . . . . . . . . . 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 19668 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) finSupp 0 ) |
67 | | incom 4177 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ({𝑗} ∩ (𝐼 ∖ {𝑗})) |
68 | | disjdif 4420 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑗} ∩ (𝐼 ∖ {𝑗})) = ∅ |
69 | 67, 68 | eqtri 2844 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅ |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅) |
71 | | difsnid 4736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ 𝐼 → ((𝐼 ∖ {𝑗}) ∪ {𝑗}) = 𝐼) |
72 | 71 | eqcomd 2827 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ 𝐼 → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗})) |
73 | 41, 72 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗})) |
74 | 7, 20, 38, 22, 23, 44, 66, 70, 73 | gsumsplit 19042 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = ((𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})))) |
75 | | vex 3497 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V |
76 | | snex 5323 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
{〈𝑗, 𝑙〉} ∈
V |
77 | 75, 76 | unex 7463 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∪ {〈𝑗, 𝑙〉}) ∈ V |
78 | | simpl3 1189 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹:𝐼⟶𝐵) |
79 | | simpl2 1188 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ 𝑋) |
80 | | fex 6983 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:𝐼⟶𝐵 ∧ 𝐼 ∈ 𝑋) → 𝐹 ∈ V) |
81 | 78, 79, 80 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹 ∈ V) |
82 | 81 | adantr 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 ∈ V) |
83 | | offres 7678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∈ V ∧ 𝐹 ∈ V) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
84 | 77, 82, 83 | sylancr 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
85 | 28 | ffnd 6509 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 Fn (𝐼 ∖ {𝑗})) |
86 | | neldifsn 4718 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ¬
𝑗 ∈ (𝐼 ∖ {𝑗}) |
87 | | fsnunres 6944 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 Fn (𝐼 ∖ {𝑗}) ∧ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) = 𝑦) |
88 | 85, 86, 87 | sylancl 588 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) = 𝑦) |
89 | 88 | oveq1d 7165 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) = (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
90 | 84, 89 | eqtrd 2856 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
91 | 90 | oveq2d 7166 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗}))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) |
92 | 44 | ffnd 6509 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) Fn 𝐼) |
93 | | fnressn 6914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) Fn 𝐼 ∧ 𝑗 ∈ 𝐼) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉}) |
94 | 92, 41, 93 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉}) |
95 | 43 | ffnd 6509 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼) |
96 | 29 | ffnd 6509 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 Fn 𝐼) |
97 | | fnfvof 7417 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼 ∧ 𝐹 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑗 ∈ 𝐼)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗))) |
98 | 95, 96, 23, 41, 97 | syl22anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗))) |
99 | | fndm 6449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → dom 𝑦 = (𝐼 ∖ {𝑗})) |
100 | 99 | eleq2d 2898 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
101 | 86, 100 | mtbiri 329 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ dom 𝑦) |
102 | | vex 3497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑗 ∈ V |
103 | | vex 3497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑙 ∈ V |
104 | | fsnunfv 6943 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 7165 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗))) |
108 | 98, 107 | eqtrd 2856 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (𝑙 · (𝐹‘𝑗))) |
109 | 108 | opeq2d 4803 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉 = 〈𝑗, (𝑙 · (𝐹‘𝑗))〉) |
110 | 109 | sneqd 4572 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉} = {〈𝑗, (𝑙 · (𝐹‘𝑗))〉}) |
111 | | ovex 7183 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 · (𝐹‘𝑗)) ∈ V |
112 | | fmptsn 6923 |
. . . . . . . . . . . . . . . . . . . . . 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 2860 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) |
116 | 115 | oveq2d 7166 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})) = (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))))) |
117 | | cmnmnd 18916 |
. . . . . . . . . . . . . . . . . . . 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 2822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑗 → (𝑙 · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗))) |
121 | 7, 120 | gsumsn 19068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Mnd ∧ 𝑗 ∈ V ∧ (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗))) |
122 | 118, 119,
19, 121 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗))) |
123 | 116, 122 | eqtrd 2856 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})) = (𝑙 · (𝐹‘𝑗))) |
124 | 91, 123 | oveq12d 7168 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}))) = ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗)))) |
125 | 74, 124 | eqtr2d 2857 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹))) |
126 | 125 | eqeq1d 2823 |
. . . . . . . . . . . . . 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 2827 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 = ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗)) |
129 | 128 | eqeq1d 2823 |
. . . . . . . . . . . . 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 3198 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
139 | | breq1 5061 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
140 | | oveq1 7157 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥 ∘f · 𝐹) = ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) |
141 | 140 | oveq2d 7166 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑊 Σg (𝑥 ∘f · 𝐹)) = (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹))) |
142 | 141 | eqeq1d 2823 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 )) |
143 | | fveq1 6663 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥‘𝑗) = ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗)) |
144 | 143 | eqeq1d 2823 |
. . . . . . . . . . . 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 8454 |
. . . . . . . . 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 5061 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 finSupp 𝑌 ↔ 𝑥 finSupp 𝑌)) |
151 | 150 | ralrab 3684 |
. . . . . . 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 5881 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) = (𝐹 “ (𝐼 ∖ {𝑗})) |
154 | 153 | eqcomi 2830 |
. . . . . . . . . . . 12
⊢ (𝐹 “ (𝐼 ∖ {𝑗})) = ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) |
155 | 154 | fveq2i 6667 |
. . . . . . . . . . 11
⊢
((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) = ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) |
156 | 155 | eleq2i 2904 |
. . . . . . . . . 10
⊢
((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})))) |
157 | | eqid 2821 |
. . . . . . . . . . 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 20940 |
. . . . . . . . . 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 3279 |
. . . . . . . 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 3197 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) |
168 | 8 | fvexi 6678 |
. . . . . . . . . . 11
⊢ 𝑅 ∈ V |
169 | | eqid 2821 |
. . . . . . . . . . . 12
⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼) |
170 | | eqid 2821 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} |
171 | 169, 12, 34, 170 | frlmbas 20893 |
. . . . . . . . . . 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 2875 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐿 = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌}) |
177 | 176 | raleqdv 3415 |
. . . . . 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 19637 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑅 ∈ Grp) |
181 | 12, 34, 11 | grpinvnzcl 18165 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌})) |
182 | 180, 181 | sylan 582 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌})) |
183 | 12, 34, 11 | grpinvnzcl 18165 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌})) |
184 | 180, 183 | sylan 582 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌})) |
185 | | eldifi 4102 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) → 𝑘 ∈ (Base‘𝑅)) |
186 | 12, 11 | grpinvinv 18160 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ (Base‘𝑅)) →
((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘) |
187 | 180, 185,
186 | syl2an 597 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘) |
188 | 187 | eqcomd 2827 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) |
189 | | fveq2 6664 |
. . . . . . . . 9
⊢ (𝑙 = ((invg‘𝑅)‘𝑘) → ((invg‘𝑅)‘𝑙) = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) |
190 | 189 | rspceeqv 3637 |
. . . . . . . 8
⊢
((((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}) ∧ 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙)) |
191 | 184, 188,
190 | syl2anc 586 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙)) |
192 | | oveq1 7157 |
. . . . . . . . . 10
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (𝑘 · (𝐹‘𝑗)) = (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗))) |
193 | 192 | eleq1d 2897 |
. . . . . . . . 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 5300 |
. . . . . 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 6678 |
. . . . . . . . 9
⊢ 𝑌 ∈ V |
201 | 200 | fvconst2 6960 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝐼 → ((𝐼 × {𝑌})‘𝑗) = 𝑌) |
202 | 199, 201 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝐼 × {𝑌})‘𝑗) = 𝑌) |
203 | 202 | eqeq2d 2832 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗) ↔ (𝑥‘𝑗) = 𝑌)) |
204 | 203 | imbi2d 343 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
205 | 204 | ralbidva 3196 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
206 | 179, 198,
205 | 3bitr4d 313 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
207 | 206 | ralbidva 3196 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
208 | 7, 9, 157, 8, 12, 34 | islindf2 20952 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
209 | 169, 12, 175 | frlmbasf 20898 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅)) |
210 | 209 | 3ad2antl2 1182 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅)) |
211 | 210 | ffnd 6509 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥 Fn 𝐼) |
212 | | fnconstg 6561 |
. . . . . . 7
⊢ (𝑌 ∈ V → (𝐼 × {𝑌}) Fn 𝐼) |
213 | 200, 212 | ax-mp 5 |
. . . . . 6
⊢ (𝐼 × {𝑌}) Fn 𝐼 |
214 | | eqfnfv 6796 |
. . . . . 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 3196 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
218 | | r19.21v 3175 |
. . . . 5
⊢
(∀𝑗 ∈
𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
219 | 218 | ralbii 3165 |
. . . 4
⊢
(∀𝑥 ∈
𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
220 | | ralcom 3354 |
. . . 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 → 𝑥 = (𝐼 × {𝑌})))) |