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 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 → 𝑥 = ( 𝐼 × { 𝑌 } ) ) ) )