Step | Hyp | Ref
| Expression |
1 | | raldifsni 4324 |
. . . . 5
⊢
(∀𝑙 ∈
((Base‘𝑅) ∖
{𝑌}) ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌)) |
2 | | simpll1 1100 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ LMod) |
3 | | simprll 802 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 ∈ (Base‘𝑅)) |
4 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐼⟶𝐵 ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑗) ∈ 𝐵) |
5 | 4 | 3ad2antl3 1225 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐹‘𝑗) ∈ 𝐵) |
6 | 5 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹‘𝑗) ∈ 𝐵) |
7 | | islindf4.b |
. . . . . . . . . . . . . . . . 17
⊢ 𝐵 = (Base‘𝑊) |
8 | | islindf4.r |
. . . . . . . . . . . . . . . . 17
⊢ 𝑅 = (Scalar‘𝑊) |
9 | | islindf4.t |
. . . . . . . . . . . . . . . . 17
⊢ · = (
·𝑠 ‘𝑊) |
10 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(invg‘𝑊) = (invg‘𝑊) |
11 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(invg‘𝑅) = (invg‘𝑅) |
12 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑅) =
(Base‘𝑅) |
13 | 7, 8, 9, 10, 11, 12 | lmodvsinv 19036 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗)))) |
14 | 2, 3, 6, 13 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗)))) |
15 | 14 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))))) |
16 | | lmodgrp 18870 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
17 | 2, 16 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Grp) |
18 | 7, 8, 9, 12 | lmodvscl 18880 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ (Base‘𝑅) ∧ (𝐹‘𝑗) ∈ 𝐵) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) |
19 | 2, 3, 6, 18 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) |
20 | | islindf4.z |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝑊) |
21 | | lmodcmn 18911 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd) |
22 | 2, 21 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ CMnd) |
23 | | simpll2 1101 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 ∈ 𝑋) |
24 | | difexg 4808 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑋 → (𝐼 ∖ {𝑗}) ∈ V) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐼 ∖ {𝑗}) ∈ V) |
26 | | simprlr 803 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) |
27 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((Base‘𝑅) ↑𝑚
(𝐼 ∖ {𝑗})) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅)) |
29 | | simpll3 1102 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹:𝐼⟶𝐵) |
30 | | difss 3737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∖ {𝑗}) ⊆ 𝐼 |
31 | | fssres 6070 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐼⟶𝐵 ∧ (𝐼 ∖ {𝑗}) ⊆ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
32 | 29, 30, 31 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
33 | 8, 12, 9, 7, 2, 28,
32, 25 | lcomf 18902 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘𝑓 · (𝐹 ↾ (𝐼 ∖ {𝑗}))):(𝐼 ∖ {𝑗})⟶𝐵) |
34 | | islindf4.y |
. . . . . . . . . . . . . . . . 17
⊢ 𝑌 = (0g‘𝑅) |
35 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 finSupp 𝑌) |
36 | 8, 12, 9, 7, 2, 28,
32, 25, 20, 34, 35 | lcomfsupp 18903 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∘𝑓 · (𝐹 ↾ (𝐼 ∖ {𝑗}))) finSupp 0 ) |
37 | 7, 20, 22, 25, 33, 36 | gsumcl 18316 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵) |
38 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘𝑊) = (+g‘𝑊) |
39 | 7, 38, 20, 10 | grpinvid2 17471 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Grp ∧ (𝑙 · (𝐹‘𝑗)) ∈ 𝐵 ∧ (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) ∈ 𝐵) → (((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 )) |
40 | 17, 19, 37, 39 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((invg‘𝑊)‘(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ ((𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 )) |
41 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑗 ∈ 𝐼) |
42 | | fsnunf2 6452 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) ∧ 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) → (𝑦 ∪ {〈𝑗, 𝑙〉}):𝐼⟶(Base‘𝑅)) |
43 | 28, 41, 3, 42 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}):𝐼⟶(Base‘𝑅)) |
44 | 8, 12, 9, 7, 2, 43,
29, 23 | lcomf 18902 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹):𝐼⟶𝐵) |
45 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝑗 ∈ 𝐼) |
46 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) → 𝑙 ∈ (Base‘𝑅)) |
47 | 45, 46 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) → (𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅))) |
48 | | elmapfun 7881 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ((Base‘𝑅) ↑𝑚
(𝐼 ∖ {𝑗})) → Fun 𝑦) |
49 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) → dom 𝑦 = (𝐼 ∖ {𝑗})) |
50 | | neldifsnd 4322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) |
51 | | df-nel 2898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ dom 𝑦) |
52 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
53 | 52 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (¬ 𝑗 ∈ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
54 | 51, 53 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → (𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
55 | 50, 54 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (dom
𝑦 = (𝐼 ∖ {𝑗}) → 𝑗 ∉ dom 𝑦) |
56 | 49, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) → 𝑗 ∉ dom 𝑦) |
57 | 27, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ((Base‘𝑅) ↑𝑚
(𝐼 ∖ {𝑗})) → 𝑗 ∉ dom 𝑦) |
58 | 48, 57 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ((Base‘𝑅) ↑𝑚
(𝐼 ∖ {𝑗})) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) |
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) |
60 | 59 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) → (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) |
61 | 47, 60 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) → ((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦))) |
62 | | funsnfsupp 8299 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌)) |
63 | 62 | bicomd 213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Base‘𝑅)) ∧ (Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦)) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
64 | 61, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
65 | 64 | biimpd 219 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) → (𝑦 finSupp 𝑌 → (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
66 | 65 | impr 649 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌) |
67 | 8, 12, 9, 7, 2, 43,
29, 23, 20, 34, 66 | lcomfsupp 18903 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) finSupp 0 ) |
68 | | incom 3805 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ({𝑗} ∩ (𝐼 ∖ {𝑗})) |
69 | | disjdif 4040 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑗} ∩ (𝐼 ∖ {𝑗})) = ∅ |
70 | 68, 69 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅ |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝐼 ∖ {𝑗}) ∩ {𝑗}) = ∅) |
72 | | difsnid 4341 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ 𝐼 → ((𝐼 ∖ {𝑗}) ∪ {𝑗}) = 𝐼) |
73 | 72 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ 𝐼 → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗})) |
74 | 41, 73 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐼 = ((𝐼 ∖ {𝑗}) ∪ {𝑗})) |
75 | 7, 20, 38, 22, 23, 44, 67, 71, 74 | gsumsplit 18328 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = ((𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ {𝑗})))) |
76 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V |
77 | | snex 4908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
{〈𝑗, 𝑙〉} ∈
V |
78 | 76, 77 | unex 6956 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∪ {〈𝑗, 𝑙〉}) ∈ V |
79 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹:𝐼⟶𝐵) |
80 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐼 ∈ 𝑋) |
81 | | fex 6490 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹:𝐼⟶𝐵 ∧ 𝐼 ∈ 𝑋) → 𝐹 ∈ V) |
82 | 79, 80, 81 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐹 ∈ V) |
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 ∈ V) |
84 | | offres 7163 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∈ V ∧ 𝐹 ∈ V) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘𝑓 · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
85 | 78, 83, 84 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘𝑓 · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
86 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦:(𝐼 ∖ {𝑗})⟶(Base‘𝑅) → 𝑦 Fn (𝐼 ∖ {𝑗})) |
87 | 28, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑦 Fn (𝐼 ∖ {𝑗})) |
88 | | neldifsn 4321 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ¬
𝑗 ∈ (𝐼 ∖ {𝑗}) |
89 | | fsnunres 6454 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 Fn (𝐼 ∖ {𝑗}) ∧ ¬ 𝑗 ∈ (𝐼 ∖ {𝑗})) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) = 𝑦) |
90 | 87, 88, 89 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) = 𝑦) |
91 | 90 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ↾ (𝐼 ∖ {𝑗})) ∘𝑓 · (𝐹 ↾ (𝐼 ∖ {𝑗}))) = (𝑦 ∘𝑓 · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
92 | 85, 91 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ (𝐼 ∖ {𝑗})) = (𝑦 ∘𝑓 · (𝐹 ↾ (𝐼 ∖ {𝑗})))) |
93 | 92 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ (𝐼 ∖ {𝑗}))) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) |
94 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹):𝐼⟶𝐵 → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) Fn 𝐼) |
95 | 44, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) Fn 𝐼) |
96 | | fnressn 6425 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) Fn 𝐼 ∧ 𝑗 ∈ 𝐼) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ {𝑗}) = {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)‘𝑗)〉}) |
97 | 95, 41, 96 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ {𝑗}) = {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)‘𝑗)〉}) |
98 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∪ {〈𝑗, 𝑙〉}):𝐼⟶(Base‘𝑅) → (𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼) |
99 | 43, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼) |
100 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹:𝐼⟶𝐵 → 𝐹 Fn 𝐼) |
101 | 29, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝐹 Fn 𝐼) |
102 | | fnfvof 6911 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∪ {〈𝑗, 𝑙〉}) Fn 𝐼 ∧ 𝐹 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑗 ∈ 𝐼)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)‘𝑗) = (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗))) |
103 | 99, 101, 23, 41, 102 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)‘𝑗) = (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗))) |
104 | | fndm 5990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → dom 𝑦 = (𝐼 ∖ {𝑗})) |
105 | 104 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 ∖ {𝑗}))) |
106 | 88, 105 | mtbiri 317 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 Fn (𝐼 ∖ {𝑗}) → ¬ 𝑗 ∈ dom 𝑦) |
107 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑗 ∈ V |
108 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑙 ∈ V |
109 | | fsnunfv 6453 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ V ∧ 𝑙 ∈ V ∧ ¬ 𝑗 ∈ dom 𝑦) → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑙) |
110 | 107, 108,
109 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑗 ∈ dom 𝑦 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑙) |
111 | 87, 106, 110 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑙) |
112 | 111 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗))) |
113 | 103, 112 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)‘𝑗) = (𝑙 · (𝐹‘𝑗))) |
114 | 113 | opeq2d 4409 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)‘𝑗)〉 = 〈𝑗, (𝑙 · (𝐹‘𝑗))〉) |
115 | 114 | sneqd 4189 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {〈𝑗, (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)‘𝑗)〉} = {〈𝑗, (𝑙 · (𝐹‘𝑗))〉}) |
116 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 · (𝐹‘𝑗)) ∈ V |
117 | | fmptsn 6433 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ V ∧ (𝑙 · (𝐹‘𝑗)) ∈ V) → {〈𝑗, (𝑙 · (𝐹‘𝑗))〉} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) |
118 | 107, 116,
117 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
{〈𝑗, (𝑙 · (𝐹‘𝑗))〉} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))) |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → {〈𝑗, (𝑙 · (𝐹‘𝑗))〉} = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) |
120 | 97, 115, 119 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ {𝑗}) = (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) |
121 | 120 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ {𝑗})) = (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗))))) |
122 | | cmnmnd 18208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ CMnd → 𝑊 ∈ Mnd) |
123 | 22, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑊 ∈ Mnd) |
124 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑗 ∈ V) |
125 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑗 → (𝑙 · (𝐹‘𝑗)) = (𝑙 · (𝐹‘𝑗))) |
126 | 7, 125 | gsumsn 18354 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Mnd ∧ 𝑗 ∈ V ∧ (𝑙 · (𝐹‘𝑗)) ∈ 𝐵) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗))) |
127 | 123, 124,
19, 126 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (𝑥 ∈ {𝑗} ↦ (𝑙 · (𝐹‘𝑗)))) = (𝑙 · (𝐹‘𝑗))) |
128 | 121, 127 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ {𝑗})) = (𝑙 · (𝐹‘𝑗))) |
129 | 93, 128 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ (𝐼 ∖ {𝑗})))(+g‘𝑊)(𝑊 Σg (((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹) ↾ {𝑗}))) = ((𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗)))) |
130 | 75, 129 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹))) |
131 | 130 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))(+g‘𝑊)(𝑙 · (𝐹‘𝑗))) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 )) |
132 | 15, 40, 131 | 3bitrd 294 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 )) |
133 | 111 | eqcomd 2628 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → 𝑙 = ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗)) |
134 | 133 | eqeq1d 2624 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (𝑙 = 𝑌 ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) |
135 | 132, 134 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))) ∧ 𝑦 finSupp 𝑌)) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) |
136 | 135 | anassrs 680 |
. . . . . . . . . . 11
⊢
(((((𝑊 ∈ LMod
∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) ∧ 𝑦 finSupp 𝑌) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) |
137 | 136 | pm5.74da 723 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) → ((𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌)) ↔ (𝑦 finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
138 | | impexp 462 |
. . . . . . . . . . 11
⊢ (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌))) |
139 | 138 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) → (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (𝑦 finSupp 𝑌 → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗})))) → 𝑙 = 𝑌)))) |
140 | 64 | bicomd 213 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) → ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌)) |
141 | 140 | imbi1d 331 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) → (((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) ↔ (𝑦 finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
142 | 137, 139,
141 | 3bitr4d 300 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Base‘𝑅) ∧ 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗})))) → (((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
143 | 142 | 2ralbidva 2988 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
144 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥 finSupp 𝑌 ↔ (𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌)) |
145 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥 ∘𝑓 · 𝐹) = ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) |
146 | 145 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹))) |
147 | 146 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 ↔ (𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 )) |
148 | | fveq1 6190 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (𝑥‘𝑗) = ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗)) |
149 | 148 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑥‘𝑗) = 𝑌 ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)) |
150 | 147, 149 | imbi12d 334 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → (((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌))) |
151 | 144, 150 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 ∪ {〈𝑗, 𝑙〉}) → ((𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
152 | 151 | ralxpmap 7907 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝐼 → (∀𝑥 ∈ ((Base‘𝑅) ↑𝑚 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
153 | 152 | adantl 482 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ ((Base‘𝑅) ↑𝑚 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))((𝑦 ∪ {〈𝑗, 𝑙〉}) finSupp 𝑌 → ((𝑊 Σg ((𝑦 ∪ {〈𝑗, 𝑙〉}) ∘𝑓 · 𝐹)) = 0 → ((𝑦 ∪ {〈𝑗, 𝑙〉})‘𝑗) = 𝑌)))) |
154 | 143, 153 | bitr4d 271 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑𝑚 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌)))) |
155 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 finSupp 𝑌 ↔ 𝑥 finSupp 𝑌)) |
156 | 155 | ralrab 3368 |
. . . . . . 7
⊢
(∀𝑥 ∈
{𝑧 ∈
((Base‘𝑅)
↑𝑚 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ∀𝑥 ∈ ((Base‘𝑅) ↑𝑚 𝐼)(𝑥 finSupp 𝑌 → ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
157 | 154, 156 | syl6bbr 278 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑𝑚 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
158 | | resima 5431 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) = (𝐹 “ (𝐼 ∖ {𝑗})) |
159 | 158 | eqcomi 2631 |
. . . . . . . . . . . 12
⊢ (𝐹 “ (𝐼 ∖ {𝑗})) = ((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})) |
160 | 159 | fveq2i 6194 |
. . . . . . . . . . 11
⊢
((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) = ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) |
161 | 160 | eleq2i 2693 |
. . . . . . . . . 10
⊢
((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗})))) |
162 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
163 | 79, 30, 31 | sylancl 694 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐹 ↾ (𝐼 ∖ {𝑗})):(𝐼 ∖ {𝑗})⟶𝐵) |
164 | | simpl1 1064 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝑊 ∈ LMod) |
165 | 24 | 3ad2ant2 1083 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐼 ∖ {𝑗}) ∈ V) |
166 | 165 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (𝐼 ∖ {𝑗}) ∈ V) |
167 | 162, 7, 12, 8, 34, 9, 163, 164, 166 | ellspd 20141 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘((𝐹 ↾ (𝐼 ∖ {𝑗})) “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))))) |
168 | 161, 167 | syl5bb 272 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → ((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∃𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))))) |
169 | 168 | imbi1d 331 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) |
170 | | r19.23v 3023 |
. . . . . . . 8
⊢
(∀𝑦 ∈
((Base‘𝑅)
↑𝑚 (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌) ↔ (∃𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))(𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌)) |
171 | 169, 170 | syl6bbr 278 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) |
172 | 171 | ralbidv 2986 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑙 ∈ (Base‘𝑅)∀𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝐼 ∖ {𝑗}))((𝑦 finSupp 𝑌 ∧ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) = (𝑊 Σg (𝑦 ∘𝑓
·
(𝐹 ↾ (𝐼 ∖ {𝑗}))))) → 𝑙 = 𝑌))) |
173 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑊)
∈ V |
174 | 8, 173 | eqeltri 2697 |
. . . . . . . . . . 11
⊢ 𝑅 ∈ V |
175 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼) |
176 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ ((Base‘𝑅) ↑𝑚
𝐼) ∣ 𝑧 finSupp 𝑌} = {𝑧 ∈ ((Base‘𝑅) ↑𝑚 𝐼) ∣ 𝑧 finSupp 𝑌} |
177 | 175, 12, 34, 176 | frlmbas 20099 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ V ∧ 𝐼 ∈ 𝑋) → {𝑧 ∈ ((Base‘𝑅) ↑𝑚 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
178 | 174, 177 | mpan 706 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑋 → {𝑧 ∈ ((Base‘𝑅) ↑𝑚 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
179 | 178 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → {𝑧 ∈ ((Base‘𝑅) ↑𝑚 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
180 | 179 | adantr 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → {𝑧 ∈ ((Base‘𝑅) ↑𝑚 𝐼) ∣ 𝑧 finSupp 𝑌} = (Base‘(𝑅 freeLMod 𝐼))) |
181 | | islindf4.l |
. . . . . . . 8
⊢ 𝐿 = (Base‘(𝑅 freeLMod 𝐼)) |
182 | 180, 181 | syl6reqr 2675 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → 𝐿 = {𝑧 ∈ ((Base‘𝑅) ↑𝑚 𝐼) ∣ 𝑧 finSupp 𝑌}) |
183 | 182 | raleqdv 3144 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌) ↔ ∀𝑥 ∈ {𝑧 ∈ ((Base‘𝑅) ↑𝑚 𝐼) ∣ 𝑧 finSupp 𝑌} ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
184 | 157, 172,
183 | 3bitr4d 300 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ (Base‘𝑅)((((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) → 𝑙 = 𝑌) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
185 | 1, 184 | syl5bb 272 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
186 | 8 | lmodfgrp 18872 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑅 ∈ Grp) |
187 | 12, 34, 11 | grpinvnzcl 17487 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌})) |
188 | 186, 187 | sylan 488 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑙) ∈ ((Base‘𝑅) ∖ {𝑌})) |
189 | 12, 34, 11 | grpinvnzcl 17487 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌})) |
190 | 186, 189 | sylan 488 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌})) |
191 | | eldifi 3732 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) → 𝑘 ∈ (Base‘𝑅)) |
192 | 12, 11 | grpinvinv 17482 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ 𝑘 ∈ (Base‘𝑅)) →
((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘) |
193 | 186, 191,
192 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ((invg‘𝑅)‘((invg‘𝑅)‘𝑘)) = 𝑘) |
194 | 193 | eqcomd 2628 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) |
195 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑙 = ((invg‘𝑅)‘𝑘) → ((invg‘𝑅)‘𝑙) = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) |
196 | 195 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (𝑙 = ((invg‘𝑅)‘𝑘) → (𝑘 = ((invg‘𝑅)‘𝑙) ↔ 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘)))) |
197 | 196 | rspcev 3309 |
. . . . . . . 8
⊢
((((invg‘𝑅)‘𝑘) ∈ ((Base‘𝑅) ∖ {𝑌}) ∧ 𝑘 = ((invg‘𝑅)‘((invg‘𝑅)‘𝑘))) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙)) |
198 | 190, 194,
197 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ ((Base‘𝑅) ∖ {𝑌})) → ∃𝑙 ∈ ((Base‘𝑅) ∖ {𝑌})𝑘 = ((invg‘𝑅)‘𝑙)) |
199 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (𝑘 · (𝐹‘𝑗)) = (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗))) |
200 | 199 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → ((𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
201 | 200 | notbid 308 |
. . . . . . . 8
⊢ (𝑘 = ((invg‘𝑅)‘𝑙) → (¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
202 | 201 | adantl 482 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 = ((invg‘𝑅)‘𝑙)) → (¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ¬
(((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
203 | 188, 198,
202 | ralxfrd 4879 |
. . . . . 6
⊢ (𝑊 ∈ LMod →
(∀𝑘 ∈
((Base‘𝑅) ∖
{𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
204 | 203 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
205 | 204 | adantr 481 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑙 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (((invg‘𝑅)‘𝑙) · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
206 | | simplr 792 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → 𝑗 ∈ 𝐼) |
207 | | fvex 6201 |
. . . . . . . . . 10
⊢
(0g‘𝑅) ∈ V |
208 | 34, 207 | eqeltri 2697 |
. . . . . . . . 9
⊢ 𝑌 ∈ V |
209 | 208 | fvconst2 6469 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝐼 → ((𝐼 × {𝑌})‘𝑗) = 𝑌) |
210 | 206, 209 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝐼 × {𝑌})‘𝑗) = 𝑌) |
211 | 210 | eqeq2d 2632 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → ((𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗) ↔ (𝑥‘𝑗) = 𝑌)) |
212 | 211 | imbi2d 330 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
213 | 212 | ralbidva 2985 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = 𝑌))) |
214 | 185, 205,
213 | 3bitr4d 300 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑗 ∈ 𝐼) → (∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
215 | 214 | ralbidva 2985 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
216 | 7, 9, 162, 8, 12, 34 | islindf2 20153 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑗 ∈ 𝐼 ∀𝑘 ∈ ((Base‘𝑅) ∖ {𝑌}) ¬ (𝑘 · (𝐹‘𝑗)) ∈ ((LSpan‘𝑊)‘(𝐹 “ (𝐼 ∖ {𝑗}))))) |
217 | 175, 12, 181 | frlmbasf 20104 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅)) |
218 | 217 | 3ad2antl2 1224 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥:𝐼⟶(Base‘𝑅)) |
219 | | ffn 6045 |
. . . . . . 7
⊢ (𝑥:𝐼⟶(Base‘𝑅) → 𝑥 Fn 𝐼) |
220 | 218, 219 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑥 Fn 𝐼) |
221 | | fnconstg 6093 |
. . . . . . 7
⊢ (𝑌 ∈ V → (𝐼 × {𝑌}) Fn 𝐼) |
222 | 208, 221 | ax-mp 5 |
. . . . . 6
⊢ (𝐼 × {𝑌}) Fn 𝐼 |
223 | | eqfnfv 6311 |
. . . . . 6
⊢ ((𝑥 Fn 𝐼 ∧ (𝐼 × {𝑌}) Fn 𝐼) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
224 | 220, 222,
223 | sylancl 694 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑥 = (𝐼 × {𝑌}) ↔ ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
225 | 224 | imbi2d 330 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) ∧ 𝑥 ∈ 𝐿) → (((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
226 | 225 | ralbidva 2985 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
227 | | r19.21v 2960 |
. . . . 5
⊢
(∀𝑗 ∈
𝐼 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
228 | 227 | ralbii 2980 |
. . . 4
⊢
(∀𝑥 ∈
𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
229 | | ralcom 3098 |
. . . 4
⊢
(∀𝑥 ∈
𝐿 ∀𝑗 ∈ 𝐼 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
230 | 228, 229 | bitr3i 266 |
. . 3
⊢
(∀𝑥 ∈
𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → ∀𝑗 ∈ 𝐼 (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗))) |
231 | 226, 230 | syl6bb 276 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})) ↔ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → (𝑥‘𝑗) = ((𝐼 × {𝑌})‘𝑗)))) |
232 | 215, 216,
231 | 3bitr4d 300 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟶𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑥 ∈ 𝐿 ((𝑊 Σg (𝑥 ∘𝑓
·
𝐹)) = 0 → 𝑥 = (𝐼 × {𝑌})))) |