lindslinindsimp1

Description: Implication 1 for lindslininds . (Contributed by AV, 25-Apr-2019) (Revised by AV, 30-Jul-2019) (Proof shortened by II, 16-Feb-2023)

	Ref	Expression
Hypotheses	lindslinind.r	$⊢ R = Scalar (M)$
	lindslinind.b	$⊢ B = {Base}_{R}$
	lindslinind.0	$⊢ \underset{˙}{0} = 0_{R}$
	lindslinind.z	$⊢ Z = 0_{M}$
Assertion	lindslinindsimp1	$⊢ (S \in V \land M \in LMod) \to ((S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})) \to (S \subseteq {Base}_{M} \land \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \neg y \cdot_{M} s \in LSpan (M) (S ∖ \{s\})))$

Proof

Step	Hyp	Ref	Expression
1		lindslinind.r	$⊢ R = Scalar (M)$
2		lindslinind.b	$⊢ B = {Base}_{R}$
3		lindslinind.0	$⊢ \underset{˙}{0} = 0_{R}$
4		lindslinind.z	$⊢ Z = 0_{M}$
5		elpwi	$⊢ S \in 𝒫 {Base}_{M} \to S \subseteq {Base}_{M}$
6	5	ad2antrl	$⊢ ((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \to S \subseteq {Base}_{M}$
7		simpr	$⊢ (S \in V \land M \in LMod) \to M \in LMod$
8	7	anim2i	$⊢ (S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \to (S \in 𝒫 {Base}_{M} \land M \in LMod)$
9	8	ancomd	$⊢ (S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \to (M \in LMod \land S \in 𝒫 {Base}_{M})$
10	9	ad2antrr	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (M \in LMod \land S \in 𝒫 {Base}_{M})$
11		eldifi	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \to y \in B$
12	11	adantl	$⊢ (s \in S \land y \in (B ∖ \{\underset{˙}{0}\})) \to y \in B$
13	12	adantl	$⊢ ((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to y \in B$
14	13	adantr	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to y \in B$
15		simprl	$⊢ ((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to s \in S$
16	15	adantr	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to s \in S$
17		simprl	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to g \in (B^{(S ∖ \{s\})})$
18	14 16 17	3jca	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (y \in B \land s \in S \land g \in (B^{(S ∖ \{s\})}))$
19		simprrl	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to {finSupp}_{\underset{˙}{0}} (g)$
20		eqid	$⊢ {Base}_{M} = {Base}_{M}$
21		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
22		eqid	$⊢ (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z)))$
23	20 1 2 3 4 21 22	lincext2	$⊢ ((M \in LMod \land S \in 𝒫 {Base}_{M}) \land (y \in B \land s \in S \land g \in (B^{(S ∖ \{s\})})) \land {finSupp}_{\underset{˙}{0}} (g)) \to {finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))))$
24	10 18 19 23	syl3anc	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to {finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))))$
25	8	adantr	$⊢ ((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to (S \in 𝒫 {Base}_{M} \land M \in LMod)$
26	25	ancomd	$⊢ ((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to (M \in LMod \land S \in 𝒫 {Base}_{M})$
27	26	adantr	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (M \in LMod \land S \in 𝒫 {Base}_{M})$
28	20 1 2 3 4 21 22	lincext1	$⊢ ((M \in LMod \land S \in 𝒫 {Base}_{M}) \land (y \in B \land s \in S \land g \in (B^{(S ∖ \{s\})}))) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \in (B^{S})$
29	27 18 28	syl2anc	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \in (B^{S})$
30		breq1	$⊢ f = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \to ({finSupp}_{\underset{˙}{0}} (f) \leftrightarrow {finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z)))))$
31		oveq1	$⊢ f = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \to f linC (M) S = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S$
32	31	eqeq1d	$⊢ f = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \to (f linC (M) S = Z \leftrightarrow (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S = Z)$
33	30 32	anbi12d	$⊢ f = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \leftrightarrow ({finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z)))) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S = Z))$
34		fveq1	$⊢ f = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \to f (x) = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x)$
35	34	eqeq1d	$⊢ f = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \to (f (x) = \underset{˙}{0} \leftrightarrow (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0})$
36	35	ralbidv	$⊢ f = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \to (\forall x \in S f (x) = \underset{˙}{0} \leftrightarrow \forall x \in S (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0})$
37	33 36	imbi12d	$⊢ f = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \to ((({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow (({finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z)))) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S = Z) \to \forall x \in S (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0}))$
38	37	rspcv	$⊢ (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) \in (B^{S}) \to (\forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to (({finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z)))) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S = Z) \to \forall x \in S (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0}))$
39	29 38	syl	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (\forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to (({finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z)))) \land (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S = Z) \to \forall x \in S (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0}))$
40	39	exp4a	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (\forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to ({finSupp}_{\underset{˙}{0}} ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z)))) \to ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S = Z \to \forall x \in S (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0})))$
41	24 40	mpid	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (\forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S = Z \to \forall x \in S (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0}))$
42		simprr	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
43	20 1 2 3 4 21 22	lincext3	$⊢ ((M \in LMod \land S \in 𝒫 {Base}_{M}) \land (y \in B \land s \in S \land g \in (B^{(S ∖ \{s\})})) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S = Z$
44	10 18 42 43	syl3anc	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S = Z$
45		fveqeq2	$⊢ x = s \to ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0} \leftrightarrow (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (s) = \underset{˙}{0})$
46	45	rspcv	$⊢ s \in S \to (\forall x \in S (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0} \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (s) = \underset{˙}{0})$
47	16 46	syl	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (\forall x \in S (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0} \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (s) = \underset{˙}{0})$
48		eqidd	$⊢ ((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) = (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z)))$
49		iftrue	$⊢ z = s \to if (z = s, {inv}_{g} (R) (y), g (z)) = {inv}_{g} (R) (y)$
50	49	adantl	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land z = s) \to if (z = s, {inv}_{g} (R) (y), g (z)) = {inv}_{g} (R) (y)$
51		fvexd	$⊢ ((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to {inv}_{g} (R) (y) \in V$
52	48 50 15 51	fvmptd	$⊢ ((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (s) = {inv}_{g} (R) (y)$
53	52	adantr	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (s) = {inv}_{g} (R) (y)$
54	53	eqeq1d	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (s) = \underset{˙}{0} \leftrightarrow {inv}_{g} (R) (y) = \underset{˙}{0})$
55	1	lmodfgrp	$⊢ M \in LMod \to R \in Grp$
56	2 3 21	grpinvnzcl	$⊢ (R \in Grp \land y \in (B ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (R) (y) \in (B ∖ \{\underset{˙}{0}\})$
57		eldif	$⊢ {inv}_{g} (R) (y) \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow ({inv}_{g} (R) (y) \in B \land \neg {inv}_{g} (R) (y) \in \{\underset{˙}{0}\})$
58		fvex	$⊢ {inv}_{g} (R) (y) \in V$
59	58	elsn	$⊢ {inv}_{g} (R) (y) \in \{\underset{˙}{0}\} \leftrightarrow {inv}_{g} (R) (y) = \underset{˙}{0}$
60		pm2.21	$⊢ \neg {inv}_{g} (R) (y) = \underset{˙}{0} \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to (S \in V \to (s \in S \to (S \in 𝒫 {Base}_{M} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))))$
61	60	com25	$⊢ \neg {inv}_{g} (R) (y) = \underset{˙}{0} \to (S \in 𝒫 {Base}_{M} \to (S \in V \to (s \in S \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))))$
62	59 61	sylnbi	$⊢ \neg {inv}_{g} (R) (y) \in \{\underset{˙}{0}\} \to (S \in 𝒫 {Base}_{M} \to (S \in V \to (s \in S \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))))$
63	57 62	simplbiim	$⊢ {inv}_{g} (R) (y) \in (B ∖ \{\underset{˙}{0}\}) \to (S \in 𝒫 {Base}_{M} \to (S \in V \to (s \in S \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))))$
64	56 63	syl	$⊢ (R \in Grp \land y \in (B ∖ \{\underset{˙}{0}\})) \to (S \in 𝒫 {Base}_{M} \to (S \in V \to (s \in S \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))))$
65	64	ex	$⊢ R \in Grp \to (y \in (B ∖ \{\underset{˙}{0}\}) \to (S \in 𝒫 {Base}_{M} \to (S \in V \to (s \in S \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))))$
66	55 65	syl	$⊢ M \in LMod \to (y \in (B ∖ \{\underset{˙}{0}\}) \to (S \in 𝒫 {Base}_{M} \to (S \in V \to (s \in S \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))))$
67	66	com24	$⊢ M \in LMod \to (S \in V \to (S \in 𝒫 {Base}_{M} \to (y \in (B ∖ \{\underset{˙}{0}\}) \to (s \in S \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))))$
68	67	impcom	$⊢ (S \in V \land M \in LMod) \to (S \in 𝒫 {Base}_{M} \to (y \in (B ∖ \{\underset{˙}{0}\}) \to (s \in S \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))))$
69	68	impcom	$⊢ (S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \to (y \in (B ∖ \{\underset{˙}{0}\}) \to (s \in S \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
70	69	com13	$⊢ s \in S \to (y \in (B ∖ \{\underset{˙}{0}\}) \to ((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
71	70	imp	$⊢ (s \in S \land y \in (B ∖ \{\underset{˙}{0}\})) \to ((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
72	71	impcom	$⊢ ((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
73	72	adantr	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to ({inv}_{g} (R) (y) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
74	54 73	sylbid	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to ((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (s) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
75	47 74	syld	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (\forall x \in S (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0} \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
76	44 75	embantd	$⊢ (((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to (((z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) linC (M) S = Z \to \forall x \in S (z \in S ⟼ if (z = s, {inv}_{g} (R) (y), g (z))) (x) = \underset{˙}{0}) \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
77	41 76	syldc	$⊢ \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to ((((S \in 𝒫 {Base}_{M} \land (S \in V \land M \in LMod)) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land (g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))) \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
78	77	exp5j	$⊢ \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to (S \in 𝒫 {Base}_{M} \to ((S \in V \land M \in LMod) \to ((s \in S \land y \in (B ∖ \{\underset{˙}{0}\})) \to ((g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))))$
79	78	impcom	$⊢ (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})) \to ((S \in V \land M \in LMod) \to ((s \in S \land y \in (B ∖ \{\underset{˙}{0}\})) \to ((g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
80	79	impcom	$⊢ ((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \to ((s \in S \land y \in (B ∖ \{\underset{˙}{0}\})) \to ((g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
81	80	imp	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to ((g \in (B^{(S ∖ \{s\})}) \land ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
82	81	expdimp	$⊢ ((((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land g \in (B^{(S ∖ \{s\})})) \to (({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
83	82	expd	$⊢ ((((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land g \in (B^{(S ∖ \{s\})})) \to ({finSupp}_{\underset{˙}{0}} (g) \to (y \cdot_{M} s = g linC (M) (S ∖ \{s\}) \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
84	83	impcom	$⊢ ({finSupp}_{\underset{˙}{0}} (g) \land ((((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land g \in (B^{(S ∖ \{s\})}))) \to (y \cdot_{M} s = g linC (M) (S ∖ \{s\}) \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
85	84	pm2.01d	$⊢ ({finSupp}_{\underset{˙}{0}} (g) \land ((((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land g \in (B^{(S ∖ \{s\})}))) \to \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})$
86	85	olcd	$⊢ ({finSupp}_{\underset{˙}{0}} (g) \land ((((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land g \in (B^{(S ∖ \{s\})}))) \to (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
87		animorl	$⊢ (\neg {finSupp}_{\underset{˙}{0}} (g) \land ((((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land g \in (B^{(S ∖ \{s\})}))) \to (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
88	86 87	pm2.61ian	$⊢ ((((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \land g \in (B^{(S ∖ \{s\})})) \to (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
89	88	ralrimiva	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
90		ralnex	$⊢ \forall g \in (B^{(S ∖ \{s\})}) \neg ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \leftrightarrow \neg \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
91		ianor	$⊢ \neg ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \leftrightarrow (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
92	91	ralbii	$⊢ \forall g \in (B^{(S ∖ \{s\})}) \neg ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \leftrightarrow \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
93	90 92	bitr3i	$⊢ \neg \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \leftrightarrow \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
94	89 93	sylibr	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to \neg \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
95	94	intnand	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to \neg (y \cdot_{M} s \in {Base}_{M} \land \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
96	7	ad2antrr	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to M \in LMod$
97		difexg	$⊢ S \in V \to S ∖ \{s\} \in V$
98	97	ad2antrr	$⊢ ((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \to S ∖ \{s\} \in V$
99	5	ssdifssd	$⊢ S \in 𝒫 {Base}_{M} \to S ∖ \{s\} \subseteq {Base}_{M}$
100	99	ad2antrl	$⊢ ((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \to S ∖ \{s\} \subseteq {Base}_{M}$
101	98 100	elpwd	$⊢ ((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \to S ∖ \{s\} \in 𝒫 {Base}_{M}$
102	101	adantr	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to S ∖ \{s\} \in 𝒫 {Base}_{M}$
103	20	lspeqlco	$⊢ (M \in LMod \land S ∖ \{s\} \in 𝒫 {Base}_{M}) \to M LinCo (S ∖ \{s\}) = LSpan (M) (S ∖ \{s\})$
104	103	eleq2d	$⊢ (M \in LMod \land S ∖ \{s\} \in 𝒫 {Base}_{M}) \to (y \cdot_{M} s \in (M LinCo (S ∖ \{s\})) \leftrightarrow y \cdot_{M} s \in LSpan (M) (S ∖ \{s\}))$
105	104	bicomd	$⊢ (M \in LMod \land S ∖ \{s\} \in 𝒫 {Base}_{M}) \to (y \cdot_{M} s \in LSpan (M) (S ∖ \{s\}) \leftrightarrow y \cdot_{M} s \in (M LinCo (S ∖ \{s\})))$
106	96 102 105	syl2anc	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to (y \cdot_{M} s \in LSpan (M) (S ∖ \{s\}) \leftrightarrow y \cdot_{M} s \in (M LinCo (S ∖ \{s\})))$
107	7	adantr	$⊢ ((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \to M \in LMod$
108		difexg	$⊢ S \in 𝒫 {Base}_{M} \to S ∖ \{s\} \in V$
109	108 99	elpwd	$⊢ S \in 𝒫 {Base}_{M} \to S ∖ \{s\} \in 𝒫 {Base}_{M}$
110	109	ad2antrl	$⊢ ((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \to S ∖ \{s\} \in 𝒫 {Base}_{M}$
111	107 110	jca	$⊢ ((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \to (M \in LMod \land S ∖ \{s\} \in 𝒫 {Base}_{M})$
112	111	adantr	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to (M \in LMod \land S ∖ \{s\} \in 𝒫 {Base}_{M})$
113	20 1 2	lcoval	$⊢ (M \in LMod \land S ∖ \{s\} \in 𝒫 {Base}_{M}) \to (y \cdot_{M} s \in (M LinCo (S ∖ \{s\})) \leftrightarrow (y \cdot_{M} s \in {Base}_{M} \land \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{0_{R}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
114	3	eqcomi	$⊢ 0_{R} = \underset{˙}{0}$
115	114	breq2i	$⊢ {finSupp}_{0_{R}} (g) \leftrightarrow {finSupp}_{\underset{˙}{0}} (g)$
116	115	anbi1i	$⊢ ({finSupp}_{0_{R}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
117	116	rexbii	$⊢ \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{0_{R}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \leftrightarrow \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))$
118	117	anbi2i	$⊢ (y \cdot_{M} s \in {Base}_{M} \land \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{0_{R}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \leftrightarrow (y \cdot_{M} s \in {Base}_{M} \land \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
119	113 118	bitrdi	$⊢ (M \in LMod \land S ∖ \{s\} \in 𝒫 {Base}_{M}) \to (y \cdot_{M} s \in (M LinCo (S ∖ \{s\})) \leftrightarrow (y \cdot_{M} s \in {Base}_{M} \land \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
120	112 119	syl	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to (y \cdot_{M} s \in (M LinCo (S ∖ \{s\})) \leftrightarrow (y \cdot_{M} s \in {Base}_{M} \land \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
121	106 120	bitrd	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to (y \cdot_{M} s \in LSpan (M) (S ∖ \{s\}) \leftrightarrow (y \cdot_{M} s \in {Base}_{M} \land \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
122	95 121	mtbird	$⊢ (((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to \neg y \cdot_{M} s \in LSpan (M) (S ∖ \{s\})$
123	122	ralrimivva	$⊢ ((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \to \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \neg y \cdot_{M} s \in LSpan (M) (S ∖ \{s\})$
124	6 123	jca	$⊢ ((S \in V \land M \in LMod) \land (S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}))) \to (S \subseteq {Base}_{M} \land \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \neg y \cdot_{M} s \in LSpan (M) (S ∖ \{s\}))$
125	124	ex	$⊢ (S \in V \land M \in LMod) \to ((S \in 𝒫 {Base}_{M} \land \forall f \in (B^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})) \to (S \subseteq {Base}_{M} \land \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \neg y \cdot_{M} s \in LSpan (M) (S ∖ \{s\})))$

Metamath Proof Explorer

Theorem lindslinindsimp1

Proof