Step | Hyp | Ref
| Expression |
1 | | raldifsni 4729 |
. . . . 5
⊢
(∀𝑙 ∈
((Base‘𝑅) ∖
{𝑌}) ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌)) |
2 | | simpll1 1211 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ LMod) |
3 | | simprll 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 ∈ (Base‘𝑅)) |
4 | | ffvelrn 6968 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐼⟶𝐵 ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑗) ∈ 𝐵) |
5 | 4 | 3ad2antl3 1186 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑗) ∈ 𝐵) |
6 | 5 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹‘𝑗) ∈ 𝐵) |
7 | | islindf4.b |
. . . . . . . . . . . . . . . . 17
⊢ 𝐵 = (Base‘𝑊) |
8 | | islindf4.r |
. . . . . . . . . . . . . . . . 17
⊢ 𝑅 = (Scalar‘𝑊) |
9 | | islindf4.t |
. . . . . . . . . . . . . . . . 17
⊢ · = (
·𝑠 ‘𝑊) |
10 | | eqid 2739 |
. . . . . . . . . . . . . . . . 17
⊢
(invg‘𝑊) = (invg‘𝑊) |
11 | | eqid 2739 |
. . . . . . . . . . . . . . . . 17
⊢
(invg‘𝑅) = (invg‘𝑅) |
12 | | eqid 2739 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑅) =
(Base‘𝑅) |
13 | 7, 8, 9, 10, 11, 12 | lmodvsinv 20307 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗)))) |
14 | 2, 3, 6, 13 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗)))) |
15 | 14 | eqeq1d 2741 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))))) |
16 | | lmodgrp 20139 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
17 | 2, 16 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Grp) |
18 | 7, 8, 9, 12 | lmodvscl 20149 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) |
19 | 2, 3, 6, 18 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) |
20 | | islindf4.z |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝑊) |
21 | | lmodcmn 20180 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd) |
22 | 2, 21 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ CMnd) |
23 | | simpll2 1212 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 ∈ 𝑋) |
24 | | difexg 5252 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑋 → (𝐼 ∖ {𝑗}) ∈ V) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐼 ∖ {𝑗}) ∈ V) |
26 | | simprlr 777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) |
27 | | elmapi 8646 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅)) |
29 | | simpll3 1213 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹:𝐼⟶𝐵) |
30 | | difss 4067 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∖ {𝑗}) ⊆ 𝐼 |
31 | | fssres 6649 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐼⟶𝐵 ∧ (𝐼 ∖ {𝑗}) ⊆ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
32 | 29, 30, 31 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
33 | 8, 12, 9, 7, 2, 28,
32, 25 | lcomf 20171 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))):(𝐼 ∖ {𝑗})⟶𝐵) |
34 | | islindf4.y |
. . . . . . . . . . . . . . . . 17
⊢ 𝑌 = (0g‘𝑅) |
35 | | simprr 770 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 finSupp 𝑌) |
36 | 8, 12, 9, 7, 2, 28,
32, 25, 20, 34, 35 | lcomfsupp 20172 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) finSupp 0 ) |
37 | 7, 20, 22, 25, 33, 36 | gsumcl 19525 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵) |
38 | | eqid 2739 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘𝑊) = (+g‘𝑊) |
39 | 7, 38, 20, 10 | grpinvid2 18640 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Grp ∧ (𝑙 · (𝐹‘𝑗)) ∈ 𝐵 ∧ (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵) → (((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 )) |
40 | 17, 19, 37, 39 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 )) |
41 | | simplr 766 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑗 ∈ 𝐼) |
42 | | fsnunf2 7067 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) ∧ 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) → (𝑦 ∪ {〈𝑗, 𝑙〉}):𝐼⟶(Base‘𝑅)) |
43 | 28, 41, 3, 42 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}):𝐼⟶(Base‘𝑅)) |
44 | 8, 12, 9, 7, 2, 43,
29, 23 | lcomf 20171 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹):𝐼⟶𝐵) |
45 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼) |
46 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) → 𝑙 ∈ (Base‘𝑅)) |
47 | 45, 46 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅))) |
48 | | elmapfun 8663 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → Fun 𝑦) |
49 | | fdm 6618 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) → dom 𝑦 = (𝐼 ∖ {𝑗})) |
50 | | neldifsnd 4727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) |
51 | | df-nel 3051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ dom 𝑦) |
52 | | eleq2 2828 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
53 | 52 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (¬ 𝑗 ∈ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
54 | 51, 53 | bitrid 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
55 | 50, 54 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → 𝑗 ∉ dom 𝑦) |
56 | 27, 49, 55 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → 𝑗 ∉ dom 𝑦) |
57 | 48, 56 | jca 512 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) |
58 | 57 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) |
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) |
60 | 47, 59 | jca 512 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦))) |
61 | | funsnfsupp 9161 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌)) |
62 | 61 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
64 | 63 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 → (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
65 | 64 | impr 455 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌) |
66 | 8, 12, 9, 7, 2, 43,
29, 23, 20, 34, 65 | lcomfsupp 20172 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) finSupp 0 ) |
67 | | disjdifr 4407 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅ |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅) |
69 | | difsnid 4744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ 𝐼 → ((𝐼 ∖ {𝑗}) ∪ {𝑗}) = 𝐼) |
70 | 69 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ 𝐼 → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗})) |
71 | 41, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗})) |
72 | 7, 20, 38, 22, 23, 44, 66, 68, 71 | gsumsplit 19538 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = ((𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})))) |
73 | | vex 3437 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V |
74 | | snex 5355 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
{〈𝑗, 𝑙〉} ∈
V |
75 | 73, 74 | unex 7605 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∪ {〈𝑗, 𝑙〉}) ∈ V |
76 | | simpl3 1192 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹:𝐼⟶𝐵) |
77 | | simpl2 1191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ 𝑋) |
78 | 76, 77 | fexd 7112 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹 ∈ V) |
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 ∈ V) |
80 | | offres 7835 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∈ V ∧ 𝐹 ∈ V) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
81 | 75, 79, 80 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
82 | 28 | ffnd 6610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 Fn (𝐼 ∖ {𝑗})) |
83 | | neldifsn 4726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ¬
𝑗 ∈ (𝐼 ∖ {𝑗}) |
84 | | fsnunres 7069 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 Fn (𝐼 ∖ {𝑗}) ∧ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) = 𝑦) |
85 | 82, 83, 84 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) = 𝑦) |
86 | 85 | oveq1d 7299 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) = (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
87 | 81, 86 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
88 | 87 | oveq2d 7300 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗}))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) |
89 | 44 | ffnd 6610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) Fn 𝐼) |
90 | | fnressn 7039 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) Fn 𝐼 ∧ 𝑗 ∈ 𝐼) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉}) |
91 | 89, 41, 90 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉}) |
92 | 43 | ffnd 6610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼) |
93 | 29 | ffnd 6610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 Fn 𝐼) |
94 | | fnfvof 7559 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼 ∧ 𝐹 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑗 ∈ 𝐼)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗))) |
95 | 92, 93, 23, 41, 94 | syl22anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗))) |
96 | | fndm 6545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → dom 𝑦 = (𝐼 ∖ {𝑗})) |
97 | 96 | eleq2d 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
98 | 83, 97 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ dom 𝑦) |
99 | | vex 3437 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑗 ∈ V |
100 | | vex 3437 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑙 ∈ V |
101 | | fsnunfv 7068 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ V ∧ 𝑙 ∈ V ∧ ¬ 𝑗 ∈ dom 𝑦) → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑙) |
102 | 99, 100, 101 | mp3an12 1450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑗 ∈ dom 𝑦 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑙) |
103 | 82, 98, 102 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑙) |
104 | 103 | oveq1d 7299 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗))) |
105 | 95, 104 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (𝑙 · (𝐹‘𝑗))) |
106 | 105 | opeq2d 4812 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉 = 〈𝑗, (𝑙 · (𝐹‘𝑗))〉) |
107 | 106 | sneqd 4574 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉} = {〈𝑗, (𝑙 · (𝐹‘𝑗))〉}) |
108 | | ovex 7317 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 · (𝐹‘𝑗)) ∈ V |
109 | | fmptsn 7048 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ V ∧ (𝑙 · (𝐹‘𝑗)) ∈ V) → {〈𝑗, (𝑙 · (𝐹‘𝑗))〉} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) |
110 | 99, 108, 109 | mp2an 689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
{〈𝑗, (𝑙 · (𝐹‘𝑗))〉} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))) |
111 | 110 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {〈𝑗, (𝑙 · (𝐹‘𝑗))〉} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) |
112 | 91, 107, 111 | 3eqtrd 2783 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) |
113 | 112 | oveq2d 7300 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})) = (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))))) |
114 | | cmnmnd 19411 |
. . . . . . . . . . . . . . . . . . . 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 2740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑗 → (𝑙 · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗))) |
118 | 7, 117 | gsumsn 19564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Mnd ∧ 𝑗 ∈ V ∧ (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗))) |
119 | 115, 116,
19, 118 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗))) |
120 | 113, 119 | eqtrd 2779 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})) = (𝑙 · (𝐹‘𝑗))) |
121 | 88, 120 | oveq12d 7302 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}))) = ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗)))) |
122 | 72, 121 | eqtr2d 2780 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹))) |
123 | 122 | eqeq1d 2741 |
. . . . . . . . . . . . . 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 2745 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 = ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗)) |
126 | 125 | eqeq1d 2741 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 = 𝑌 ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) |
127 | 124, 126 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) |
128 | 127 | anassrs 468 |
. . . . . . . . . . 11
⊢
(((((𝑊 ∈ LMod
∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) ∧ 𝑦 finSupp 𝑌) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) |
129 | 128 | pm5.74da 801 |
. . . . . . . . . 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 · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌))) |
131 | 130 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌)))) |
132 | 63 | bicomd 222 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌)) |
133 | 132 | imbi1d 342 |
. . . . . . . . . 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 3129 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
136 | | breq1 5078 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
137 | | oveq1 7291 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥 ∘f · 𝐹) = ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) |
138 | 137 | oveq2d 7300 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑊 Σg (𝑥 ∘f · 𝐹)) = (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹))) |
139 | 138 | eqeq1d 2741 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 )) |
140 | | fveq1 6782 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥‘𝑗) = ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗)) |
141 | 140 | eqeq1d 2741 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑥‘𝑗) = 𝑌 ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) |
142 | 139, 141 | imbi12d 345 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) |
143 | 136, 142 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
144 | 143 | ralxpmap 8693 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝐼 → (∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
145 | 144 | adantl 482 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
146 | 135, 145 | bitr4d 281 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))) |
147 | | breq1 5078 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 finSupp 𝑌 ↔ 𝑥 finSupp 𝑌)) |
148 | 147 | ralrab 3631 |
. . . . . . 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 5928 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) = (𝐹 “ (𝐼 ∖ {𝑗})) |
151 | 150 | eqcomi 2748 |
. . . . . . . . . . . 12
⊢ (𝐹 “ (𝐼 ∖ {𝑗})) = ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) |
152 | 151 | fveq2i 6786 |
. . . . . . . . . . 11
⊢
((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) = ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) |
153 | 152 | eleq2i 2831 |
. . . . . . . . . 10
⊢
((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})))) |
154 | | eqid 2739 |
. . . . . . . . . . 11
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
155 | 76, 30, 31 | sylancl 586 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
156 | | simpl1 1190 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝑊 ∈ LMod) |
157 | 24 | 3ad2ant2 1133 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐼 ∖ {𝑗}) ∈ V) |
158 | 157 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐼 ∖ {𝑗}) ∈ V) |
159 | 154, 7, 12, 8, 34, 9, 155, 156, 158 | ellspd 21018 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))))) |
160 | 153, 159 | bitrid 282 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))))) |
161 | 160 | imbi1d 342 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) |
162 | | r19.23v 3209 |
. . . . . . . 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 3113 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) |
165 | | islindf4.l |
. . . . . . . 8
⊢ 𝐿 = (Base‘(𝑅 freeLMod 𝐼)) |
166 | 8 | fvexi 6797 |
. . . . . . . . . . 11
⊢ 𝑅 ∈ V |
167 | | eqid 2739 |
. . . . . . . . . . . 12
⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼) |
168 | | eqid 2739 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} |
169 | 167, 12, 34, 168 | frlmbas 20971 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ V ∧ 𝐼 ∈ 𝑋) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
170 | 166, 169 | mpan 687 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑋 → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
171 | 170 | 3ad2ant2 1133 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
172 | 171 | adantr 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
173 | 165, 172 | eqtr4id 2798 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐿 = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌}) |
174 | 173 | raleqdv 3349 |
. . . . . 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 282 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
177 | 8 | lmodfgrp 20141 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑅 ∈ Grp) |
178 | 12, 34, 11 | grpinvnzcl 18656 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌})) |
179 | 177, 178 | sylan 580 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌})) |
180 | 12, 34, 11 | grpinvnzcl 18656 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌})) |
181 | 177, 180 | sylan 580 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌})) |
182 | | eldifi 4062 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) → 𝑘 ∈ (Base‘𝑅)) |
183 | 12, 11 | grpinvinv 18651 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ (Base‘𝑅)) →
((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘) |
184 | 177, 182,
183 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘) |
185 | 184 | eqcomd 2745 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) |
186 | | fveq2 6783 |
. . . . . . . . 9
⊢ (𝑙 = ((invg‘𝑅)‘𝑘) → ((invg‘𝑅)‘𝑙) = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) |
187 | 186 | rspceeqv 3576 |
. . . . . . . 8
⊢
((((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}) ∧ 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙)) |
188 | 181, 185,
187 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙)) |
189 | | oveq1 7291 |
. . . . . . . . . 10
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (𝑘 · (𝐹‘𝑗)) = (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗))) |
190 | 189 | eleq1d 2824 |
. . . . . . . . 9
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → ((𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
191 | 190 | notbid 318 |
. . . . . . . 8
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
192 | 191 | adantl 482 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 = ((invg‘𝑅)‘𝑙)) → (¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
193 | 179, 188,
192 | ralxfrd 5332 |
. . . . . 6
⊢ (𝑊 ∈ LMod →
(∀𝑘 ∈
((Base‘𝑅) ∖
{𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
194 | 193 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
195 | 194 | adantr 481 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
196 | | simplr 766 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → 𝑗 ∈ 𝐼) |
197 | 34 | fvexi 6797 |
. . . . . . . . 9
⊢ 𝑌 ∈ V |
198 | 197 | fvconst2 7088 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝐼 → ((𝐼 × {𝑌})‘𝑗) = 𝑌) |
199 | 196, 198 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝐼 × {𝑌})‘𝑗) = 𝑌) |
200 | 199 | eqeq2d 2750 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗) ↔ (𝑥‘𝑗) = 𝑌)) |
201 | 200 | imbi2d 341 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
202 | 201 | ralbidva 3112 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
203 | 176, 195,
202 | 3bitr4d 311 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
204 | 203 | ralbidva 3112 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
205 | 7, 9, 154, 8, 12, 34 | islindf2 21030 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
206 | 167, 12, 165 | frlmbasf 20976 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅)) |
207 | 206 | 3ad2antl2 1185 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅)) |
208 | 207 | ffnd 6610 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥 Fn 𝐼) |
209 | | fnconstg 6671 |
. . . . . . 7
⊢ (𝑌 ∈ V → (𝐼 × {𝑌}) Fn 𝐼) |
210 | 197, 209 | ax-mp 5 |
. . . . . 6
⊢ (𝐼 × {𝑌}) Fn 𝐼 |
211 | | eqfnfv 6918 |
. . . . . 6
⊢ ((𝑥 Fn 𝐼 ∧ (𝐼 × {𝑌}) Fn 𝐼) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
212 | 208, 210,
211 | sylancl 586 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
213 | 212 | imbi2d 341 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
214 | 213 | ralbidva 3112 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
215 | | r19.21v 3114 |
. . . . 5
⊢
(∀𝑗 ∈
𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
216 | 215 | ralbii 3093 |
. . . 4
⊢
(∀𝑥 ∈
𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
217 | | ralcom 3167 |
. . . 4
⊢
(∀𝑥 ∈
𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
218 | 216, 217 | bitr3i 276 |
. . 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 → 𝑥 = (𝐼 × {𝑌})))) |