Step |
Hyp |
Ref |
Expression |
1 |
|
islindf4.b |
⊢ 𝐵 = ( Base ‘ 𝑊 ) |
2 |
|
islindf4.r |
⊢ 𝑅 = ( Scalar ‘ 𝑊 ) |
3 |
|
islindf4.t |
⊢ · = ( ·𝑠 ‘ 𝑊 ) |
4 |
|
islindf4.z |
⊢ 0 = ( 0g ‘ 𝑊 ) |
5 |
|
islindf4.y |
⊢ 𝑌 = ( 0g ‘ 𝑅 ) |
6 |
|
islindf4.l |
⊢ 𝐿 = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) |
7 |
|
raldifsni |
⊢ ( ∀ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) → 𝑙 = 𝑌 ) ) |
8 |
|
simpll1 |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑊 ∈ LMod ) |
9 |
|
simprll |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑙 ∈ ( Base ‘ 𝑅 ) ) |
10 |
|
ffvelrn |
⊢ ( ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝑗 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝐵 ) |
11 |
10
|
3ad2antl3 |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝐵 ) |
12 |
11
|
adantr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝐵 ) |
13 |
|
eqid |
⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 ) |
14 |
|
eqid |
⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 ) |
15 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
16 |
1 2 3 13 14 15
|
lmodvsinv |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝐵 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) |
17 |
8 9 12 16
|
syl3anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) |
18 |
17
|
eqeq1d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ↔ ( ( invg ‘ 𝑊 ) ‘ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) ) |
19 |
|
lmodgrp |
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp ) |
20 |
8 19
|
syl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑊 ∈ Grp ) |
21 |
1 2 3 15
|
lmodvscl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐹 ‘ 𝑗 ) ∈ 𝐵 ) → ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ∈ 𝐵 ) |
22 |
8 9 12 21
|
syl3anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ∈ 𝐵 ) |
23 |
|
lmodcmn |
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ CMnd ) |
24 |
8 23
|
syl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑊 ∈ CMnd ) |
25 |
|
simpll2 |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝐼 ∈ 𝑋 ) |
26 |
|
difexg |
⊢ ( 𝐼 ∈ 𝑋 → ( 𝐼 ∖ { 𝑗 } ) ∈ V ) |
27 |
25 26
|
syl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝐼 ∖ { 𝑗 } ) ∈ V ) |
28 |
|
simprlr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) |
29 |
|
elmapi |
⊢ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) → 𝑦 : ( 𝐼 ∖ { 𝑗 } ) ⟶ ( Base ‘ 𝑅 ) ) |
30 |
28 29
|
syl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑦 : ( 𝐼 ∖ { 𝑗 } ) ⟶ ( Base ‘ 𝑅 ) ) |
31 |
|
simpll3 |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝐹 : 𝐼 ⟶ 𝐵 ) |
32 |
|
difss |
⊢ ( 𝐼 ∖ { 𝑗 } ) ⊆ 𝐼 |
33 |
|
fssres |
⊢ ( ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ ( 𝐼 ∖ { 𝑗 } ) ⊆ 𝐼 ) → ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) : ( 𝐼 ∖ { 𝑗 } ) ⟶ 𝐵 ) |
34 |
31 32 33
|
sylancl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) : ( 𝐼 ∖ { 𝑗 } ) ⟶ 𝐵 ) |
35 |
2 15 3 1 8 30 34 27
|
lcomf |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) : ( 𝐼 ∖ { 𝑗 } ) ⟶ 𝐵 ) |
36 |
|
simprr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑦 finSupp 𝑌 ) |
37 |
2 15 3 1 8 30 34 27 4 5 36
|
lcomfsupp |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) finSupp 0 ) |
38 |
1 4 24 27 35 37
|
gsumcl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ∈ 𝐵 ) |
39 |
|
eqid |
⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) |
40 |
1 39 4 13
|
grpinvid2 |
⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ∈ 𝐵 ∧ ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ∈ 𝐵 ) → ( ( ( invg ‘ 𝑊 ) ‘ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ↔ ( ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ( +g ‘ 𝑊 ) ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) = 0 ) ) |
41 |
20 22 38 40
|
syl3anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( invg ‘ 𝑊 ) ‘ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ↔ ( ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ( +g ‘ 𝑊 ) ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) = 0 ) ) |
42 |
|
simplr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑗 ∈ 𝐼 ) |
43 |
|
fsnunf2 |
⊢ ( ( 𝑦 : ( 𝐼 ∖ { 𝑗 } ) ⟶ ( Base ‘ 𝑅 ) ∧ 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
44 |
30 42 9 43
|
syl3anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
45 |
2 15 3 1 8 44 31 25
|
lcomf |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) : 𝐼 ⟶ 𝐵 ) |
46 |
|
simpr |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑗 ∈ 𝐼 ) |
47 |
|
simpl |
⊢ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) → 𝑙 ∈ ( Base ‘ 𝑅 ) ) |
48 |
46 47
|
anim12i |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ ( Base ‘ 𝑅 ) ) ) |
49 |
|
elmapfun |
⊢ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) → Fun 𝑦 ) |
50 |
|
fdm |
⊢ ( 𝑦 : ( 𝐼 ∖ { 𝑗 } ) ⟶ ( Base ‘ 𝑅 ) → dom 𝑦 = ( 𝐼 ∖ { 𝑗 } ) ) |
51 |
|
neldifsnd |
⊢ ( dom 𝑦 = ( 𝐼 ∖ { 𝑗 } ) → ¬ 𝑗 ∈ ( 𝐼 ∖ { 𝑗 } ) ) |
52 |
|
df-nel |
⊢ ( 𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ dom 𝑦 ) |
53 |
|
eleq2 |
⊢ ( dom 𝑦 = ( 𝐼 ∖ { 𝑗 } ) → ( 𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ ( 𝐼 ∖ { 𝑗 } ) ) ) |
54 |
53
|
notbid |
⊢ ( dom 𝑦 = ( 𝐼 ∖ { 𝑗 } ) → ( ¬ 𝑗 ∈ dom 𝑦 ↔ ¬ 𝑗 ∈ ( 𝐼 ∖ { 𝑗 } ) ) ) |
55 |
52 54
|
syl5bb |
⊢ ( dom 𝑦 = ( 𝐼 ∖ { 𝑗 } ) → ( 𝑗 ∉ dom 𝑦 ↔ ¬ 𝑗 ∈ ( 𝐼 ∖ { 𝑗 } ) ) ) |
56 |
51 55
|
mpbird |
⊢ ( dom 𝑦 = ( 𝐼 ∖ { 𝑗 } ) → 𝑗 ∉ dom 𝑦 ) |
57 |
29 50 56
|
3syl |
⊢ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) → 𝑗 ∉ dom 𝑦 ) |
58 |
49 57
|
jca |
⊢ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) → ( Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦 ) ) |
59 |
58
|
adantl |
⊢ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) → ( Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦 ) ) |
60 |
59
|
adantl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦 ) ) |
61 |
48 60
|
jca |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ ( Base ‘ 𝑅 ) ) ∧ ( Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦 ) ) ) |
62 |
|
funsnfsupp |
⊢ ( ( ( 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ ( Base ‘ 𝑅 ) ) ∧ ( Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦 ) ) → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌 ) ) |
63 |
62
|
bicomd |
⊢ ( ( ( 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ ( Base ‘ 𝑅 ) ) ∧ ( Fun 𝑦 ∧ 𝑗 ∉ dom 𝑦 ) ) → ( 𝑦 finSupp 𝑌 ↔ ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 ) ) |
64 |
61 63
|
syl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( 𝑦 finSupp 𝑌 ↔ ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 ) ) |
65 |
64
|
biimpd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( 𝑦 finSupp 𝑌 → ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 ) ) |
66 |
65
|
impr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 ) |
67 |
2 15 3 1 8 44 31 25 4 5 66
|
lcomfsupp |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) finSupp 0 ) |
68 |
|
incom |
⊢ ( ( 𝐼 ∖ { 𝑗 } ) ∩ { 𝑗 } ) = ( { 𝑗 } ∩ ( 𝐼 ∖ { 𝑗 } ) ) |
69 |
|
disjdif |
⊢ ( { 𝑗 } ∩ ( 𝐼 ∖ { 𝑗 } ) ) = ∅ |
70 |
68 69
|
eqtri |
⊢ ( ( 𝐼 ∖ { 𝑗 } ) ∩ { 𝑗 } ) = ∅ |
71 |
70
|
a1i |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝐼 ∖ { 𝑗 } ) ∩ { 𝑗 } ) = ∅ ) |
72 |
|
difsnid |
⊢ ( 𝑗 ∈ 𝐼 → ( ( 𝐼 ∖ { 𝑗 } ) ∪ { 𝑗 } ) = 𝐼 ) |
73 |
72
|
eqcomd |
⊢ ( 𝑗 ∈ 𝐼 → 𝐼 = ( ( 𝐼 ∖ { 𝑗 } ) ∪ { 𝑗 } ) ) |
74 |
42 73
|
syl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝐼 = ( ( 𝐼 ∖ { 𝑗 } ) ∪ { 𝑗 } ) ) |
75 |
1 4 39 24 25 45 67 71 74
|
gsumsplit |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = ( ( 𝑊 Σg ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ( +g ‘ 𝑊 ) ( 𝑊 Σg ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) ) ) ) |
76 |
|
vex |
⊢ 𝑦 ∈ V |
77 |
|
snex |
⊢ { 〈 𝑗 , 𝑙 〉 } ∈ V |
78 |
76 77
|
unex |
⊢ ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∈ V |
79 |
|
simpl3 |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐹 : 𝐼 ⟶ 𝐵 ) |
80 |
|
simpl2 |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐼 ∈ 𝑋 ) |
81 |
|
fex |
⊢ ( ( 𝐹 : 𝐼 ⟶ 𝐵 ∧ 𝐼 ∈ 𝑋 ) → 𝐹 ∈ V ) |
82 |
79 80 81
|
syl2anc |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐹 ∈ V ) |
83 |
82
|
adantr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝐹 ∈ V ) |
84 |
|
offres |
⊢ ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∈ V ∧ 𝐹 ∈ V ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) = ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) |
85 |
78 83 84
|
sylancr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) = ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) |
86 |
30
|
ffnd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑦 Fn ( 𝐼 ∖ { 𝑗 } ) ) |
87 |
|
neldifsn |
⊢ ¬ 𝑗 ∈ ( 𝐼 ∖ { 𝑗 } ) |
88 |
|
fsnunres |
⊢ ( ( 𝑦 Fn ( 𝐼 ∖ { 𝑗 } ) ∧ ¬ 𝑗 ∈ ( 𝐼 ∖ { 𝑗 } ) ) → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) = 𝑦 ) |
89 |
86 87 88
|
sylancl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) = 𝑦 ) |
90 |
89
|
oveq1d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) = ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) |
91 |
85 90
|
eqtrd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) = ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) |
92 |
91
|
oveq2d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) |
93 |
45
|
ffnd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) Fn 𝐼 ) |
94 |
|
fnressn |
⊢ ( ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) Fn 𝐼 ∧ 𝑗 ∈ 𝐼 ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) = { 〈 𝑗 , ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ‘ 𝑗 ) 〉 } ) |
95 |
93 42 94
|
syl2anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) = { 〈 𝑗 , ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ‘ 𝑗 ) 〉 } ) |
96 |
44
|
ffnd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) Fn 𝐼 ) |
97 |
31
|
ffnd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝐹 Fn 𝐼 ) |
98 |
|
fnfvof |
⊢ ( ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) Fn 𝐼 ∧ 𝐹 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑋 ∧ 𝑗 ∈ 𝐼 ) ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ‘ 𝑗 ) = ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) · ( 𝐹 ‘ 𝑗 ) ) ) |
99 |
96 97 25 42 98
|
syl22anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ‘ 𝑗 ) = ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) · ( 𝐹 ‘ 𝑗 ) ) ) |
100 |
|
fndm |
⊢ ( 𝑦 Fn ( 𝐼 ∖ { 𝑗 } ) → dom 𝑦 = ( 𝐼 ∖ { 𝑗 } ) ) |
101 |
100
|
eleq2d |
⊢ ( 𝑦 Fn ( 𝐼 ∖ { 𝑗 } ) → ( 𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ ( 𝐼 ∖ { 𝑗 } ) ) ) |
102 |
87 101
|
mtbiri |
⊢ ( 𝑦 Fn ( 𝐼 ∖ { 𝑗 } ) → ¬ 𝑗 ∈ dom 𝑦 ) |
103 |
|
vex |
⊢ 𝑗 ∈ V |
104 |
|
vex |
⊢ 𝑙 ∈ V |
105 |
|
fsnunfv |
⊢ ( ( 𝑗 ∈ V ∧ 𝑙 ∈ V ∧ ¬ 𝑗 ∈ dom 𝑦 ) → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑙 ) |
106 |
103 104 105
|
mp3an12 |
⊢ ( ¬ 𝑗 ∈ dom 𝑦 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑙 ) |
107 |
86 102 106
|
3syl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑙 ) |
108 |
107
|
oveq1d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) |
109 |
99 108
|
eqtrd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ‘ 𝑗 ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) |
110 |
109
|
opeq2d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 〈 𝑗 , ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ‘ 𝑗 ) 〉 = 〈 𝑗 , ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) 〉 ) |
111 |
110
|
sneqd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → { 〈 𝑗 , ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ‘ 𝑗 ) 〉 } = { 〈 𝑗 , ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) 〉 } ) |
112 |
|
ovex |
⊢ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ∈ V |
113 |
|
fmptsn |
⊢ ( ( 𝑗 ∈ V ∧ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ∈ V ) → { 〈 𝑗 , ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) 〉 } = ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) |
114 |
103 112 113
|
mp2an |
⊢ { 〈 𝑗 , ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) 〉 } = ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) |
115 |
114
|
a1i |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → { 〈 𝑗 , ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) 〉 } = ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) |
116 |
95 111 115
|
3eqtrd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) = ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) |
117 |
116
|
oveq2d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) ) = ( 𝑊 Σg ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) ) |
118 |
|
cmnmnd |
⊢ ( 𝑊 ∈ CMnd → 𝑊 ∈ Mnd ) |
119 |
8 23 118
|
3syl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑊 ∈ Mnd ) |
120 |
103
|
a1i |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑗 ∈ V ) |
121 |
|
eqidd |
⊢ ( 𝑥 = 𝑗 → ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) |
122 |
1 121
|
gsumsn |
⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑗 ∈ V ∧ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ∈ 𝐵 ) → ( 𝑊 Σg ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) |
123 |
119 120 22 122
|
syl3anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) |
124 |
117 123
|
eqtrd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) |
125 |
92 124
|
oveq12d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑊 Σg ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ( +g ‘ 𝑊 ) ( 𝑊 Σg ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) ) ) = ( ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ( +g ‘ 𝑊 ) ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) |
126 |
75 125
|
eqtr2d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ( +g ‘ 𝑊 ) ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) = ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) ) |
127 |
126
|
eqeq1d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ( +g ‘ 𝑊 ) ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) = 0 ↔ ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 ) ) |
128 |
18 41 127
|
3bitrd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ↔ ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 ) ) |
129 |
107
|
eqcomd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑙 = ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) ) |
130 |
129
|
eqeq1d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑙 = 𝑌 ↔ ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) |
131 |
128 130
|
imbi12d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ) |
132 |
131
|
anassrs |
⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) ∧ 𝑦 finSupp 𝑌 ) → ( ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ) |
133 |
132
|
pm5.74da |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( 𝑦 finSupp 𝑌 → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) → 𝑙 = 𝑌 ) ) ↔ ( 𝑦 finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ) ) |
134 |
|
impexp |
⊢ ( ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( 𝑦 finSupp 𝑌 → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) → 𝑙 = 𝑌 ) ) ) |
135 |
134
|
a1i |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( 𝑦 finSupp 𝑌 → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) → 𝑙 = 𝑌 ) ) ) ) |
136 |
64
|
bicomd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌 ) ) |
137 |
136
|
imbi1d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ↔ ( 𝑦 finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ) ) |
138 |
133 135 137
|
3bitr4d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ) ) |
139 |
138
|
2ralbidva |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ) ) |
140 |
|
breq1 |
⊢ ( 𝑥 = ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) → ( 𝑥 finSupp 𝑌 ↔ ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 ) ) |
141 |
|
oveq1 |
⊢ ( 𝑥 = ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) → ( 𝑥 ∘f · 𝐹 ) = ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) |
142 |
141
|
oveq2d |
⊢ ( 𝑥 = ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) → ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) ) |
143 |
142
|
eqeq1d |
⊢ ( 𝑥 = ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 ↔ ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 ) ) |
144 |
|
fveq1 |
⊢ ( 𝑥 = ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) → ( 𝑥 ‘ 𝑗 ) = ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) ) |
145 |
144
|
eqeq1d |
⊢ ( 𝑥 = ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) → ( ( 𝑥 ‘ 𝑗 ) = 𝑌 ↔ ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) |
146 |
143 145
|
imbi12d |
⊢ ( 𝑥 = ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) → ( ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ↔ ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ) |
147 |
140 146
|
imbi12d |
⊢ ( 𝑥 = ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) → ( ( 𝑥 finSupp 𝑌 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ↔ ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ) ) |
148 |
147
|
ralxpmap |
⊢ ( 𝑗 ∈ 𝐼 → ( ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ( 𝑥 finSupp 𝑌 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ↔ ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ) ) |
149 |
148
|
adantl |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ( 𝑥 finSupp 𝑌 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ↔ ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { 〈 𝑗 , 𝑙 〉 } ) ‘ 𝑗 ) = 𝑌 ) ) ) ) |
150 |
139 149
|
bitr4d |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ( 𝑥 finSupp 𝑌 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ) ) |
151 |
|
breq1 |
⊢ ( 𝑧 = 𝑥 → ( 𝑧 finSupp 𝑌 ↔ 𝑥 finSupp 𝑌 ) ) |
152 |
151
|
ralrab |
⊢ ( ∀ 𝑥 ∈ { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ↔ ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ( 𝑥 finSupp 𝑌 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ) |
153 |
150 152
|
bitr4di |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑥 ∈ { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ) |
154 |
|
resima |
⊢ ( ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) “ ( 𝐼 ∖ { 𝑗 } ) ) = ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) |
155 |
154
|
eqcomi |
⊢ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) = ( ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) “ ( 𝐼 ∖ { 𝑗 } ) ) |
156 |
155
|
fveq2i |
⊢ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) = ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) “ ( 𝐼 ∖ { 𝑗 } ) ) ) |
157 |
156
|
eleq2i |
⊢ ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) |
158 |
|
eqid |
⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 ) |
159 |
79 32 33
|
sylancl |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) : ( 𝐼 ∖ { 𝑗 } ) ⟶ 𝐵 ) |
160 |
|
simpl1 |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑊 ∈ LMod ) |
161 |
26
|
3ad2ant2 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐼 ∖ { 𝑗 } ) ∈ V ) |
162 |
161
|
adantr |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝐼 ∖ { 𝑗 } ) ∈ V ) |
163 |
158 1 15 2 5 3 159 160 162
|
ellspd |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) ) ) |
164 |
157 163
|
syl5bb |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) ) ) |
165 |
164
|
imbi1d |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) → 𝑙 = 𝑌 ) ↔ ( ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ) ) |
166 |
|
r19.23v |
⊢ ( ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ) |
167 |
165 166
|
bitr4di |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ) ) |
168 |
167
|
ralbidv |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ) ) |
169 |
2
|
fvexi |
⊢ 𝑅 ∈ V |
170 |
|
eqid |
⊢ ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 freeLMod 𝐼 ) |
171 |
|
eqid |
⊢ { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } = { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } |
172 |
170 15 5 171
|
frlmbas |
⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ 𝑋 ) → { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
173 |
169 172
|
mpan |
⊢ ( 𝐼 ∈ 𝑋 → { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
174 |
173
|
3ad2ant2 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
175 |
174
|
adantr |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) ) |
176 |
6 175
|
eqtr4id |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐿 = { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } ) |
177 |
176
|
raleqdv |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ↔ ∀ 𝑥 ∈ { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ) |
178 |
153 168 177
|
3bitr4d |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ) |
179 |
7 178
|
syl5bb |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ) |
180 |
2
|
lmodfgrp |
⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Grp ) |
181 |
15 5 14
|
grpinvnzcl |
⊢ ( ( 𝑅 ∈ Grp ∧ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) |
182 |
180 181
|
sylan |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) |
183 |
15 5 14
|
grpinvnzcl |
⊢ ( ( 𝑅 ∈ Grp ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) |
184 |
180 183
|
sylan |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) |
185 |
|
eldifi |
⊢ ( 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) → 𝑘 ∈ ( Base ‘ 𝑅 ) ) |
186 |
15 14
|
grpinvinv |
⊢ ( ( 𝑅 ∈ Grp ∧ 𝑘 ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ) = 𝑘 ) |
187 |
180 185 186
|
syl2an |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ) = 𝑘 ) |
188 |
187
|
eqcomd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → 𝑘 = ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ) ) |
189 |
|
fveq2 |
⊢ ( 𝑙 = ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) = ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ) ) |
190 |
189
|
rspceeqv |
⊢ ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ∧ 𝑘 = ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ) ) → ∃ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) ) |
191 |
184 188 190
|
syl2anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ∃ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) ) |
192 |
|
oveq1 |
⊢ ( 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) → ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) = ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ) |
193 |
192
|
eleq1d |
⊢ ( 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) → ( ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) |
194 |
193
|
notbid |
⊢ ( 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) → ( ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) |
195 |
194
|
adantl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) ) → ( ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) |
196 |
182 191 195
|
ralxfrd |
⊢ ( 𝑊 ∈ LMod → ( ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) |
197 |
196
|
3ad2ant1 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) |
198 |
197
|
adantr |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) |
199 |
|
simplr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝐿 ) → 𝑗 ∈ 𝐼 ) |
200 |
5
|
fvexi |
⊢ 𝑌 ∈ V |
201 |
200
|
fvconst2 |
⊢ ( 𝑗 ∈ 𝐼 → ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) = 𝑌 ) |
202 |
199 201
|
syl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) = 𝑌 ) |
203 |
202
|
eqeq2d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ↔ ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) |
204 |
203
|
imbi2d |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ) |
205 |
204
|
ralbidva |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ) |
206 |
179 198 205
|
3bitr4d |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) ) |
207 |
206
|
ralbidva |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑗 ∈ 𝐼 ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑗 ∈ 𝐼 ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) ) |
208 |
1 3 158 2 15 5
|
islindf2 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑗 ∈ 𝐼 ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) |
209 |
170 15 6
|
frlmbasf |
⊢ ( ( 𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐿 ) → 𝑥 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
210 |
209
|
3ad2antl2 |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → 𝑥 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
211 |
210
|
ffnd |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → 𝑥 Fn 𝐼 ) |
212 |
|
fnconstg |
⊢ ( 𝑌 ∈ V → ( 𝐼 × { 𝑌 } ) Fn 𝐼 ) |
213 |
200 212
|
ax-mp |
⊢ ( 𝐼 × { 𝑌 } ) Fn 𝐼 |
214 |
|
eqfnfv |
⊢ ( ( 𝑥 Fn 𝐼 ∧ ( 𝐼 × { 𝑌 } ) Fn 𝐼 ) → ( 𝑥 = ( 𝐼 × { 𝑌 } ) ↔ ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) |
215 |
211 213 214
|
sylancl |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑥 = ( 𝐼 × { 𝑌 } ) ↔ ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) |
216 |
215
|
imbi2d |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ↔ ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) ) |
217 |
216
|
ralbidva |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) ) |
218 |
|
r19.21v |
⊢ ( ∀ 𝑗 ∈ 𝐼 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) |
219 |
218
|
ralbii |
⊢ ( ∀ 𝑥 ∈ 𝐿 ∀ 𝑗 ∈ 𝐼 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) |
220 |
|
ralcom |
⊢ ( ∀ 𝑥 ∈ 𝐿 ∀ 𝑗 ∈ 𝐼 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝐼 ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) |
221 |
219 220
|
bitr3i |
⊢ ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝐼 ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) |
222 |
217 221
|
bitrdi |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ↔ ∀ 𝑗 ∈ 𝐼 ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) ) |
223 |
207 208 222
|
3bitr4d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ) ) |