islindf4

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

	Ref	Expression
Hypotheses	islindf4.b	$⊢ B = {Base}_{W}$
	islindf4.r	$⊢ R = Scalar (W)$
	islindf4.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	islindf4.z	$⊢ \underset{˙}{0} = 0_{W}$
	islindf4.y	$⊢ Y = 0_{R}$
	islindf4.l	$⊢ L = {Base}_{(R freeLMod I)}$
Assertion	islindf4	$⊢ (W \in LMod \land I \in X \land F : I ⟶ B) \to (F LIndF W \leftrightarrow \forall x \in L (\sum_{W} (x {\underset{˙}{\cdot}}_{f} F) = \underset{˙}{0} \to x = I \times \{Y\}))$

Proof

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

Metamath Proof Explorer

Theorem islindf4

Proof