Step | Hyp | Ref
| Expression |
1 | | raldifsni 4680 |
. . . . 5
⊢
(∀𝑙 ∈
((Base‘𝑅) ∖
{𝑌}) ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌)) |
2 | | simpll1 1213 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ LMod) |
3 | | simprll 779 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 ∈ (Base‘𝑅)) |
4 | | ffvelrn 6853 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐼⟶𝐵 ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑗) ∈ 𝐵) |
5 | 4 | 3ad2antl3 1188 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑗) ∈ 𝐵) |
6 | 5 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹‘𝑗) ∈ 𝐵) |
7 | | islindf4.b |
. . . . . . . . . . . . . . . . 17
⊢ 𝐵 = (Base‘𝑊) |
8 | | islindf4.r |
. . . . . . . . . . . . . . . . 17
⊢ 𝑅 = (Scalar‘𝑊) |
9 | | islindf4.t |
. . . . . . . . . . . . . . . . 17
⊢ · = (
·𝑠 ‘𝑊) |
10 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(invg‘𝑊) = (invg‘𝑊) |
11 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(invg‘𝑅) = (invg‘𝑅) |
12 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑅) =
(Base‘𝑅) |
13 | 7, 8, 9, 10, 11, 12 | lmodvsinv 19920 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗)))) |
14 | 2, 3, 6, 13 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗)))) |
15 | 14 | eqeq1d 2740 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))))) |
16 | | lmodgrp 19753 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
17 | 2, 16 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Grp) |
18 | 7, 8, 9, 12 | lmodvscl 19763 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) |
19 | 2, 3, 6, 18 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) |
20 | | islindf4.z |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝑊) |
21 | | lmodcmn 19794 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd) |
22 | 2, 21 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ CMnd) |
23 | | simpll2 1214 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 ∈ 𝑋) |
24 | | difexg 5192 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑋 → (𝐼 ∖ {𝑗}) ∈ V) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐼 ∖ {𝑗}) ∈ V) |
26 | | simprlr 780 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) |
27 | | elmapi 8452 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅)) |
29 | | simpll3 1215 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹:𝐼⟶𝐵) |
30 | | difss 4020 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∖ {𝑗}) ⊆ 𝐼 |
31 | | fssres 6538 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐼⟶𝐵 ∧ (𝐼 ∖ {𝑗}) ⊆ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
32 | 29, 30, 31 | sylancl 589 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
33 | 8, 12, 9, 7, 2, 28,
32, 25 | lcomf 19785 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))):(𝐼 ∖ {𝑗})⟶𝐵) |
34 | | islindf4.y |
. . . . . . . . . . . . . . . . 17
⊢ 𝑌 = (0g‘𝑅) |
35 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 finSupp 𝑌) |
36 | 8, 12, 9, 7, 2, 28,
32, 25, 20, 34, 35 | lcomfsupp 19786 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) finSupp 0 ) |
37 | 7, 20, 22, 25, 33, 36 | gsumcl 19147 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵) |
38 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘𝑊) = (+g‘𝑊) |
39 | 7, 38, 20, 10 | grpinvid2 18266 |
. . . . . . . . . . . . . . 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 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑗 ∈ 𝐼) |
42 | | fsnunf2 6952 |
. . . . . . . . . . . . . . . . . . 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 19785 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹):𝐼⟶𝐵) |
45 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼) |
46 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) → 𝑙 ∈ (Base‘𝑅)) |
47 | 45, 46 | anim12i 616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅))) |
48 | | elmapfun 8469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → Fun 𝑦) |
49 | | fdm 6507 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) → dom 𝑦 = (𝐼 ∖ {𝑗})) |
50 | | neldifsnd 4678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) |
51 | | df-nel 3039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ dom 𝑦) |
52 | | eleq2 2821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
53 | 52 | notbid 321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (¬ 𝑗 ∈ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
54 | 51, 53 | syl5bb 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
55 | 50, 54 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → 𝑗 ∉ dom 𝑦) |
56 | 27, 49, 55 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → 𝑗 ∉ dom 𝑦) |
57 | 48, 56 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) |
58 | 57 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) |
59 | 58 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) |
60 | 47, 59 | jca 515 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦))) |
61 | | funsnfsupp 8923 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌)) |
62 | 61 | bicomd 226 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
64 | 63 | biimpd 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 → (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
65 | 64 | impr 458 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌) |
66 | 8, 12, 9, 7, 2, 43,
29, 23, 20, 34, 65 | lcomfsupp 19786 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) finSupp 0 ) |
67 | | disjdifr 4359 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅ |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅) |
69 | | difsnid 4695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ 𝐼 → ((𝐼 ∖ {𝑗}) ∪ {𝑗}) = 𝐼) |
70 | 69 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ 𝐼 → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗})) |
71 | 41, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗})) |
72 | 7, 20, 38, 22, 23, 44, 66, 68, 71 | gsumsplit 19160 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = ((𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})))) |
73 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V |
74 | | snex 5295 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
{〈𝑗, 𝑙〉} ∈
V |
75 | 73, 74 | unex 7481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∪ {〈𝑗, 𝑙〉}) ∈ V |
76 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹:𝐼⟶𝐵) |
77 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ 𝑋) |
78 | 76, 77 | fexd 6994 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹 ∈ V) |
79 | 78 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 ∈ V) |
80 | | offres 7702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∈ V ∧ 𝐹 ∈ V) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
81 | 75, 79, 80 | sylancr 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
82 | 28 | ffnd 6499 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 Fn (𝐼 ∖ {𝑗})) |
83 | | neldifsn 4677 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ¬
𝑗 ∈ (𝐼 ∖ {𝑗}) |
84 | | fsnunres 6954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 Fn (𝐼 ∖ {𝑗}) ∧ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) = 𝑦) |
85 | 82, 83, 84 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) = 𝑦) |
86 | 85 | oveq1d 7179 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))) = (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
87 | 81, 86 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
88 | 87 | oveq2d 7180 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗}))) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) |
89 | 44 | ffnd 6499 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) Fn 𝐼) |
90 | | fnressn 6924 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) Fn 𝐼 ∧ 𝑗 ∈ 𝐼) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉}) |
91 | 89, 41, 90 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉}) |
92 | 43 | ffnd 6499 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼) |
93 | 29 | ffnd 6499 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 Fn 𝐼) |
94 | | fnfvof 7435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼 ∧ 𝐹 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑗 ∈ 𝐼)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗))) |
95 | 92, 93, 23, 41, 94 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗))) |
96 | | fndm 6434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → dom 𝑦 = (𝐼 ∖ {𝑗})) |
97 | 96 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
98 | 83, 97 | mtbiri 330 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ dom 𝑦) |
99 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑗 ∈ V |
100 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑙 ∈ V |
101 | | fsnunfv 6953 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 7179 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗))) |
105 | 95, 104 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗) = (𝑙 · (𝐹‘𝑗))) |
106 | 105 | opeq2d 4765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉 = 〈𝑗, (𝑙 · (𝐹‘𝑗))〉) |
107 | 106 | sneqd 4525 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)‘𝑗)〉} = {〈𝑗, (𝑙 · (𝐹‘𝑗))〉}) |
108 | | ovex 7197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 · (𝐹‘𝑗)) ∈ V |
109 | | fmptsn 6933 |
. . . . . . . . . . . . . . . . . . . . . 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 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}) = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) |
113 | 112 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})) = (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))))) |
114 | | cmnmnd 19033 |
. . . . . . . . . . . . . . . . . . . 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 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑗 → (𝑙 · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗))) |
118 | 7, 117 | gsumsn 19186 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Mnd ∧ 𝑗 ∈ V ∧ (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗))) |
119 | 115, 116,
19, 118 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗))) |
120 | 113, 119 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗})) = (𝑙 · (𝐹‘𝑗))) |
121 | 88, 120 | oveq12d 7182 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹) ↾ {𝑗}))) = ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗)))) |
122 | 72, 121 | eqtr2d 2774 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹))) |
123 | 122 | eqeq1d 2740 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 )) |
124 | 15, 40, 123 | 3bitrd 308 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 )) |
125 | 103 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 = ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗)) |
126 | 125 | eqeq1d 2740 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 = 𝑌 ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) |
127 | 124, 126 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) |
128 | 127 | anassrs 471 |
. . . . . . . . . . 11
⊢
(((((𝑊 ∈ LMod
∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) ∧ 𝑦 finSupp 𝑌) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) |
129 | 128 | pm5.74da 804 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌)) ↔ (𝑦 finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
130 | | impexp 454 |
. . . . . . . . . . 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 226 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌)) |
133 | 132 | imbi1d 345 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) ↔ (𝑦 finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
134 | 129, 131,
133 | 3bitr4d 314 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗})))) → (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
135 | 134 | 2ralbidva 3110 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
136 | | breq1 5030 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
137 | | oveq1 7171 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥 ∘f · 𝐹) = ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) |
138 | 137 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑊 Σg (𝑥 ∘f · 𝐹)) = (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹))) |
139 | 138 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 )) |
140 | | fveq1 6667 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥‘𝑗) = ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗)) |
141 | 140 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑥‘𝑗) = 𝑌 ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) |
142 | 139, 141 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) |
143 | 136, 142 | imbi12d 348 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
144 | 143 | ralxpmap 8499 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝐼 → (∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
145 | 144 | adantl 485 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘f · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
146 | 135, 145 | bitr4d 285 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))) |
147 | | breq1 5030 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 finSupp 𝑌 ↔ 𝑥 finSupp 𝑌)) |
148 | 147 | ralrab 3591 |
. . . . . . 7
⊢
(∀𝑥 ∈
{𝑧 ∈
((Base‘𝑅)
↑m 𝐼)
∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑m 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
149 | 146, 148 | bitr4di 292 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
150 | | resima 5853 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) = (𝐹 “ (𝐼 ∖ {𝑗})) |
151 | 150 | eqcomi 2747 |
. . . . . . . . . . . 12
⊢ (𝐹 “ (𝐼 ∖ {𝑗})) = ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) |
152 | 151 | fveq2i 6671 |
. . . . . . . . . . 11
⊢
((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) = ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) |
153 | 152 | eleq2i 2824 |
. . . . . . . . . 10
⊢
((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})))) |
154 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
155 | 76, 30, 31 | sylancl 589 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
156 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝑊 ∈ LMod) |
157 | 24 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐼 ∖ {𝑗}) ∈ V) |
158 | 157 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐼 ∖ {𝑗}) ∈ V) |
159 | 154, 7, 12, 8, 34, 9, 155, 156, 158 | ellspd 20611 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))))) |
160 | 153, 159 | syl5bb 286 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))))) |
161 | 160 | imbi1d 345 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) |
162 | | r19.23v 3188 |
. . . . . . . 8
⊢
(∀𝑦 ∈
((Base‘𝑅)
↑m (𝐼
∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌)) |
163 | 161, 162 | bitr4di 292 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) |
164 | 163 | ralbidv 3109 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑m (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘f · (𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) |
165 | | islindf4.l |
. . . . . . . 8
⊢ 𝐿 = (Base‘(𝑅 freeLMod 𝐼)) |
166 | 8 | fvexi 6682 |
. . . . . . . . . . 11
⊢ 𝑅 ∈ V |
167 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼) |
168 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} |
169 | 167, 12, 34, 168 | frlmbas 20564 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ V ∧ 𝐼 ∈ 𝑋) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
170 | 166, 169 | mpan 690 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑋 → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
171 | 170 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
172 | 171 | adantr 484 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
173 | 165, 172 | eqtr4id 2792 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐿 = {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌}) |
174 | 173 | raleqdv 3315 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑m 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
175 | 149, 164,
174 | 3bitr4d 314 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
176 | 1, 175 | syl5bb 286 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
177 | 8 | lmodfgrp 19755 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑅 ∈ Grp) |
178 | 12, 34, 11 | grpinvnzcl 18282 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌})) |
179 | 177, 178 | sylan 583 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌})) |
180 | 12, 34, 11 | grpinvnzcl 18282 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌})) |
181 | 177, 180 | sylan 583 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌})) |
182 | | eldifi 4015 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) → 𝑘 ∈ (Base‘𝑅)) |
183 | 12, 11 | grpinvinv 18277 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ (Base‘𝑅)) →
((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘) |
184 | 177, 182,
183 | syl2an 599 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘) |
185 | 184 | eqcomd 2744 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) |
186 | | fveq2 6668 |
. . . . . . . . 9
⊢ (𝑙 = ((invg‘𝑅)‘𝑘) → ((invg‘𝑅)‘𝑙) = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) |
187 | 186 | rspceeqv 3539 |
. . . . . . . 8
⊢
((((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}) ∧ 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙)) |
188 | 181, 185,
187 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙)) |
189 | | oveq1 7171 |
. . . . . . . . . 10
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (𝑘 · (𝐹‘𝑗)) = (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗))) |
190 | 189 | eleq1d 2817 |
. . . . . . . . 9
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → ((𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
191 | 190 | notbid 321 |
. . . . . . . 8
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
192 | 191 | adantl 485 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 = ((invg‘𝑅)‘𝑙)) → (¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
193 | 179, 188,
192 | ralxfrd 5272 |
. . . . . 6
⊢ (𝑊 ∈ LMod →
(∀𝑘 ∈
((Base‘𝑅) ∖
{𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
194 | 193 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
195 | 194 | adantr 484 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
196 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → 𝑗 ∈ 𝐼) |
197 | 34 | fvexi 6682 |
. . . . . . . . 9
⊢ 𝑌 ∈ V |
198 | 197 | fvconst2 6970 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝐼 → ((𝐼 × {𝑌})‘𝑗) = 𝑌) |
199 | 196, 198 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝐼 × {𝑌})‘𝑗) = 𝑌) |
200 | 199 | eqeq2d 2749 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗) ↔ (𝑥‘𝑗) = 𝑌)) |
201 | 200 | imbi2d 344 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
202 | 201 | ralbidva 3108 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
203 | 176, 195,
202 | 3bitr4d 314 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
204 | 203 | ralbidva 3108 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
205 | 7, 9, 154, 8, 12, 34 | islindf2 20623 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
206 | 167, 12, 165 | frlmbasf 20569 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅)) |
207 | 206 | 3ad2antl2 1187 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅)) |
208 | 207 | ffnd 6499 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥 Fn 𝐼) |
209 | | fnconstg 6560 |
. . . . . . 7
⊢ (𝑌 ∈ V → (𝐼 × {𝑌}) Fn 𝐼) |
210 | 197, 209 | ax-mp 5 |
. . . . . 6
⊢ (𝐼 × {𝑌}) Fn 𝐼 |
211 | | eqfnfv 6803 |
. . . . . 6
⊢ ((𝑥 Fn 𝐼 ∧ (𝐼 × {𝑌}) Fn 𝐼) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
212 | 208, 210,
211 | sylancl 589 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
213 | 212 | imbi2d 344 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
214 | 213 | ralbidva 3108 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
215 | | r19.21v 3089 |
. . . . 5
⊢
(∀𝑗 ∈
𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
216 | 215 | ralbii 3080 |
. . . 4
⊢
(∀𝑥 ∈
𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
217 | | ralcom 3257 |
. . . 4
⊢
(∀𝑥 ∈
𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
218 | 216, 217 | bitr3i 280 |
. . 3
⊢
(∀𝑥 ∈
𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
219 | 214, 218 | bitrdi 290 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
220 | 204, 205,
219 | 3bitr4d 314 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘f · 𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})))) |