MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islindf4 Structured version   Visualization version   GIF version
Theorem islindf4 21392
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 4798 . . . . 5 (βˆ€π‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘™ ∈ (Baseβ€˜π‘…)((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) β†’ 𝑙 = π‘Œ))
2 simpll1 1212 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ π‘Š ∈ LMod)
3 simprll 777 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑙 ∈ (Baseβ€˜π‘…))
4 ffvelcdm 7083 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐼⟢𝐡 ∧ 𝑗 ∈ 𝐼) β†’ (πΉβ€˜π‘—) ∈ 𝐡)
543ad2antl3 1187 . . . . . . . . . . . . . . . . 17 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (πΉβ€˜π‘—) ∈ 𝐡)
65adantr 481 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (πΉβ€˜π‘—) ∈ 𝐡)
7 islindf4.b . . . . . . . . . . . . . . . . 17 𝐡 = (Baseβ€˜π‘Š)
8 islindf4.r . . . . . . . . . . . . . . . . 17 𝑅 = (Scalarβ€˜π‘Š)
9 islindf4.t . . . . . . . . . . . . . . . . 17 Β· = ( ·𝑠 β€˜π‘Š)
10 eqid 2732 . . . . . . . . . . . . . . . . 17 (invgβ€˜π‘Š) = (invgβ€˜π‘Š)
11 eqid 2732 . . . . . . . . . . . . . . . . 17 (invgβ€˜π‘…) = (invgβ€˜π‘…)
12 eqid 2732 . . . . . . . . . . . . . . . . 17 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
137, 8, 9, 10, 11, 12lmodvsinv 20646 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ LMod ∧ 𝑙 ∈ (Baseβ€˜π‘…) ∧ (πΉβ€˜π‘—) ∈ 𝐡) β†’ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = ((invgβ€˜π‘Š)β€˜(𝑙 Β· (πΉβ€˜π‘—))))
142, 3, 6, 13syl3anc 1371 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = ((invgβ€˜π‘Š)β€˜(𝑙 Β· (πΉβ€˜π‘—))))
1514eqeq1d 2734 . . . . . . . . . . . . . 14 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ↔ ((invgβ€˜π‘Š)β€˜(𝑙 Β· (πΉβ€˜π‘—))) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))))
16 lmodgrp 20477 . . . . . . . . . . . . . . . 16 (π‘Š ∈ LMod β†’ π‘Š ∈ Grp)
172, 16syl 17 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ π‘Š ∈ Grp)
187, 8, 9, 12lmodvscl 20488 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ LMod ∧ 𝑙 ∈ (Baseβ€˜π‘…) ∧ (πΉβ€˜π‘—) ∈ 𝐡) β†’ (𝑙 Β· (πΉβ€˜π‘—)) ∈ 𝐡)
192, 3, 6, 18syl3anc 1371 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑙 Β· (πΉβ€˜π‘—)) ∈ 𝐡)
20 islindf4.z . . . . . . . . . . . . . . . 16 0 = (0gβ€˜π‘Š)
21 lmodcmn 20519 . . . . . . . . . . . . . . . . 17 (π‘Š ∈ LMod β†’ π‘Š ∈ CMnd)
222, 21syl 17 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ π‘Š ∈ CMnd)
23 simpll2 1213 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝐼 ∈ 𝑋)
24 difexg 5327 . . . . . . . . . . . . . . . . 17 (𝐼 ∈ 𝑋 β†’ (𝐼 βˆ– {𝑗}) ∈ V)
2523, 24syl 17 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝐼 βˆ– {𝑗}) ∈ V)
26 simprlr 778 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))
27 elmapi 8842 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})) β†’ 𝑦:(𝐼 βˆ– {𝑗})⟢(Baseβ€˜π‘…))
2826, 27syl 17 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑦:(𝐼 βˆ– {𝑗})⟢(Baseβ€˜π‘…))
29 simpll3 1214 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝐹:𝐼⟢𝐡)
30 difss 4131 . . . . . . . . . . . . . . . . . 18 (𝐼 βˆ– {𝑗}) βŠ† 𝐼
31 fssres 6757 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐼⟢𝐡 ∧ (𝐼 βˆ– {𝑗}) βŠ† 𝐼) β†’ (𝐹 β†Ύ (𝐼 βˆ– {𝑗})):(𝐼 βˆ– {𝑗})⟢𝐡)
3229, 30, 31sylancl 586 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝐹 β†Ύ (𝐼 βˆ– {𝑗})):(𝐼 βˆ– {𝑗})⟢𝐡)
338, 12, 9, 7, 2, 28, 32, 25lcomf 20510 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))):(𝐼 βˆ– {𝑗})⟢𝐡)
34 islindf4.y . . . . . . . . . . . . . . . . 17 π‘Œ = (0gβ€˜π‘…)
35 simprr 771 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑦 finSupp π‘Œ)
368, 12, 9, 7, 2, 28, 32, 25, 20, 34, 35lcomfsupp 20511 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))) finSupp 0 )
377, 20, 22, 25, 33, 36gsumcl 19782 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ∈ 𝐡)
38 eqid 2732 . . . . . . . . . . . . . . . 16 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
397, 38, 20, 10grpinvid2 18876 . . . . . . . . . . . . . . 15 ((π‘Š ∈ Grp ∧ (𝑙 Β· (πΉβ€˜π‘—)) ∈ 𝐡 ∧ (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ∈ 𝐡) β†’ (((invgβ€˜π‘Š)β€˜(𝑙 Β· (πΉβ€˜π‘—))) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ↔ ((π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))(+gβ€˜π‘Š)(𝑙 Β· (πΉβ€˜π‘—))) = 0 ))
4017, 19, 37, 39syl3anc 1371 . . . . . . . . . . . . . 14 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((invgβ€˜π‘Š)β€˜(𝑙 Β· (πΉβ€˜π‘—))) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ↔ ((π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))(+gβ€˜π‘Š)(𝑙 Β· (πΉβ€˜π‘—))) = 0 ))
41 simplr 767 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑗 ∈ 𝐼)
42 fsnunf2 7183 . . . . . . . . . . . . . . . . . . 19 ((𝑦:(𝐼 βˆ– {𝑗})⟢(Baseβ€˜π‘…) ∧ 𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Baseβ€˜π‘…)) β†’ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}):𝐼⟢(Baseβ€˜π‘…))
4328, 41, 3, 42syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}):𝐼⟢(Baseβ€˜π‘…))
448, 12, 9, 7, 2, 43, 29, 23lcomf 20510 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹):𝐼⟢𝐡)
45 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ 𝑗 ∈ 𝐼)
46 simpl 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) β†’ 𝑙 ∈ (Baseβ€˜π‘…))
4745, 46anim12i 613 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Baseβ€˜π‘…)))
48 elmapfun 8859 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})) β†’ Fun 𝑦)
49 fdm 6726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦:(𝐼 βˆ– {𝑗})⟢(Baseβ€˜π‘…) β†’ dom 𝑦 = (𝐼 βˆ– {𝑗}))
50 neldifsnd 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (dom 𝑦 = (𝐼 βˆ– {𝑗}) β†’ Β¬ 𝑗 ∈ (𝐼 βˆ– {𝑗}))
51 df-nel 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 βˆ‰ dom 𝑦 ↔ Β¬ 𝑗 ∈ dom 𝑦)
52 eleq2 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑦 = (𝐼 βˆ– {𝑗}) β†’ (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 βˆ– {𝑗})))
5352notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (dom 𝑦 = (𝐼 βˆ– {𝑗}) β†’ (Β¬ 𝑗 ∈ dom 𝑦 ↔ Β¬ 𝑗 ∈ (𝐼 βˆ– {𝑗})))
5451, 53bitrid 282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (dom 𝑦 = (𝐼 βˆ– {𝑗}) β†’ (𝑗 βˆ‰ dom 𝑦 ↔ Β¬ 𝑗 ∈ (𝐼 βˆ– {𝑗})))
5550, 54mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (dom 𝑦 = (𝐼 βˆ– {𝑗}) β†’ 𝑗 βˆ‰ dom 𝑦)
5627, 49, 553syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})) β†’ 𝑗 βˆ‰ dom 𝑦)
5748, 56jca 512 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})) β†’ (Fun 𝑦 ∧ 𝑗 βˆ‰ dom 𝑦))
5857adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) β†’ (Fun 𝑦 ∧ 𝑗 βˆ‰ dom 𝑦))
5958adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (Fun 𝑦 ∧ 𝑗 βˆ‰ dom 𝑦))
6047, 59jca 512 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ ((𝑗 ∈ 𝐼 ∧ 𝑙 ∈ (Baseβ€˜π‘…)) ∧ (Fun 𝑦 ∧ 𝑗 βˆ‰ dom 𝑦)))
61 funsnfsupp 9386 . . . . . . . . . . . . . . . . . . . . . 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 455 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ)
668, 12, 9, 7, 2, 43, 29, 23, 20, 34, 65lcomfsupp 20511 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) finSupp 0 )
67 disjdifr 4472 . . . . . . . . . . . . . . . . . 18 ((𝐼 βˆ– {𝑗}) ∩ {𝑗}) = βˆ…
6867a1i 11 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝐼 βˆ– {𝑗}) ∩ {𝑗}) = βˆ…)
69 difsnid 4813 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ 𝐼 β†’ ((𝐼 βˆ– {𝑗}) βˆͺ {𝑗}) = 𝐼)
7069eqcomd 2738 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ 𝐼 β†’ 𝐼 = ((𝐼 βˆ– {𝑗}) βˆͺ {𝑗}))
7141, 70syl 17 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝐼 = ((𝐼 βˆ– {𝑗}) βˆͺ {𝑗}))
727, 20, 38, 22, 23, 44, 66, 68, 71gsumsplit 19795 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = ((π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗})))(+gβ€˜π‘Š)(π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗}))))
73 vex 3478 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
74 snex 5431 . . . . . . . . . . . . . . . . . . . . 21 {βŸ¨π‘—, π‘™βŸ©} ∈ V
7573, 74unex 7732 . . . . . . . . . . . . . . . . . . . 20 (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∈ V
76 simpl3 1193 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ 𝐹:𝐼⟢𝐡)
77 simpl2 1192 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ 𝐼 ∈ 𝑋)
7876, 77fexd 7228 . . . . . . . . . . . . . . . . . . . . 21 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ 𝐹 ∈ V)
7978adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝐹 ∈ V)
80 offres 7969 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∈ V ∧ 𝐹 ∈ V) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗})) = (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†Ύ (𝐼 βˆ– {𝑗})) ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))
8175, 79, 80sylancr 587 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗})) = (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†Ύ (𝐼 βˆ– {𝑗})) ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))
8228ffnd 6718 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑦 Fn (𝐼 βˆ– {𝑗}))
83 neldifsn 4795 . . . . . . . . . . . . . . . . . . . . 21 Β¬ 𝑗 ∈ (𝐼 βˆ– {𝑗})
84 fsnunres 7185 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 Fn (𝐼 βˆ– {𝑗}) ∧ Β¬ 𝑗 ∈ (𝐼 βˆ– {𝑗})) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†Ύ (𝐼 βˆ– {𝑗})) = 𝑦)
8582, 83, 84sylancl 586 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†Ύ (𝐼 βˆ– {𝑗})) = 𝑦)
8685oveq1d 7423 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†Ύ (𝐼 βˆ– {𝑗})) ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))) = (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))
8781, 86eqtrd 2772 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗})) = (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))
8887oveq2d 7424 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗}))) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))))
8944ffnd 6718 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) Fn 𝐼)
90 fnressn 7155 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) Fn 𝐼 ∧ 𝑗 ∈ 𝐼) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗}) = {βŸ¨π‘—, (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—)⟩})
9189, 41, 90syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗}) = {βŸ¨π‘—, (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—)⟩})
9243ffnd 6718 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) Fn 𝐼)
9329ffnd 6718 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝐹 Fn 𝐼)
94 fnfvof 7686 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) Fn 𝐼 ∧ 𝐹 Fn 𝐼) ∧ (𝐼 ∈ 𝑋 ∧ 𝑗 ∈ 𝐼)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—) = (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) Β· (πΉβ€˜π‘—)))
9592, 93, 23, 41, 94syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—) = (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) Β· (πΉβ€˜π‘—)))
96 fndm 6652 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 Fn (𝐼 βˆ– {𝑗}) β†’ dom 𝑦 = (𝐼 βˆ– {𝑗}))
9796eleq2d 2819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 Fn (𝐼 βˆ– {𝑗}) β†’ (𝑗 ∈ dom 𝑦 ↔ 𝑗 ∈ (𝐼 βˆ– {𝑗})))
9883, 97mtbiri 326 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 Fn (𝐼 βˆ– {𝑗}) β†’ Β¬ 𝑗 ∈ dom 𝑦)
99 vex 3478 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑗 ∈ V
100 vex 3478 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑙 ∈ V
101 fsnunfv 7184 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ V ∧ 𝑙 ∈ V ∧ Β¬ 𝑗 ∈ dom 𝑦) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = 𝑙)
10299, 100, 101mp3an12 1451 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Β¬ 𝑗 ∈ dom 𝑦 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = 𝑙)
10382, 98, 1023syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = 𝑙)
104103oveq1d 7423 . . . . . . . . . . . . . . . . . . . . . . 23 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) Β· (πΉβ€˜π‘—)) = (𝑙 Β· (πΉβ€˜π‘—)))
10595, 104eqtrd 2772 . . . . . . . . . . . . . . . . . . . . . 22 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—) = (𝑙 Β· (πΉβ€˜π‘—)))
106105opeq2d 4880 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ βŸ¨π‘—, (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—)⟩ = βŸ¨π‘—, (𝑙 Β· (πΉβ€˜π‘—))⟩)
107106sneqd 4640 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ {βŸ¨π‘—, (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)β€˜π‘—)⟩} = {βŸ¨π‘—, (𝑙 Β· (πΉβ€˜π‘—))⟩})
108 ovex 7441 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 Β· (πΉβ€˜π‘—)) ∈ V
109 fmptsn 7164 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ V ∧ (𝑙 Β· (πΉβ€˜π‘—)) ∈ V) β†’ {βŸ¨π‘—, (𝑙 Β· (πΉβ€˜π‘—))⟩} = (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—))))
11099, 108, 109mp2an 690 . . . . . . . . . . . . . . . . . . . . 21 {βŸ¨π‘—, (𝑙 Β· (πΉβ€˜π‘—))⟩} = (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—)))
111110a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ {βŸ¨π‘—, (𝑙 Β· (πΉβ€˜π‘—))⟩} = (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—))))
11291, 107, 1113eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗}) = (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—))))
113112oveq2d 7424 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗})) = (π‘Š Ξ£g (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—)))))
114 cmnmnd 19664 . . . . . . . . . . . . . . . . . . . 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 2733 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑗 β†’ (𝑙 Β· (πΉβ€˜π‘—)) = (𝑙 Β· (πΉβ€˜π‘—)))
1187, 117gsumsn 19821 . . . . . . . . . . . . . . . . . . 19 ((π‘Š ∈ Mnd ∧ 𝑗 ∈ V ∧ (𝑙 Β· (πΉβ€˜π‘—)) ∈ 𝐡) β†’ (π‘Š Ξ£g (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—)))) = (𝑙 Β· (πΉβ€˜π‘—)))
119115, 116, 19, 118syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g (π‘₯ ∈ {𝑗} ↦ (𝑙 Β· (πΉβ€˜π‘—)))) = (𝑙 Β· (πΉβ€˜π‘—)))
120113, 119eqtrd 2772 . . . . . . . . . . . . . . . . 17 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗})) = (𝑙 Β· (πΉβ€˜π‘—)))
12188, 120oveq12d 7426 . . . . . . . . . . . . . . . 16 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ (𝐼 βˆ– {𝑗})))(+gβ€˜π‘Š)(π‘Š Ξ£g (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹) β†Ύ {𝑗}))) = ((π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))(+gβ€˜π‘Š)(𝑙 Β· (πΉβ€˜π‘—))))
12272, 121eqtr2d 2773 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))(+gβ€˜π‘Š)(𝑙 Β· (πΉβ€˜π‘—))) = (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)))
123122eqeq1d 2734 . . . . . . . . . . . . . 14 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))(+gβ€˜π‘Š)(𝑙 Β· (πΉβ€˜π‘—))) = 0 ↔ (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 ))
12415, 40, 1233bitrd 304 . . . . . . . . . . . . 13 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) ↔ (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 ))
125103eqcomd 2738 . . . . . . . . . . . . . 14 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ 𝑙 = ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—))
126125eqeq1d 2734 . . . . . . . . . . . . 13 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (𝑙 = π‘Œ ↔ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))
127124, 126imbi12d 344 . . . . . . . . . . . 12 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ ((𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))) ∧ 𝑦 finSupp π‘Œ)) β†’ (((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) β†’ 𝑙 = π‘Œ) ↔ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ)))
128127anassrs 468 . . . . . . . . . . 11 (((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) ∧ 𝑦 finSupp π‘Œ) β†’ (((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) β†’ 𝑙 = π‘Œ) ↔ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ)))
129128pm5.74da 802 . . . . . . . . . 10 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ ((𝑦 finSupp π‘Œ β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))) β†’ 𝑙 = π‘Œ)) ↔ (𝑦 finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
130 impexp 451 . . . . . . . . . . 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 341 . . . . . . . . . 10 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ)) ↔ (𝑦 finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
134129, 131, 1333bitr4d 310 . . . . . . . . 9 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ (𝑙 ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗})))) β†’ (((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
1351342ralbidva 3216 . . . . . . . 8 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
136 breq1 5151 . . . . . . . . . . 11 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ (π‘₯ finSupp π‘Œ ↔ (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ))
137 oveq1 7415 . . . . . . . . . . . . . 14 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ (π‘₯ ∘f Β· 𝐹) = ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹))
138137oveq2d 7424 . . . . . . . . . . . . 13 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ (π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)))
139138eqeq1d 2734 . . . . . . . . . . . 12 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 ↔ (π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 ))
140 fveq1 6890 . . . . . . . . . . . . 13 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ (π‘₯β€˜π‘—) = ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—))
141140eqeq1d 2734 . . . . . . . . . . . 12 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ ((π‘₯β€˜π‘—) = π‘Œ ↔ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))
142139, 141imbi12d 344 . . . . . . . . . . 11 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ (((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ) ↔ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ)))
143136, 142imbi12d 344 . . . . . . . . . 10 (π‘₯ = (𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) β†’ ((π‘₯ finSupp π‘Œ β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)) ↔ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
144143ralxpmap 8889 . . . . . . . . 9 (𝑗 ∈ 𝐼 β†’ (βˆ€π‘₯ ∈ ((Baseβ€˜π‘…) ↑m 𝐼)(π‘₯ finSupp π‘Œ β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)) ↔ βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
145144adantl 482 . . . . . . . 8 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘₯ ∈ ((Baseβ€˜π‘…) ↑m 𝐼)(π‘₯ finSupp π‘Œ β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)) ↔ βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) finSupp π‘Œ β†’ ((π‘Š Ξ£g ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©}) ∘f Β· 𝐹)) = 0 β†’ ((𝑦 βˆͺ {βŸ¨π‘—, π‘™βŸ©})β€˜π‘—) = π‘Œ))))
146135, 145bitr4d 281 . . . . . . 7 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘₯ ∈ ((Baseβ€˜π‘…) ↑m 𝐼)(π‘₯ finSupp π‘Œ β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ))))
147 breq1 5151 . . . . . . . 8 (𝑧 = π‘₯ β†’ (𝑧 finSupp π‘Œ ↔ π‘₯ finSupp π‘Œ))
148147ralrab 3689 . . . . . . 7 (βˆ€π‘₯ ∈ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ) ↔ βˆ€π‘₯ ∈ ((Baseβ€˜π‘…) ↑m 𝐼)(π‘₯ finSupp π‘Œ β†’ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
149146, 148bitr4di 288 . . . . . 6 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘₯ ∈ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
150 resima 6015 . . . . . . . . . . . . 13 ((𝐹 β†Ύ (𝐼 βˆ– {𝑗})) β€œ (𝐼 βˆ– {𝑗})) = (𝐹 β€œ (𝐼 βˆ– {𝑗}))
151150eqcomi 2741 . . . . . . . . . . . 12 (𝐹 β€œ (𝐼 βˆ– {𝑗})) = ((𝐹 β†Ύ (𝐼 βˆ– {𝑗})) β€œ (𝐼 βˆ– {𝑗}))
152151fveq2i 6894 . . . . . . . . . . 11 ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) = ((LSpanβ€˜π‘Š)β€˜((𝐹 β†Ύ (𝐼 βˆ– {𝑗})) β€œ (𝐼 βˆ– {𝑗})))
153152eleq2i 2825 . . . . . . . . . 10 ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜((𝐹 β†Ύ (𝐼 βˆ– {𝑗})) β€œ (𝐼 βˆ– {𝑗}))))
154 eqid 2732 . . . . . . . . . . 11 (LSpanβ€˜π‘Š) = (LSpanβ€˜π‘Š)
15576, 30, 31sylancl 586 . . . . . . . . . . 11 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (𝐹 β†Ύ (𝐼 βˆ– {𝑗})):(𝐼 βˆ– {𝑗})⟢𝐡)
156 simpl1 1191 . . . . . . . . . . 11 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ π‘Š ∈ LMod)
157243ad2ant2 1134 . . . . . . . . . . . 12 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (𝐼 βˆ– {𝑗}) ∈ V)
158157adantr 481 . . . . . . . . . . 11 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (𝐼 βˆ– {𝑗}) ∈ V)
159154, 7, 12, 8, 34, 9, 155, 156, 158ellspd 21356 . . . . . . . . . 10 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜((𝐹 β†Ύ (𝐼 βˆ– {𝑗})) β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆƒπ‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))(𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))))))
160153, 159bitrid 282 . . . . . . . . 9 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ ((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆƒπ‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))(𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗})))))))
161160imbi1d 341 . . . . . . . 8 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) β†’ 𝑙 = π‘Œ) ↔ (βˆƒπ‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))(𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ)))
162 r19.23v 3182 . . . . . . . 8 (βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ) ↔ (βˆƒπ‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))(𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ))
163161, 162bitr4di 288 . . . . . . 7 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ)))
164163ralbidv 3177 . . . . . 6 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ (Baseβ€˜π‘…)((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘™ ∈ (Baseβ€˜π‘…)βˆ€π‘¦ ∈ ((Baseβ€˜π‘…) ↑m (𝐼 βˆ– {𝑗}))((𝑦 finSupp π‘Œ ∧ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) = (π‘Š Ξ£g (𝑦 ∘f Β· (𝐹 β†Ύ (𝐼 βˆ– {𝑗}))))) β†’ 𝑙 = π‘Œ)))
165 islindf4.l . . . . . . . 8 𝐿 = (Baseβ€˜(𝑅 freeLMod 𝐼))
1668fvexi 6905 . . . . . . . . . . 11 𝑅 ∈ V
167 eqid 2732 . . . . . . . . . . . 12 (𝑅 freeLMod 𝐼) = (𝑅 freeLMod 𝐼)
168 eqid 2732 . . . . . . . . . . . 12 {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} = {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ}
169167, 12, 34, 168frlmbas 21309 . . . . . . . . . . 11 ((𝑅 ∈ V ∧ 𝐼 ∈ 𝑋) β†’ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} = (Baseβ€˜(𝑅 freeLMod 𝐼)))
170166, 169mpan 688 . . . . . . . . . 10 (𝐼 ∈ 𝑋 β†’ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} = (Baseβ€˜(𝑅 freeLMod 𝐼)))
1711703ad2ant2 1134 . . . . . . . . 9 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} = (Baseβ€˜(𝑅 freeLMod 𝐼)))
172171adantr 481 . . . . . . . 8 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} = (Baseβ€˜(𝑅 freeLMod 𝐼)))
173165, 172eqtr4id 2791 . . . . . . 7 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ 𝐿 = {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ})
174173raleqdv 3325 . . . . . 6 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ) ↔ βˆ€π‘₯ ∈ {𝑧 ∈ ((Baseβ€˜π‘…) ↑m 𝐼) ∣ 𝑧 finSupp π‘Œ} ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
175149, 164, 1743bitr4d 310 . . . . 5 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ (Baseβ€˜π‘…)((((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) β†’ 𝑙 = π‘Œ) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
1761, 175bitrid 282 . . . 4 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
1778lmodfgrp 20479 . . . . . . . 8 (π‘Š ∈ LMod β†’ 𝑅 ∈ Grp)
17812, 34, 11grpinvnzcl 18894 . . . . . . . 8 ((𝑅 ∈ Grp ∧ 𝑙 ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ ((invgβ€˜π‘…)β€˜π‘™) ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}))
179177, 178sylan 580 . . . . . . 7 ((π‘Š ∈ LMod ∧ 𝑙 ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ ((invgβ€˜π‘…)β€˜π‘™) ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}))
18012, 34, 11grpinvnzcl 18894 . . . . . . . . 9 ((𝑅 ∈ Grp ∧ π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ ((invgβ€˜π‘…)β€˜π‘˜) ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}))
181177, 180sylan 580 . . . . . . . 8 ((π‘Š ∈ LMod ∧ π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ ((invgβ€˜π‘…)β€˜π‘˜) ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}))
182 eldifi 4126 . . . . . . . . . 10 (π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) β†’ π‘˜ ∈ (Baseβ€˜π‘…))
18312, 11grpinvinv 18889 . . . . . . . . . 10 ((𝑅 ∈ Grp ∧ π‘˜ ∈ (Baseβ€˜π‘…)) β†’ ((invgβ€˜π‘…)β€˜((invgβ€˜π‘…)β€˜π‘˜)) = π‘˜)
184177, 182, 183syl2an 596 . . . . . . . . 9 ((π‘Š ∈ LMod ∧ π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ ((invgβ€˜π‘…)β€˜((invgβ€˜π‘…)β€˜π‘˜)) = π‘˜)
185184eqcomd 2738 . . . . . . . 8 ((π‘Š ∈ LMod ∧ π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ π‘˜ = ((invgβ€˜π‘…)β€˜((invgβ€˜π‘…)β€˜π‘˜)))
186 fveq2 6891 . . . . . . . . 9 (𝑙 = ((invgβ€˜π‘…)β€˜π‘˜) β†’ ((invgβ€˜π‘…)β€˜π‘™) = ((invgβ€˜π‘…)β€˜((invgβ€˜π‘…)β€˜π‘˜)))
187186rspceeqv 3633 . . . . . . . 8 ((((invgβ€˜π‘…)β€˜π‘˜) ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) ∧ π‘˜ = ((invgβ€˜π‘…)β€˜((invgβ€˜π‘…)β€˜π‘˜))) β†’ βˆƒπ‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})π‘˜ = ((invgβ€˜π‘…)β€˜π‘™))
188181, 185, 187syl2anc 584 . . . . . . 7 ((π‘Š ∈ LMod ∧ π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})) β†’ βˆƒπ‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ})π‘˜ = ((invgβ€˜π‘…)β€˜π‘™))
189 oveq1 7415 . . . . . . . . . 10 (π‘˜ = ((invgβ€˜π‘…)β€˜π‘™) β†’ (π‘˜ Β· (πΉβ€˜π‘—)) = (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)))
190189eleq1d 2818 . . . . . . . . 9 (π‘˜ = ((invgβ€˜π‘…)β€˜π‘™) β†’ ((π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
191190notbid 317 . . . . . . . 8 (π‘˜ = ((invgβ€˜π‘…)β€˜π‘™) β†’ (Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
192191adantl 482 . . . . . . 7 ((π‘Š ∈ LMod ∧ π‘˜ = ((invgβ€˜π‘…)β€˜π‘™)) β†’ (Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
193179, 188, 192ralxfrd 5406 . . . . . 6 (π‘Š ∈ LMod β†’ (βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
1941933ad2ant1 1133 . . . . 5 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
195194adantr 481 . . . 4 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘™ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (((invgβ€˜π‘…)β€˜π‘™) Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
196 simplr 767 . . . . . . . 8 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ π‘₯ ∈ 𝐿) β†’ 𝑗 ∈ 𝐼)
19734fvexi 6905 . . . . . . . . 9 π‘Œ ∈ V
198197fvconst2 7204 . . . . . . . 8 (𝑗 ∈ 𝐼 β†’ ((𝐼 Γ— {π‘Œ})β€˜π‘—) = π‘Œ)
199196, 198syl 17 . . . . . . 7 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ π‘₯ ∈ 𝐿) β†’ ((𝐼 Γ— {π‘Œ})β€˜π‘—) = π‘Œ)
200199eqeq2d 2743 . . . . . 6 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ π‘₯ ∈ 𝐿) β†’ ((π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—) ↔ (π‘₯β€˜π‘—) = π‘Œ))
201200imbi2d 340 . . . . 5 ((((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) ∧ π‘₯ ∈ 𝐿) β†’ (((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
202201ralbidva 3175 . . . 4 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = π‘Œ)))
203176, 195, 2023bitr4d 310 . . 3 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ 𝑗 ∈ 𝐼) β†’ (βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—))))
204203ralbidva 3175 . 2 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (βˆ€π‘— ∈ 𝐼 βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗}))) ↔ βˆ€π‘— ∈ 𝐼 βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—))))
2057, 9, 154, 8, 12, 34islindf2 21368 . 2 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (𝐹 LIndF π‘Š ↔ βˆ€π‘— ∈ 𝐼 βˆ€π‘˜ ∈ ((Baseβ€˜π‘…) βˆ– {π‘Œ}) Β¬ (π‘˜ Β· (πΉβ€˜π‘—)) ∈ ((LSpanβ€˜π‘Š)β€˜(𝐹 β€œ (𝐼 βˆ– {𝑗})))))
206167, 12, 165frlmbasf 21314 . . . . . . . 8 ((𝐼 ∈ 𝑋 ∧ π‘₯ ∈ 𝐿) β†’ π‘₯:𝐼⟢(Baseβ€˜π‘…))
2072063ad2antl2 1186 . . . . . . 7 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ π‘₯ ∈ 𝐿) β†’ π‘₯:𝐼⟢(Baseβ€˜π‘…))
208207ffnd 6718 . . . . . 6 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ π‘₯ ∈ 𝐿) β†’ π‘₯ Fn 𝐼)
209 fnconstg 6779 . . . . . . 7 (π‘Œ ∈ V β†’ (𝐼 Γ— {π‘Œ}) Fn 𝐼)
210197, 209ax-mp 5 . . . . . 6 (𝐼 Γ— {π‘Œ}) Fn 𝐼
211 eqfnfv 7032 . . . . . 6 ((π‘₯ Fn 𝐼 ∧ (𝐼 Γ— {π‘Œ}) Fn 𝐼) β†’ (π‘₯ = (𝐼 Γ— {π‘Œ}) ↔ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
212208, 210, 211sylancl 586 . . . . 5 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ π‘₯ ∈ 𝐿) β†’ (π‘₯ = (𝐼 Γ— {π‘Œ}) ↔ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
213212imbi2d 340 . . . 4 (((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) ∧ π‘₯ ∈ 𝐿) β†’ (((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ π‘₯ = (𝐼 Γ— {π‘Œ})) ↔ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—))))
214213ralbidva 3175 . . 3 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ π‘₯ = (𝐼 Γ— {π‘Œ})) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—))))
215 r19.21v 3179 . . . . 5 (βˆ€π‘— ∈ 𝐼 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
216215ralbii 3093 . . . 4 (βˆ€π‘₯ ∈ 𝐿 βˆ€π‘— ∈ 𝐼 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
217 ralcom 3286 . . . 4 (βˆ€π‘₯ ∈ 𝐿 βˆ€π‘— ∈ 𝐼 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ βˆ€π‘— ∈ 𝐼 βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
218216, 217bitr3i 276 . . 3 (βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ βˆ€π‘— ∈ 𝐼 (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)) ↔ βˆ€π‘— ∈ 𝐼 βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—)))
219214, 218bitrdi 286 . 2 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ π‘₯ = (𝐼 Γ— {π‘Œ})) ↔ βˆ€π‘— ∈ 𝐼 βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ (π‘₯β€˜π‘—) = ((𝐼 Γ— {π‘Œ})β€˜π‘—))))
220204, 205, 2193bitr4d 310 1 ((π‘Š ∈ LMod ∧ 𝐼 ∈ 𝑋 ∧ 𝐹:𝐼⟢𝐡) β†’ (𝐹 LIndF π‘Š ↔ βˆ€π‘₯ ∈ 𝐿 ((π‘Š Ξ£g (π‘₯ ∘f Β· 𝐹)) = 0 β†’ π‘₯ = (𝐼 Γ— {π‘Œ}))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   βˆ‰ wnel 3046  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628  βŸ¨cop 4634   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  dom cdm 5676   β†Ύ cres 5678   β€œ cima 5679  Fun wfun 6537   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7408   ∘f cof 7667   ↑m cmap 8819   finSupp cfsupp 9360  Basecbs 17143  +gcplusg 17196  Scalarcsca 17199   ·𝑠 cvsca 17200  0gc0g 17384   Ξ£g cgsu 17385  Mndcmnd 18624  Grpcgrp 18818  invgcminusg 18819  CMndccmn 19647  LModclmod 20470  LSpanclspn 20581   freeLMod cfrlm 21300   LIndF clindf 21358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-of 7669  df-om 7855  df-1st 7974  df-2nd 7975  df-supp 8146  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-er 8702  df-map 8821  df-ixp 8891  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-sup 9436  df-oi 9504  df-card 9933  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-nn 12212  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12472  df-z 12558  df-dec 12677  df-uz 12822  df-fz 13484  df-fzo 13627  df-seq 13966  df-hash 14290  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-hom 17220  df-cco 17221  df-0g 17386  df-gsum 17387  df-prds 17392  df-pws 17394  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18560  df-sgrp 18609  df-mnd 18625  df-mhm 18670  df-submnd 18671  df-grp 18821  df-minusg 18822  df-sbg 18823  df-mulg 18950  df-subg 19002  df-ghm 19089  df-cntz 19180  df-cmn 19649  df-abl 19650  df-mgp 19987  df-ur 20004  df-ring 20057  df-nzr 20291  df-subrg 20316  df-lmod 20472  df-lss 20542  df-lsp 20582  df-lmhm 20632  df-lbs 20685  df-sra 20784  df-rgmod 20785  df-dsmm 21286  df-frlm 21301  df-uvc 21337  df-lindf 21360
This theorem is referenced by:  islindf5  21393  islinds5  32475  islbs5  32491  fedgmul  32711  matunitlindflem1  36479  aacllem  47838
  Copyright terms: Public domain W3C validator