MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islindf4 Structured version   Visualization version   GIF version

Theorem islindf4 21260
Description: A family is independent iff it has no nontrivial representations of zero. (Contributed by Stefan O'Rear, 28-Feb-2015.)
Hypotheses
Ref Expression
islindf4.b 𝐡 = (Baseβ€˜π‘Š)
islindf4.r 𝑅 = (Scalarβ€˜π‘Š)
islindf4.t Β· = ( ·𝑠 β€˜π‘Š)
islindf4.z 0 = (0gβ€˜π‘Š)
islindf4.y π‘Œ = (0gβ€˜π‘…)
islindf4.l 𝐿 = (Baseβ€˜(𝑅 freeLMod 𝐼))
Assertion
Ref Expression
islindf4 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (𝐹 LIndF π‘Š ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ π‘₯ = (𝐼 Γ— {π‘Œ}))))
Distinct variable groups:   π‘₯,𝐡   π‘₯,𝐹   π‘₯,𝐼   π‘₯,𝐿   π‘₯,𝑅   π‘₯, Β·   π‘₯,π‘Š   π‘₯,𝑋   π‘₯,π‘Œ   π‘₯, 0

Proof of Theorem islindf4
Dummy variables 𝑗 π‘˜ 𝑙 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raldifsni 4756 . . . . 5 (βˆ€π‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘™ ∈ (Baseβ€˜π‘…)((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) β†’ 𝑙 = π‘Œ))
2 simpll1 1213 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ π‘Š ∈ LMod)
3 simprll 778 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑙 ∈ (Baseβ€˜π‘…))
4 ffvelcdm 7033 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐼⟢𝐡 ∧ 𝑗 ∈ 𝐼) β†’ (πΉβ€˜π‘—) ∈ 𝐡)
543ad2antl3 1188 . . . . . . . . . . . . . . . . 17 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (πΉβ€˜π‘—) ∈ 𝐡)
65adantr 482 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (πΉβ€˜π‘—) ∈ 𝐡)
7 islindf4.b . . . . . . . . . . . . . . . . 17 𝐡 = (Baseβ€˜π‘Š)
8 islindf4.r . . . . . . . . . . . . . . . . 17 𝑅 = (Scalarβ€˜π‘Š)
9 islindf4.t . . . . . . . . . . . . . . . . 17 Β· = ( ·𝑠 β€˜π‘Š)
10 eqid 2733 . . . . . . . . . . . . . . . . 17 (invgβ€˜π‘Š) = (invgβ€˜π‘Š)
11 eqid 2733 . . . . . . . . . . . . . . . . 17 (invgβ€˜π‘…) = (invgβ€˜π‘…)
12 eqid 2733 . . . . . . . . . . . . . . . . 17 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
137, 8, 9, 10, 11, 12lmodvsinv 20512 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ LMod ∧ 𝑙 ∈ (Baseβ€˜π‘…) ∧ (πΉβ€˜π‘—) ∈ 𝐡) β†’ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = ((invgβ€˜π‘Š)β€˜(𝑙 Β· (πΉβ€˜π‘—))))
142, 3, 6, 13syl3anc 1372 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = ((invgβ€˜π‘Š)β€˜(𝑙 Β· (πΉβ€˜π‘—))))
1514eqeq1d 2735 . . . . . . . . . . . . . 14 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ↔ ((invgβ€˜π‘Š)β€˜(𝑙 Β· (πΉβ€˜π‘—))) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))))
16 lmodgrp 20343 . . . . . . . . . . . . . . . 16 (π‘Š ∈ LMod β†’ π‘Š ∈ Grp)
172, 16syl 17 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ π‘Š ∈ Grp)
187, 8, 9, 12lmodvscl 20354 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ LMod ∧ 𝑙 ∈ (Baseβ€˜π‘…) ∧ (πΉβ€˜π‘—) ∈ 𝐡) β†’ (𝑙 Β· (πΉβ€˜π‘—)) ∈ 𝐡)
192, 3, 6, 18syl3anc 1372 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑙 Β· (πΉβ€˜π‘—)) ∈ 𝐡)
20 islindf4.z . . . . . . . . . . . . . . . 16 0 = (0gβ€˜π‘Š)
21 lmodcmn 20385 . . . . . . . . . . . . . . . . 17 (π‘Š ∈ LMod β†’ π‘Š ∈ CMnd)
222, 21syl 17 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ π‘Š ∈ CMnd)
23 simpll2 1214 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝐼 ∈ 𝑋)
24 difexg 5285 . . . . . . . . . . . . . . . . 17 (𝐼 ∈ 𝑋 β†’ (𝐼 βˆ– {𝑗}) ∈ V)
2523, 24syl 17 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝐼 βˆ– {𝑗}) ∈ V)
26 simprlr 779 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))
27 elmapi 8790 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})) β†’ 𝑦:(𝐼 βˆ– {𝑗})⟢(Baseβ€˜π‘…))
2826, 27syl 17 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑦:(𝐼 βˆ– {𝑗})⟢(Baseβ€˜π‘…))
29 simpll3 1215 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝐹:𝐼⟢𝐡)
30 difss 4092 . . . . . . . . . . . . . . . . . 18 (𝐼 βˆ– {𝑗}) βŠ† 𝐼
31 fssres 6709 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐼⟢𝐡 ∧ (𝐼 βˆ– {𝑗}) βŠ† 𝐼) β†’ (𝐹 β†Ύ (𝐼 βˆ– {𝑗})):(𝐼 βˆ– {𝑗})⟢𝐡)
3229, 30, 31sylancl 587 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝐹 β†Ύ (𝐼 βˆ– {𝑗})):(𝐼 βˆ– {𝑗})⟢𝐡)
338, 12, 9, 7, 2, 28, 32, 25lcomf 20376 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))):(𝐼 βˆ– {𝑗})⟢𝐡)
34 islindf4.y . . . . . . . . . . . . . . . . 17 π‘Œ = (0gβ€˜π‘…)
35 simprr 772 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑦 finSupp π‘Œ)
368, 12, 9, 7, 2, 28, 32, 25, 20, 34, 35lcomfsupp 20377 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))) finSupp 0 )
377, 20, 22, 25, 33, 36gsumcl 19697 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ∈ 𝐡)
38 eqid 2733 . . . . . . . . . . . . . . . 16 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
397, 38, 20, 10grpinvid2 18808 . . . . . . . . . . . . . . 15 ((π‘Š ∈ Grp ∧ (𝑙 Β· (πΉβ€˜π‘—)) ∈ 𝐡 ∧ (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ∈ 𝐡) β†’ (((invgβ€˜π‘Š)β€˜(𝑙 Β· (πΉβ€˜π‘—))) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ↔ ((π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))(+gβ€˜π‘Š)(𝑙 Β· (πΉβ€˜π‘—))) = 0 ))
4017, 19, 37, 39syl3anc 1372 . . . . . . . . . . . . . 14 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((invgβ€˜π‘Š)β€˜(𝑙 Β· (πΉβ€˜π‘—))) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ↔ ((π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))(+gβ€˜π‘Š)(𝑙 Β· (πΉβ€˜π‘—))) = 0 ))
41 simplr 768 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑗 ∈ 𝐼)
42 fsnunf2 7133 . . . . . . . . . . . . . . . . . . 19 ((𝑦:(𝐼 βˆ– {𝑗})⟢(Baseβ€˜π‘…) ∧ 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Baseβ€˜π‘…)) β†’ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}):𝐼⟢(Baseβ€˜π‘…))
4328, 41, 3, 42syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}):𝐼⟢(Baseβ€˜π‘…))
448, 12, 9, 7, 2, 43, 29, 23lcomf 20376 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹):𝐼⟢𝐡)
45 simpr 486 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ 𝑗 ∈ 𝐼)
46 simpl 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) β†’ 𝑙 ∈ (Baseβ€˜π‘…))
4745, 46anim12i 614 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Baseβ€˜π‘…)))
48 elmapfun 8807 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})) β†’ Fun 𝑦)
49 fdm 6678 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦:(𝐼 βˆ– {𝑗})⟢(Baseβ€˜π‘…) β†’ dom 𝑦 = (𝐼 βˆ– {𝑗}))
50 neldifsnd 4754 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (dom 𝑦 = (𝐼 βˆ– {𝑗}) β†’ Β¬ 𝑗 ∈ (𝐼 βˆ– {𝑗}))
51 df-nel 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 βˆ‰ dom 𝑦 ↔ Β¬ 𝑗 ∈ dom 𝑦)
52 eleq2 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑦 = (𝐼 βˆ– {𝑗}) β†’ (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 βˆ– {𝑗})))
5352notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (dom 𝑦 = (𝐼 βˆ– {𝑗}) β†’ (Β¬ 𝑗 ∈ dom 𝑦 ↔ Β¬ 𝑗 ∈ (𝐼 βˆ– {𝑗})))
5451, 53bitrid 283 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (dom 𝑦 = (𝐼 βˆ– {𝑗}) β†’ (𝑗 βˆ‰ dom 𝑦 ↔ Β¬ 𝑗 ∈ (𝐼 βˆ– {𝑗})))
5550, 54mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑦 = (𝐼 βˆ– {𝑗}) β†’ 𝑗 βˆ‰ dom 𝑦)
5627, 49, 553syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})) β†’ 𝑗 βˆ‰ dom 𝑦)
5748, 56jca 513 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})) β†’ (Fun 𝑦 ∧ 𝑗 βˆ‰ dom 𝑦))
5857adantl 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) β†’ (Fun 𝑦 ∧ 𝑗 βˆ‰ dom 𝑦))
5958adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (Fun 𝑦 ∧ 𝑗 βˆ‰ dom 𝑦))
6047, 59jca 513 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ ((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Baseβ€˜π‘…)) ∧ (Fun 𝑦 ∧ 𝑗 βˆ‰ dom 𝑦)))
61 funsnfsupp 9334 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Baseβ€˜π‘…)) ∧ (Fun 𝑦 ∧ 𝑗 βˆ‰ dom 𝑦)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ ↔ 𝑦 finSupp π‘Œ))
6261bicomd 222 . . . . . . . . . . . . . . . . . . . . 21 (((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Baseβ€˜π‘…)) ∧ (Fun 𝑦 ∧ 𝑗 βˆ‰ dom 𝑦)) β†’ (𝑦 finSupp π‘Œ ↔ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ))
6360, 62syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (𝑦 finSupp π‘Œ ↔ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ))
6463biimpd 228 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (𝑦 finSupp π‘Œ β†’ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ))
6564impr 456 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ)
668, 12, 9, 7, 2, 43, 29, 23, 20, 34, 65lcomfsupp 20377 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) finSupp 0 )
67 disjdifr 4433 . . . . . . . . . . . . . . . . . 18 ((𝐼 βˆ– {𝑗}) ∩ {𝑗}) = βˆ…
6867a1i 11 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝐼 βˆ– {𝑗}) ∩ {𝑗}) = βˆ…)
69 difsnid 4771 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ 𝐼 β†’ ((𝐼 βˆ– {𝑗}) βˆͺ {𝑗}) = 𝐼)
7069eqcomd 2739 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ 𝐼 β†’ 𝐼 = ((𝐼 βˆ– {𝑗}) βˆͺ {𝑗}))
7141, 70syl 17 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝐼 = ((𝐼 βˆ– {𝑗}) βˆͺ {𝑗}))
727, 20, 38, 22, 23, 44, 66, 68, 71gsumsplit 19710 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = ((π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗})))(+gβ€˜π‘Š)(π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗}))))
73 vex 3448 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
74 snex 5389 . . . . . . . . . . . . . . . . . . . . 21 {βŸ¨π‘—, π‘™βŸ©} ∈ V
7573, 74unex 7681 . . . . . . . . . . . . . . . . . . . 20 (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∈ V
76 simpl3 1194 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ 𝐹:𝐼⟢𝐡)
77 simpl2 1193 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ 𝐼 ∈ 𝑋)
7876, 77fexd 7178 . . . . . . . . . . . . . . . . . . . . 21 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ 𝐹 ∈ V)
7978adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝐹 ∈ V)
80 offres 7917 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∈ V ∧ 𝐹 ∈ V) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗})) = (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†Ύ (𝐼 βˆ– {𝑗})) ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))
8175, 79, 80sylancr 588 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗})) = (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†Ύ (𝐼 βˆ– {𝑗})) ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))
8228ffnd 6670 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑦 Fn (𝐼 βˆ– {𝑗}))
83 neldifsn 4753 . . . . . . . . . . . . . . . . . . . . 21 Β¬ 𝑗 ∈ (𝐼 βˆ– {𝑗})
84 fsnunres 7135 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 Fn (𝐼 βˆ– {𝑗}) ∧ Β¬ 𝑗 ∈ (𝐼 βˆ– {𝑗})) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†Ύ (𝐼 βˆ– {𝑗})) = 𝑦)
8582, 83, 84sylancl 587 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†Ύ (𝐼 βˆ– {𝑗})) = 𝑦)
8685oveq1d 7373 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†Ύ (𝐼 βˆ– {𝑗})) ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))) = (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))
8781, 86eqtrd 2773 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗})) = (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))
8887oveq2d 7374 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗}))) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))))
8944ffnd 6670 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) Fn 𝐼)
90 fnressn 7105 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) Fn 𝐼 ∧ 𝑗 ∈ 𝐼) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗}) = {βŸ¨π‘—, (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—)⟩})
9189, 41, 90syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗}) = {βŸ¨π‘—, (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—)⟩})
9243ffnd 6670 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) Fn 𝐼)
9329ffnd 6670 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝐹 Fn 𝐼)
94 fnfvof 7635 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) Fn 𝐼 ∧ 𝐹 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑗 ∈ 𝐼)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—) = (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) Β· (πΉβ€˜π‘—)))
9592, 93, 23, 41, 94syl22anc 838 . . . . . . . . . . . . . . . . . . . . . . 23 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—) = (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) Β· (πΉβ€˜π‘—)))
96 fndm 6606 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 Fn (𝐼 βˆ– {𝑗}) β†’ dom 𝑦 = (𝐼 βˆ– {𝑗}))
9796eleq2d 2820 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 Fn (𝐼 βˆ– {𝑗}) β†’ (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 βˆ– {𝑗})))
9883, 97mtbiri 327 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 Fn (𝐼 βˆ– {𝑗}) β†’ Β¬ 𝑗 ∈ dom 𝑦)
99 vex 3448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑗 ∈ V
100 vex 3448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑙 ∈ V
101 fsnunfv 7134 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ V ∧ 𝑙 ∈ V ∧ Β¬ 𝑗 ∈ dom 𝑦) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = 𝑙)
10299, 100, 101mp3an12 1452 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Β¬ 𝑗 ∈ dom 𝑦 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = 𝑙)
10382, 98, 1023syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = 𝑙)
104103oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . 23 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) Β· (πΉβ€˜π‘—)) = (𝑙 Β· (πΉβ€˜π‘—)))
10595, 104eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—) = (𝑙 Β· (πΉβ€˜π‘—)))
106105opeq2d 4838 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ βŸ¨π‘—, (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—)⟩ = βŸ¨π‘—, (𝑙 Β· (πΉβ€˜π‘—))⟩)
107106sneqd 4599 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ {βŸ¨π‘—, (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—)⟩} = {βŸ¨π‘—, (𝑙 Β· (πΉβ€˜π‘—))⟩})
108 ovex 7391 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 Β· (πΉβ€˜π‘—)) ∈ V
109 fmptsn 7114 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ V ∧ (𝑙 Β· (πΉβ€˜π‘—)) ∈ V) β†’ {βŸ¨π‘—, (𝑙 Β· (πΉβ€˜π‘—))⟩} = (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—))))
11099, 108, 109mp2an 691 . . . . . . . . . . . . . . . . . . . . 21 {βŸ¨π‘—, (𝑙 Β· (πΉβ€˜π‘—))⟩} = (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—)))
111110a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ {βŸ¨π‘—, (𝑙 Β· (πΉβ€˜π‘—))⟩} = (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—))))
11291, 107, 1113eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗}) = (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—))))
113112oveq2d 7374 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗})) = (π‘Š Ξ£g (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—)))))
114 cmnmnd 19584 . . . . . . . . . . . . . . . . . . . 20 (π‘Š ∈ CMnd β†’ π‘Š ∈ Mnd)
1152, 21, 1143syl 18 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ π‘Š ∈ Mnd)
11699a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑗 ∈ V)
117 eqidd 2734 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑗 β†’ (𝑙 Β· (πΉβ€˜π‘—)) = (𝑙 Β· (πΉβ€˜π‘—)))
1187, 117gsumsn 19736 . . . . . . . . . . . . . . . . . . 19 ((π‘Š ∈ Mnd ∧ 𝑗 ∈ V ∧ (𝑙 Β· (πΉβ€˜π‘—)) ∈ 𝐡) β†’ (π‘Š Ξ£g (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—)))) = (𝑙 Β· (πΉβ€˜π‘—)))
119115, 116, 19, 118syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—)))) = (𝑙 Β· (πΉβ€˜π‘—)))
120113, 119eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗})) = (𝑙 Β· (πΉβ€˜π‘—)))
12188, 120oveq12d 7376 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗})))(+gβ€˜π‘Š)(π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗}))) = ((π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))(+gβ€˜π‘Š)(𝑙 Β· (πΉβ€˜π‘—))))
12272, 121eqtr2d 2774 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))(+gβ€˜π‘Š)(𝑙 Β· (πΉβ€˜π‘—))) = (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)))
123122eqeq1d 2735 . . . . . . . . . . . . . 14 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))(+gβ€˜π‘Š)(𝑙 Β· (πΉβ€˜π‘—))) = 0 ↔ (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 ))
12415, 40, 1233bitrd 305 . . . . . . . . . . . . 13 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ↔ (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 ))
125103eqcomd 2739 . . . . . . . . . . . . . 14 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑙 = ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—))
126125eqeq1d 2735 . . . . . . . . . . . . 13 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑙 = π‘Œ ↔ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))
127124, 126imbi12d 345 . . . . . . . . . . . 12 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) β†’ 𝑙 = π‘Œ) ↔ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ)))
128127anassrs 469 . . . . . . . . . . 11 (((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) ∧ 𝑦 finSupp π‘Œ) β†’ (((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) β†’ 𝑙 = π‘Œ) ↔ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ)))
129128pm5.74da 803 . . . . . . . . . 10 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ ((𝑦 finSupp π‘Œ β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) β†’ 𝑙 = π‘Œ)) ↔ (𝑦 finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
130 impexp 452 . . . . . . . . . . 11 (((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ (𝑦 finSupp π‘Œ β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) β†’ 𝑙 = π‘Œ)))
131130a1i 11 . . . . . . . . . 10 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ (𝑦 finSupp π‘Œ β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) β†’ 𝑙 = π‘Œ))))
13263bicomd 222 . . . . . . . . . . 11 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ ↔ 𝑦 finSupp π‘Œ))
133132imbi1d 342 . . . . . . . . . 10 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ)) ↔ (𝑦 finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
134129, 131, 1333bitr4d 311 . . . . . . . . 9 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
1351342ralbidva 3207 . . . . . . . 8 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
136 breq1 5109 . . . . . . . . . . 11 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ (π‘₯ finSupp π‘Œ ↔ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ))
137 oveq1 7365 . . . . . . . . . . . . . 14 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ (π‘₯ ∘f Β· 𝐹) = ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹))
138137oveq2d 7374 . . . . . . . . . . . . 13 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ (π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)))
139138eqeq1d 2735 . . . . . . . . . . . 12 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 ↔ (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 ))
140 fveq1 6842 . . . . . . . . . . . . 13 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ (π‘₯β€˜π‘—) = ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—))
141140eqeq1d 2735 . . . . . . . . . . . 12 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ ((π‘₯β€˜π‘—) = π‘Œ ↔ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))
142139, 141imbi12d 345 . . . . . . . . . . 11 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ (((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ) ↔ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ)))
143136, 142imbi12d 345 . . . . . . . . . 10 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ ((π‘₯ finSupp π‘Œ β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)) ↔ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
144143ralxpmap 8837 . . . . . . . . 9 (𝑗 ∈ 𝐼 β†’ (βˆ€π‘₯ ∈ ((Baseβ€˜π‘…) ↑m 𝐼)(π‘₯ finSupp π‘Œ β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)) ↔ βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
145144adantl 483 . . . . . . . 8 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘₯ ∈ ((Baseβ€˜π‘…) ↑m 𝐼)(π‘₯ finSupp π‘Œ β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)) ↔ βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
146135, 145bitr4d 282 . . . . . . 7 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘₯ ∈ ((Baseβ€˜π‘…) ↑m 𝐼)(π‘₯ finSupp π‘Œ β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ))))
147 breq1 5109 . . . . . . . 8 (𝑧 = π‘₯ β†’ (𝑧 finSupp π‘Œ ↔ π‘₯ finSupp π‘Œ))
148147ralrab 3652 . . . . . . 7 (βˆ€π‘₯ ∈ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ) ↔ βˆ€π‘₯ ∈ ((Baseβ€˜π‘…) ↑m 𝐼)(π‘₯ finSupp π‘Œ β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
149146, 148bitr4di 289 . . . . . 6 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘₯ ∈ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
150 resima 5972 . . . . . . . . . . . . 13 ((𝐹 β†Ύ (𝐼 βˆ– {𝑗})) β€œ (𝐼 βˆ– {𝑗})) = (𝐹 β€œ (𝐼 βˆ– {𝑗}))
151150eqcomi 2742 . . . . . . . . . . . 12 (𝐹 β€œ (𝐼 βˆ– {𝑗})) = ((𝐹 β†Ύ (𝐼 βˆ– {𝑗})) β€œ (𝐼 βˆ– {𝑗}))
152151fveq2i 6846 . . . . . . . . . . 11 ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) = ((LSpanβ€˜π‘Š)β€˜((𝐹 β†Ύ (𝐼 βˆ– {𝑗})) β€œ (𝐼 βˆ– {𝑗})))
153152eleq2i 2826 . . . . . . . . . 10 ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜((𝐹 β†Ύ (𝐼 βˆ– {𝑗})) β€œ (𝐼 βˆ– {𝑗}))))
154 eqid 2733 . . . . . . . . . . 11 (LSpanβ€˜π‘Š) = (LSpanβ€˜π‘Š)
15576, 30, 31sylancl 587 . . . . . . . . . . 11 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (𝐹 β†Ύ (𝐼 βˆ– {𝑗})):(𝐼 βˆ– {𝑗})⟢𝐡)
156 simpl1 1192 . . . . . . . . . . 11 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ π‘Š ∈ LMod)
157243ad2ant2 1135 . . . . . . . . . . . 12 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (𝐼 βˆ– {𝑗}) ∈ V)
158157adantr 482 . . . . . . . . . . 11 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (𝐼 βˆ– {𝑗}) ∈ V)
159154, 7, 12, 8, 34, 9, 155, 156, 158ellspd 21224 . . . . . . . . . 10 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜((𝐹 β†Ύ (𝐼 βˆ– {𝑗})) β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆƒπ‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))(𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))))))
160153, 159bitrid 283 . . . . . . . . 9 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆƒπ‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))(𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))))))
161160imbi1d 342 . . . . . . . 8 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) β†’ 𝑙 = π‘Œ) ↔ (βˆƒπ‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))(𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ)))
162 r19.23v 3176 . . . . . . . 8 (βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ (βˆƒπ‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))(𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ))
163161, 162bitr4di 289 . . . . . . 7 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ)))
164163ralbidv 3171 . . . . . 6 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ (Baseβ€˜π‘…)((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ)))
165 islindf4.l . . . . . . . 8 𝐿 = (Baseβ€˜(𝑅 freeLMod 𝐼))
1668fvexi 6857 . . . . . . . . . . 11 𝑅 ∈ V
167 eqid 2733 . . . . . . . . . . . 12 (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼)
168 eqid 2733 . . . . . . . . . . . 12 {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} = {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ}
169167, 12, 34, 168frlmbas 21177 . . . . . . . . . . 11 ((𝑅 ∈ V ∧ 𝐼 ∈ 𝑋) β†’ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} = (Baseβ€˜(𝑅 freeLMod 𝐼)))
170166, 169mpan 689 . . . . . . . . . 10 (𝐼 ∈ 𝑋 β†’ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} = (Baseβ€˜(𝑅 freeLMod 𝐼)))
1711703ad2ant2 1135 . . . . . . . . 9 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} = (Baseβ€˜(𝑅 freeLMod 𝐼)))
172171adantr 482 . . . . . . . 8 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} = (Baseβ€˜(𝑅 freeLMod 𝐼)))
173165, 172eqtr4id 2792 . . . . . . 7 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ 𝐿 = {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ})
174173raleqdv 3312 . . . . . 6 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ) ↔ βˆ€π‘₯ ∈ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
175149, 164, 1743bitr4d 311 . . . . 5 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ (Baseβ€˜π‘…)((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
1761, 175bitrid 283 . . . 4 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
1778lmodfgrp 20345 . . . . . . . 8 (π‘Š ∈ LMod β†’ 𝑅 ∈ Grp)
17812, 34, 11grpinvnzcl 18824 . . . . . . . 8 ((𝑅 ∈ Grp ∧ 𝑙 ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ ((invgβ€˜π‘…)β€˜π‘™) ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}))
179177, 178sylan 581 . . . . . . 7 ((π‘Š ∈ LMod ∧ 𝑙 ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ ((invgβ€˜π‘…)β€˜π‘™) ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}))
18012, 34, 11grpinvnzcl 18824 . . . . . . . . 9 ((𝑅 ∈ Grp ∧ π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ ((invgβ€˜π‘…)β€˜π‘˜) ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}))
181177, 180sylan 581 . . . . . . . 8 ((π‘Š ∈ LMod ∧ π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ ((invgβ€˜π‘…)β€˜π‘˜) ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}))
182 eldifi 4087 . . . . . . . . . 10 (π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) β†’ π‘˜ ∈ (Baseβ€˜π‘…))
18312, 11grpinvinv 18819 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ π‘˜ ∈ (Baseβ€˜π‘…)) β†’ ((invgβ€˜π‘…)β€˜((invgβ€˜π‘…)β€˜π‘˜)) = π‘˜)
184177, 182, 183syl2an 597 . . . . . . . . 9 ((π‘Š ∈ LMod ∧ π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ ((invgβ€˜π‘…)β€˜((invgβ€˜π‘…)β€˜π‘˜)) = π‘˜)
185184eqcomd 2739 . . . . . . . 8 ((π‘Š ∈ LMod ∧ π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ π‘˜ = ((invgβ€˜π‘…)β€˜((invgβ€˜π‘…)β€˜π‘˜)))
186 fveq2 6843 . . . . . . . . 9 (𝑙 = ((invgβ€˜π‘…)β€˜π‘˜) β†’ ((invgβ€˜π‘…)β€˜π‘™) = ((invgβ€˜π‘…)β€˜((invgβ€˜π‘…)β€˜π‘˜)))
187186rspceeqv 3596 . . . . . . . 8 ((((invgβ€˜π‘…)β€˜π‘˜) ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) ∧ π‘˜ = ((invgβ€˜π‘…)β€˜((invgβ€˜π‘…)β€˜π‘˜))) β†’ βˆƒπ‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})π‘˜ = ((invgβ€˜π‘…)β€˜π‘™))
188181, 185, 187syl2anc 585 . . . . . . 7 ((π‘Š ∈ LMod ∧ π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ βˆƒπ‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})π‘˜ = ((invgβ€˜π‘…)β€˜π‘™))
189 oveq1 7365 . . . . . . . . . 10 (π‘˜ = ((invgβ€˜π‘…)β€˜π‘™) β†’ (π‘˜ Β· (πΉβ€˜π‘—)) = (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)))
190189eleq1d 2819 . . . . . . . . 9 (π‘˜ = ((invgβ€˜π‘…)β€˜π‘™) β†’ ((π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
191190notbid 318 . . . . . . . 8 (π‘˜ = ((invgβ€˜π‘…)β€˜π‘™) β†’ (Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
192191adantl 483 . . . . . . 7 ((π‘Š ∈ LMod ∧ π‘˜ = ((invgβ€˜π‘…)β€˜π‘™)) β†’ (Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
193179, 188, 192ralxfrd 5364 . . . . . 6 (π‘Š ∈ LMod β†’ (βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
1941933ad2ant1 1134 . . . . 5 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
195194adantr 482 . . . 4 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
196 simplr 768 . . . . . . . 8 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ π‘₯ ∈ 𝐿) β†’ 𝑗 ∈ 𝐼)
19734fvexi 6857 . . . . . . . . 9 π‘Œ ∈ V
198197fvconst2 7154 . . . . . . . 8 (𝑗 ∈ 𝐼 β†’ ((𝐼 Γ— {π‘Œ})β€˜π‘—) = π‘Œ)
199196, 198syl 17 . . . . . . 7 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ π‘₯ ∈ 𝐿) β†’ ((𝐼 Γ— {π‘Œ})β€˜π‘—) = π‘Œ)
200199eqeq2d 2744 . . . . . 6 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ π‘₯ ∈ 𝐿) β†’ ((π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—) ↔ (π‘₯β€˜π‘—) = π‘Œ))
201200imbi2d 341 . . . . 5 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ π‘₯ ∈ 𝐿) β†’ (((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
202201ralbidva 3169 . . . 4 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
203176, 195, 2023bitr4d 311 . . 3 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—))))
204203ralbidva 3169 . 2 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (βˆ€π‘— ∈ 𝐼 βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘— ∈ 𝐼 βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—))))
2057, 9, 154, 8, 12, 34islindf2 21236 . 2 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (𝐹 LIndF π‘Š ↔ βˆ€π‘— ∈ 𝐼 βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
206167, 12, 165frlmbasf 21182 . . . . . . . 8 ((𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐿) β†’ π‘₯:𝐼⟢(Baseβ€˜π‘…))
2072063ad2antl2 1187 . . . . . . 7 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ π‘₯ ∈ 𝐿) β†’ π‘₯:𝐼⟢(Baseβ€˜π‘…))
208207ffnd 6670 . . . . . 6 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ π‘₯ ∈ 𝐿) β†’ π‘₯ Fn 𝐼)
209 fnconstg 6731 . . . . . . 7 (π‘Œ ∈ V β†’ (𝐼 Γ— {π‘Œ}) Fn 𝐼)
210197, 209ax-mp 5 . . . . . 6 (𝐼 Γ— {π‘Œ}) Fn 𝐼
211 eqfnfv 6983 . . . . . 6 ((π‘₯ Fn 𝐼 ∧ (𝐼 Γ— {π‘Œ}) Fn 𝐼) β†’ (π‘₯ = (𝐼 Γ— {π‘Œ}) ↔ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
212208, 210, 211sylancl 587 . . . . 5 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ π‘₯ ∈ 𝐿) β†’ (π‘₯ = (𝐼 Γ— {π‘Œ}) ↔ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
213212imbi2d 341 . . . 4 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ π‘₯ ∈ 𝐿) β†’ (((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ π‘₯ = (𝐼 Γ— {π‘Œ})) ↔ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—))))
214213ralbidva 3169 . . 3 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ π‘₯ = (𝐼 Γ— {π‘Œ})) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—))))
215 r19.21v 3173 . . . . 5 (βˆ€π‘— ∈ 𝐼 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
216215ralbii 3093 . . . 4 (βˆ€π‘₯ ∈ 𝐿 βˆ€π‘— ∈ 𝐼 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
217 ralcom 3271 . . . 4 (βˆ€π‘₯ ∈ 𝐿 βˆ€π‘— ∈ 𝐼 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ βˆ€π‘— ∈ 𝐼 βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
218216, 217bitr3i 277 . . 3 (βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ βˆ€π‘— ∈ 𝐼 βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
219214, 218bitrdi 287 . 2 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ π‘₯ = (𝐼 Γ— {π‘Œ})) ↔ βˆ€π‘— ∈ 𝐼 βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—))))
220204, 205, 2193bitr4d 311 1 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (𝐹 LIndF π‘Š ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ π‘₯ = (𝐼 Γ— {π‘Œ}))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   βˆ‰ wnel 3046  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406  Vcvv 3444   βˆ– cdif 3908   βˆͺ cun 3909   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  {csn 4587  βŸ¨cop 4593   class class class wbr 5106   ↦ cmpt 5189   Γ— cxp 5632  dom cdm 5634   β†Ύ cres 5636   β€œ cima 5637  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358   ∘f cof 7616   ↑m cmap 8768   finSupp cfsupp 9308  Basecbs 17088  +gcplusg 17138  Scalarcsca 17141   ·𝑠 cvsca 17142  0gc0g 17326   Ξ£g cgsu 17327  Mndcmnd 18561  Grpcgrp 18753  invgcminusg 18754  CMndccmn 19567  LModclmod 20336  LSpanclspn 20447   freeLMod cfrlm 21168   LIndF clindf 21226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-er 8651  df-map 8770  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-sup 9383  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-z 12505  df-dec 12624  df-uz 12769  df-fz 13431  df-fzo 13574  df-seq 13913  df-hash 14237  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-hom 17162  df-cco 17163  df-0g 17328  df-gsum 17329  df-prds 17334  df-pws 17336  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-mhm 18606  df-submnd 18607  df-grp 18756  df-minusg 18757  df-sbg 18758  df-mulg 18878  df-subg 18930  df-ghm 19011  df-cntz 19102  df-cmn 19569  df-abl 19570  df-mgp 19902  df-ur 19919  df-ring 19971  df-subrg 20234  df-lmod 20338  df-lss 20408  df-lsp 20448  df-lmhm 20498  df-lbs 20551  df-sra 20649  df-rgmod 20650  df-nzr 20744  df-dsmm 21154  df-frlm 21169  df-uvc 21205  df-lindf 21228
This theorem is referenced by:  islindf5  21261  islinds5  32203  islbs5  32215  fedgmul  32383  matunitlindflem1  36120  aacllem  47334
  Copyright terms: Public domain W3C validator