Metamath Proof Explorer

Theorem islindf4

Description: A family is independent iff it has no nontrivial representations of zero. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Hypotheses islindf4.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
islindf4.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
islindf4.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
islindf4.z ⊢ 0 = ( 0g ‘ 𝑊 )
islindf4.y ⊢ 𝑌 = ( 0g ‘ 𝑅 )
islindf4.l ⊢ 𝐿 = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) )
Assertion islindf4 ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ) )

Proof

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 disjdifr ⊢ ( ( 𝐼 ∖ { 𝑗 } ) ∩ { 𝑗 } ) = ∅
69 68 a1i ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝐼 ∖ { 𝑗 } ) ∩ { 𝑗 } ) = ∅ )
70 difsnid ⊢ ( 𝑗 ∈ 𝐼 → ( ( 𝐼 ∖ { 𝑗 } ) ∪ { 𝑗 } ) = 𝐼 )
71 70 eqcomd ⊢ ( 𝑗 ∈ 𝐼 → 𝐼 = ( ( 𝐼 ∖ { 𝑗 } ) ∪ { 𝑗 } ) )
72 42 71 syl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝐼 = ( ( 𝐼 ∖ { 𝑗 } ) ∪ { 𝑗 } ) )
73 1 4 39 24 25 45 67 69 72 gsumsplit ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = ( ( 𝑊 Σg ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ( +g ‘ 𝑊 ) ( 𝑊 Σg ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) ) ) )
74 vex ⊢ 𝑦 ∈ V
75 snex ⊢ { ⟨ 𝑗 , 𝑙 ⟩ } ∈ V
76 74 75 unex ⊢ ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∈ V
77 simpl3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐹 : 𝐼 ⟶ 𝐵 )
78 simpl2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐼 ∈ 𝑋 )
79 77 78 fexd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐹 ∈ V )
80 79 adantr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝐹 ∈ V )
81 offres ⊢ ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∈ V ∧ 𝐹 ∈ V ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) = ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) )
82 76 80 81 sylancr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) = ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) )
83 30 ffnd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑦 Fn ( 𝐼 ∖ { 𝑗 } ) )
84 neldifsn ⊢ ¬ 𝑗 ∈ ( 𝐼 ∖ { 𝑗 } )
85 fsnunres ⊢ ( ( 𝑦 Fn ( 𝐼 ∖ { 𝑗 } ) ∧ ¬ 𝑗 ∈ ( 𝐼 ∖ { 𝑗 } ) ) → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) = 𝑦 )
86 83 84 85 sylancl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) = 𝑦 )
87 86 oveq1d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) = ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) )
88 82 87 eqtrd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) = ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) )
89 88 oveq2d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) )
90 45 ffnd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) Fn 𝐼 )
91 fnressn ⊢ ( ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) Fn 𝐼 ∧ 𝑗 ∈ 𝐼 ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) = { ⟨ 𝑗 , ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ‘ 𝑗 ) ⟩ } )
92 90 42 91 syl2anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) = { ⟨ 𝑗 , ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ‘ 𝑗 ) ⟩ } )
93 44 ffnd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) Fn 𝐼 )
94 31 ffnd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝐹 Fn 𝐼 )
95 fnfvof ⊢ ( ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) Fn 𝐼 ∧ 𝐹 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑋 ∧ 𝑗 ∈ 𝐼 ) ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ‘ 𝑗 ) = ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) · ( 𝐹 ‘ 𝑗 ) ) )
96 93 94 25 42 95 syl22anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ‘ 𝑗 ) = ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) · ( 𝐹 ‘ 𝑗 ) ) )
97 fndm ⊢ ( 𝑦 Fn ( 𝐼 ∖ { 𝑗 } ) → dom 𝑦 = ( 𝐼 ∖ { 𝑗 } ) )
98 97 eleq2d ⊢ ( 𝑦 Fn ( 𝐼 ∖ { 𝑗 } ) → ( 𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ ( 𝐼 ∖ { 𝑗 } ) ) )
99 84 98 mtbiri ⊢ ( 𝑦 Fn ( 𝐼 ∖ { 𝑗 } ) → ¬ 𝑗 ∈ dom 𝑦 )
100 vex ⊢ 𝑗 ∈ V
101 vex ⊢ 𝑙 ∈ V
102 fsnunfv ⊢ ( ( 𝑗 ∈ V ∧ 𝑙 ∈ V ∧ ¬ 𝑗 ∈ dom 𝑦 ) → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑙 )
103 100 101 102 mp3an12 ⊢ ( ¬ 𝑗 ∈ dom 𝑦 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑙 )
104 83 99 103 3syl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑙 )
105 104 oveq1d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) )
106 96 105 eqtrd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ‘ 𝑗 ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) )
107 106 opeq2d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ⟨ 𝑗 , ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ‘ 𝑗 ) ⟩ = ⟨ 𝑗 , ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ⟩ )
108 107 sneqd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → { ⟨ 𝑗 , ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ‘ 𝑗 ) ⟩ } = { ⟨ 𝑗 , ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ⟩ } )
109 ovex ⊢ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ∈ V
110 fmptsn ⊢ ( ( 𝑗 ∈ V ∧ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ∈ V ) → { ⟨ 𝑗 , ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ⟩ } = ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) )
111 100 109 110 mp2an ⊢ { ⟨ 𝑗 , ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ⟩ } = ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) )
112 111 a1i ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → { ⟨ 𝑗 , ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ⟩ } = ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) )
113 92 108 112 3eqtrd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) = ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) )
114 113 oveq2d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) ) = ( 𝑊 Σg ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) )
115 cmnmnd ⊢ ( 𝑊 ∈ CMnd → 𝑊 ∈ Mnd )
116 8 23 115 3syl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑊 ∈ Mnd )
117 100 a1i ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑗 ∈ V )
118 eqidd ⊢ ( 𝑥 = 𝑗 → ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) )
119 1 118 gsumsn ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑗 ∈ V ∧ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ∈ 𝐵 ) → ( 𝑊 Σg ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) )
120 116 117 22 119 syl3anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( 𝑥 ∈ { 𝑗 } ↦ ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) )
121 114 120 eqtrd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑊 Σg ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) ) = ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) )
122 89 121 oveq12d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑊 Σg ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ( +g ‘ 𝑊 ) ( 𝑊 Σg ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ↾ { 𝑗 } ) ) ) = ( ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ( +g ‘ 𝑊 ) ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) )
123 73 122 eqtr2d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ( +g ‘ 𝑊 ) ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) = ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) )
124 123 eqeq1d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ( +g ‘ 𝑊 ) ( 𝑙 · ( 𝐹 ‘ 𝑗 ) ) ) = 0 ↔ ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 ) )
125 18 41 124 3bitrd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ↔ ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 ) )
126 104 eqcomd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → 𝑙 = ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) )
127 126 eqeq1d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( 𝑙 = 𝑌 ↔ ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) )
128 125 127 imbi12d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ∧ 𝑦 finSupp 𝑌 ) ) → ( ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) )
129 128 anassrs ⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) ∧ 𝑦 finSupp 𝑌 ) → ( ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) )
130 129 pm5.74da ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( 𝑦 finSupp 𝑌 → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) → 𝑙 = 𝑌 ) ) ↔ ( 𝑦 finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) ) )
131 impexp ⊢ ( ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( 𝑦 finSupp 𝑌 → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) → 𝑙 = 𝑌 ) ) )
132 131 a1i ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( 𝑦 finSupp 𝑌 → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) → 𝑙 = 𝑌 ) ) ) )
133 64 bicomd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) finSupp 𝑌 ↔ 𝑦 finSupp 𝑌 ) )
134 133 imbi1d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) ↔ ( 𝑦 finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) ) )
135 130 132 134 3bitr4d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ ( 𝑙 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ) ) → ( ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) ) )
136 135 2ralbidva ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) ) )
137 breq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) → ( 𝑥 finSupp 𝑌 ↔ ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) finSupp 𝑌 ) )
138 oveq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) → ( 𝑥 ∘f · 𝐹 ) = ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) )
139 138 oveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) → ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) )
140 139 eqeq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 ↔ ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 ) )
141 fveq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) → ( 𝑥 ‘ 𝑗 ) = ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) )
142 141 eqeq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) → ( ( 𝑥 ‘ 𝑗 ) = 𝑌 ↔ ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) )
143 140 142 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) → ( ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ↔ ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) )
144 137 143 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) → ( ( 𝑥 finSupp 𝑌 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ↔ ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) ) )
145 144 ralxpmap ⊢ ( 𝑗 ∈ 𝐼 → ( ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ( 𝑥 finSupp 𝑌 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ↔ ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) ) )
146 145 adantl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ( 𝑥 finSupp 𝑌 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ↔ ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) finSupp 𝑌 → ( ( 𝑊 Σg ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ∘f · 𝐹 ) ) = 0 → ( ( 𝑦 ∪ { ⟨ 𝑗 , 𝑙 ⟩ } ) ‘ 𝑗 ) = 𝑌 ) ) ) )
147 136 146 bitr4d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ( 𝑥 finSupp 𝑌 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) ) )
148 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 finSupp 𝑌 ↔ 𝑥 finSupp 𝑌 ) )
149 148 ralrab ⊢ ( ∀ 𝑥 ∈ { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ↔ ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ( 𝑥 finSupp 𝑌 → ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) )
150 147 149 bitr4di ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑥 ∈ { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) )
151 resima ⊢ ( ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) “ ( 𝐼 ∖ { 𝑗 } ) ) = ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) )
152 151 eqcomi ⊢ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) = ( ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) “ ( 𝐼 ∖ { 𝑗 } ) )
153 152 fveq2i ⊢ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) = ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) “ ( 𝐼 ∖ { 𝑗 } ) ) )
154 153 eleq2i ⊢ ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) “ ( 𝐼 ∖ { 𝑗 } ) ) ) )
155 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
156 77 32 33 sylancl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) : ( 𝐼 ∖ { 𝑗 } ) ⟶ 𝐵 )
157 simpl1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝑊 ∈ LMod )
158 26 3ad2ant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐼 ∖ { 𝑗 } ) ∈ V )
159 158 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( 𝐼 ∖ { 𝑗 } ) ∈ V )
160 155 1 15 2 5 3 156 157 159 ellspd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) ) )
161 154 160 syl5bb ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) ) )
162 161 imbi1d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) → 𝑙 = 𝑌 ) ↔ ( ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ) )
163 r19.23v ⊢ ( ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ↔ ( ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) )
164 162 163 bitr4di ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ) )
165 164 ralbidv ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 ∖ { 𝑗 } ) ) ( ( 𝑦 finSupp 𝑌 ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) = ( 𝑊 Σg ( 𝑦 ∘f · ( 𝐹 ↾ ( 𝐼 ∖ { 𝑗 } ) ) ) ) ) → 𝑙 = 𝑌 ) ) )
166 2 fvexi ⊢ 𝑅 ∈ V
167 eqid ⊢ ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 freeLMod 𝐼 )
168 eqid ⊢ { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } = { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 }
169 167 15 5 168 frlmbas ⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ 𝑋 ) → { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
170 166 169 mpan ⊢ ( 𝐼 ∈ 𝑋 → { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
171 170 3ad2ant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
172 171 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } = ( Base ‘ ( 𝑅 freeLMod 𝐼 ) ) )
173 6 172 eqtr4id ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → 𝐿 = { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } )
174 173 raleqdv ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ↔ ∀ 𝑥 ∈ { 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑧 finSupp 𝑌 } ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) )
175 150 165 174 3bitr4d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( Base ‘ 𝑅 ) ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) → 𝑙 = 𝑌 ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) )
176 7 175 syl5bb ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) )
177 2 lmodfgrp ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Grp )
178 15 5 14 grpinvnzcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) )
179 177 178 sylan ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) )
180 15 5 14 grpinvnzcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) )
181 177 180 sylan ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) )
182 eldifi ⊢ ( 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) → 𝑘 ∈ ( Base ‘ 𝑅 ) )
183 15 14 grpinvinv ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑘 ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ) = 𝑘 )
184 177 182 183 syl2an ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ) = 𝑘 )
185 184 eqcomd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → 𝑘 = ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ) )
186 fveq2 ⊢ ( 𝑙 = ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) = ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ) )
187 186 rspceeqv ⊢ ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ∧ 𝑘 = ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝑘 ) ) ) → ∃ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) )
188 181 185 187 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ) → ∃ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) )
189 oveq1 ⊢ ( 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) → ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) = ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) )
190 189 eleq1d ⊢ ( 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) → ( ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) )
191 190 notbid ⊢ ( 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) → ( ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) )
192 191 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 = ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) ) → ( ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) )
193 179 188 192 ralxfrd ⊢ ( 𝑊 ∈ LMod → ( ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) )
194 193 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) )
195 194 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑙 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( ( ( invg ‘ 𝑅 ) ‘ 𝑙 ) · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) )
196 simplr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝐿 ) → 𝑗 ∈ 𝐼 )
197 5 fvexi ⊢ 𝑌 ∈ V
198 197 fvconst2 ⊢ ( 𝑗 ∈ 𝐼 → ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) = 𝑌 )
199 196 198 syl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) = 𝑌 )
200 199 eqeq2d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ↔ ( 𝑥 ‘ 𝑗 ) = 𝑌 ) )
201 200 imbi2d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) )
202 201 ralbidva ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = 𝑌 ) ) )
203 176 195 202 3bitr4d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑗 ∈ 𝐼 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) )
204 203 ralbidva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑗 ∈ 𝐼 ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ↔ ∀ 𝑗 ∈ 𝐼 ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) )
205 1 3 155 2 15 5 islindf2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑗 ∈ 𝐼 ∀ 𝑘 ∈ ( ( Base ‘ 𝑅 ) ∖ { 𝑌 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑗 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑗 } ) ) ) ) )
206 167 15 6 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐿 ) → 𝑥 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
207 206 3ad2antl2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → 𝑥 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
208 207 ffnd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → 𝑥 Fn 𝐼 )
209 fnconstg ⊢ ( 𝑌 ∈ V → ( 𝐼 × { 𝑌 } ) Fn 𝐼 )
210 197 209 ax-mp ⊢ ( 𝐼 × { 𝑌 } ) Fn 𝐼
211 eqfnfv ⊢ ( ( 𝑥 Fn 𝐼 ∧ ( 𝐼 × { 𝑌 } ) Fn 𝐼 ) → ( 𝑥 = ( 𝐼 × { 𝑌 } ) ↔ ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) )
212 208 210 211 sylancl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( 𝑥 = ( 𝐼 × { 𝑌 } ) ↔ ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) )
213 212 imbi2d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) ∧ 𝑥 ∈ 𝐿 ) → ( ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ↔ ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) )
214 213 ralbidva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) )
215 r19.21v ⊢ ( ∀ 𝑗 ∈ 𝐼 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) )
216 215 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐿 ∀ 𝑗 ∈ 𝐼 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) )
217 ralcom ⊢ ( ∀ 𝑥 ∈ 𝐿 ∀ 𝑗 ∈ 𝐼 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝐼 ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) )
218 216 217 bitr3i ⊢ ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ∀ 𝑗 ∈ 𝐼 ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝐼 ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) )
219 214 218 bitrdi ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ↔ ∀ 𝑗 ∈ 𝐼 ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → ( 𝑥 ‘ 𝑗 ) = ( ( 𝐼 × { 𝑌 } ) ‘ 𝑗 ) ) ) )
220 204 205 219 3bitr4d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑥 ∈ 𝐿 ( ( 𝑊 Σg ( 𝑥 ∘f · 𝐹 ) ) = 0 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ) )