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		incom	$⊢ (I ∖ \{j\}) \cap \{j\} = \{j\} \cap (I ∖ \{j\})$
69		disjdif	$⊢ \{j\} \cap (I ∖ \{j\}) = \emptyset$
70	68 69	eqtri	$⊢ (I ∖ \{j\}) \cap \{j\} = \emptyset$
71	70	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$
72		difsnid	$⊢ j \in I \to (I ∖ \{j\}) \cup \{j\} = I$
73	72	eqcomd	$⊢ j \in I \to I = (I ∖ \{j\}) \cup \{j\}$
74	42 73	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\}$
75	1 4 39 24 25 45 67 71 74	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\}}))$
76		vex	$⊢ y \in V$
77		snex	$⊢ \{⟨j, l⟩\} \in V$
78	76 77	unex	$⊢ y \cup \{⟨j, l⟩\} \in V$
79		simpl3	$⊢ ((W \in LMod \land I \in X \land F : I ⟶ B) \land j \in I) \to F : I ⟶ B$
80		simpl2	$⊢ ((W \in LMod \land I \in X \land F : I ⟶ B) \land j \in I) \to I \in X$
81		fex	$⊢ (F : I ⟶ B \land I \in X) \to F \in V$
82	79 80 81	syl2anc	$⊢ ((W \in LMod \land I \in X \land F : I ⟶ B) \land j \in I) \to F \in V$
83	82	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$
84		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\})})$
85	78 83 84	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\})})$
86	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\})$
87		neldifsn	$⊢ \neg j \in (I ∖ \{j\})$
88		fsnunres	$⊢ (y Fn (I ∖ \{j\}) \land \neg j \in (I ∖ \{j\})) \to {(y \cup \{⟨j, l⟩\}) ↾}_{(I ∖ \{j\})} = y$
89	86 87 88	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$
90	89	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\})})$
91	85 90	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\})})$
92	91	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\})}))$
93	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$
94		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)⟩\}$
95	93 42 94	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)⟩\}$
96	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$
97	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$
98		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)$
99	96 97 25 42 98	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)$
100		fndm	$⊢ y Fn (I ∖ \{j\}) \to dom y = I ∖ \{j\}$
101	100	eleq2d	$⊢ y Fn (I ∖ \{j\}) \to (j \in dom y \leftrightarrow j \in (I ∖ \{j\}))$
102	87 101	mtbiri	$⊢ y Fn (I ∖ \{j\}) \to \neg j \in dom y$
103		vex	$⊢ j \in V$
104		vex	$⊢ l \in V$
105		fsnunfv	$⊢ (j \in V \land l \in V \land \neg j \in dom y) \to (y \cup \{⟨j, l⟩\}) (j) = l$
106	103 104 105	mp3an12	$⊢ \neg j \in dom y \to (y \cup \{⟨j, l⟩\}) (j) = l$
107	86 102 106	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$
108	107	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)$
109	99 108	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)$
110	109	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)⟩$
111	110	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)⟩\}$
112		ovex	$⊢ l \underset{˙}{\cdot} F (j) \in V$
113		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))$
114	103 112 113	mp2an	$⊢ \{⟨j, l \underset{˙}{\cdot} F (j)⟩\} = (x \in \{j\} ⟼ l \underset{˙}{\cdot} F (j))$
115	114	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))$
116	95 111 115	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))$
117	116	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))$
118		cmnmnd	$⊢ W \in CMnd \to W \in Mnd$
119	8 23 118	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$
120	103	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$
121		eqidd	$⊢ x = j \to l \underset{˙}{\cdot} F (j) = l \underset{˙}{\cdot} F (j)$
122	1 121	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)$
123	119 120 22 122	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)$
124	117 123	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)$
125	92 124	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))$
126	75 125	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)$
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 ((\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})$
128	18 41 127	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})$
129	107	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)$
130	129	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)$
131	128 130	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))$
132	131	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))$
133	132	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)))$
134		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))$
135	134	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)))$
136	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))$
137	136	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)))$
138	133 135 137	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)))$
139	138	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)))$
140		breq1	$⊢ x = y \cup \{⟨j, l⟩\} \to ({finSupp}_{Y} (x) \leftrightarrow {finSupp}_{Y} ((y \cup \{⟨j, l⟩\})))$
141		oveq1	$⊢ x = y \cup \{⟨j, l⟩\} \to x {\underset{˙}{\cdot}}_{f} F = (y \cup \{⟨j, l⟩\}) {\underset{˙}{\cdot}}_{f} F$
142	141	oveq2d	$⊢ x = y \cup \{⟨j, l⟩\} \to \sum_{W} (x {\underset{˙}{\cdot}}_{f} F) = \sum_{W} ((y \cup \{⟨j, l⟩\}) {\underset{˙}{\cdot}}_{f} F)$
143	142	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})$
144		fveq1	$⊢ x = y \cup \{⟨j, l⟩\} \to x (j) = (y \cup \{⟨j, l⟩\}) (j)$
145	144	eqeq1d	$⊢ x = y \cup \{⟨j, l⟩\} \to (x (j) = Y \leftrightarrow (y \cup \{⟨j, l⟩\}) (j) = Y)$
146	143 145	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))$
147	140 146	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)))$
148	147	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)))$
149	148	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)))$
150	139 149	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)))$
151		breq1	$⊢ z = x \to ({finSupp}_{Y} (z) \leftrightarrow {finSupp}_{Y} (x))$
152	151	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))$
153	150 152	syl6bbr	$⊢ ((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))$
154		resima	$⊢ ({F ↾}_{(I ∖ \{j\})}) [I ∖ \{j\}] = F [I ∖ \{j\}]$
155	154	eqcomi	$⊢ F [I ∖ \{j\}] = ({F ↾}_{(I ∖ \{j\})}) [I ∖ \{j\}]$
156	155	fveq2i	$⊢ LSpan (W) (F [I ∖ \{j\}]) = LSpan (W) (({F ↾}_{(I ∖ \{j\})}) [I ∖ \{j\}])$
157	156	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\}])$
158		eqid	$⊢ LSpan (W) = LSpan (W)$
159	79 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$
160		simpl1	$⊢ ((W \in LMod \land I \in X \land F : I ⟶ B) \land j \in I) \to W \in LMod$
161	26	3ad2ant2	$⊢ (W \in LMod \land I \in X \land F : I ⟶ B) \to I ∖ \{j\} \in V$
162	161	adantr	$⊢ ((W \in LMod \land I \in X \land F : I ⟶ B) \land j \in I) \to I ∖ \{j\} \in V$
163	158 1 15 2 5 3 159 160 162	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\})}))))$
164	157 163	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\})}))))$
165	164	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))$
166		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)$
167	165 166	syl6bbr	$⊢ ((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))$
168	167	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))$
169	2	fvexi	$⊢ R \in V$
170		eqid	$⊢ R freeLMod I = R freeLMod I$
171		eqid	$⊢ \{z \in ({Base}_{R}^{I}) \| {finSupp}_{Y} (z)\} = \{z \in ({Base}_{R}^{I}) \| {finSupp}_{Y} (z)\}$
172	170 15 5 171	frlmbas	$⊢ (R \in V \land I \in X) \to \{z \in ({Base}_{R}^{I}) \| {finSupp}_{Y} (z)\} = {Base}_{(R freeLMod I)}$
173	169 172	mpan	$⊢ I \in X \to \{z \in ({Base}_{R}^{I}) \| {finSupp}_{Y} (z)\} = {Base}_{(R freeLMod I)}$
174	173	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)}$
175	174	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)}$
176	6 175	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)\}$
177	176	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))$
178	153 168 177	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))$
179	7 178	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))$
180	2	lmodfgrp	$⊢ W \in LMod \to R \in Grp$
181	15 5 14	grpinvnzcl	$⊢ (R \in Grp \land l \in ({Base}_{R} ∖ \{Y\})) \to {inv}_{g} (R) (l) \in ({Base}_{R} ∖ \{Y\})$
182	180 181	sylan	$⊢ (W \in LMod \land l \in ({Base}_{R} ∖ \{Y\})) \to {inv}_{g} (R) (l) \in ({Base}_{R} ∖ \{Y\})$
183	15 5 14	grpinvnzcl	$⊢ (R \in Grp \land k \in ({Base}_{R} ∖ \{Y\})) \to {inv}_{g} (R) (k) \in ({Base}_{R} ∖ \{Y\})$
184	180 183	sylan	$⊢ (W \in LMod \land k \in ({Base}_{R} ∖ \{Y\})) \to {inv}_{g} (R) (k) \in ({Base}_{R} ∖ \{Y\})$
185		eldifi	$⊢ k \in ({Base}_{R} ∖ \{Y\}) \to k \in {Base}_{R}$
186	15 14	grpinvinv	$⊢ (R \in Grp \land k \in {Base}_{R}) \to {inv}_{g} (R) ({inv}_{g} (R) (k)) = k$
187	180 185 186	syl2an	$⊢ (W \in LMod \land k \in ({Base}_{R} ∖ \{Y\})) \to {inv}_{g} (R) ({inv}_{g} (R) (k)) = k$
188	187	eqcomd	$⊢ (W \in LMod \land k \in ({Base}_{R} ∖ \{Y\})) \to k = {inv}_{g} (R) ({inv}_{g} (R) (k))$
189		fveq2	$⊢ l = {inv}_{g} (R) (k) \to {inv}_{g} (R) (l) = {inv}_{g} (R) ({inv}_{g} (R) (k))$
190	189	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)$
191	184 188 190	syl2anc	$⊢ (W \in LMod \land k \in ({Base}_{R} ∖ \{Y\})) \to \exists l \in ({Base}_{R} ∖ \{Y\}) k = {inv}_{g} (R) (l)$
192		oveq1	$⊢ k = {inv}_{g} (R) (l) \to k \underset{˙}{\cdot} F (j) = {inv}_{g} (R) (l) \underset{˙}{\cdot} F (j)$
193	192	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\}]))$
194	193	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\}]))$
195	194	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\}]))$
196	182 191 195	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\}]))$
197	196	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\}]))$
198	197	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\}]))$
199		simplr	$⊢ (((W \in LMod \land I \in X \land F : I ⟶ B) \land j \in I) \land x \in L) \to j \in I$
200	5	fvexi	$⊢ Y \in V$
201	200	fvconst2	$⊢ j \in I \to (I \times \{Y\}) (j) = Y$
202	199 201	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$
203	202	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)$
204	203	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))$
205	204	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))$
206	179 198 205	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)))$
207	206	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)))$
208	1 3 158 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\}]))$
209	170 15 6	frlmbasf	$⊢ (I \in X \land x \in L) \to x : I ⟶ {Base}_{R}$
210	209	3ad2antl2	$⊢ ((W \in LMod \land I \in X \land F : I ⟶ B) \land x \in L) \to x : I ⟶ {Base}_{R}$
211	210	ffnd	$⊢ ((W \in LMod \land I \in X \land F : I ⟶ B) \land x \in L) \to x Fn I$
212		fnconstg	$⊢ Y \in V \to (I \times \{Y\}) Fn I$
213	200 212	ax-mp	$⊢ (I \times \{Y\}) Fn I$
214		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))$
215	211 213 214	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))$
216	215	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)))$
217	216	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)))$
218		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))$
219	218	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))$
220		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))$
221	219 220	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))$
222	217 221	syl6bb	$⊢ (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)))$
223	207 208 222	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