lindslinindsimp2

Description: Implication 2 for lindslininds . (Contributed by AV, 26-Apr-2019) (Revised by AV, 30-Jul-2019)

	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	lindslinindsimp2	$⊢ (S \in V \land M \in LMod) \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\})) \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})))$

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		simprl	$⊢ ((S \in V \land M \in LMod) \land (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\}))) \to S \subseteq {Base}_{M}$
6		elpwg	$⊢ S \in V \to (S \in 𝒫 {Base}_{M} \leftrightarrow S \subseteq {Base}_{M})$
7	6	ad2antrr	$⊢ ((S \in V \land M \in LMod) \land (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\}))) \to (S \in 𝒫 {Base}_{M} \leftrightarrow S \subseteq {Base}_{M})$
8	5 7	mpbird	$⊢ ((S \in V \land M \in LMod) \land (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\}))) \to S \in 𝒫 {Base}_{M}$
9		simplr	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to M \in LMod$
10		ssdifss	$⊢ S \subseteq {Base}_{M} \to S ∖ \{s\} \subseteq {Base}_{M}$
11	10	adantl	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to S ∖ \{s\} \subseteq {Base}_{M}$
12		difexg	$⊢ S \in V \to S ∖ \{s\} \in V$
13	12	ad2antrr	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to S ∖ \{s\} \in V$
14		elpwg	$⊢ S ∖ \{s\} \in V \to (S ∖ \{s\} \in 𝒫 {Base}_{M} \leftrightarrow S ∖ \{s\} \subseteq {Base}_{M})$
15	13 14	syl	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (S ∖ \{s\} \in 𝒫 {Base}_{M} \leftrightarrow S ∖ \{s\} \subseteq {Base}_{M})$
16	11 15	mpbird	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to S ∖ \{s\} \in 𝒫 {Base}_{M}$
17		eqid	$⊢ {Base}_{M} = {Base}_{M}$
18	17	lspeqlco	$⊢ (M \in LMod \land S ∖ \{s\} \in 𝒫 {Base}_{M}) \to M LinCo (S ∖ \{s\}) = LSpan (M) (S ∖ \{s\})$
19	18	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\}))$
20	19	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\})))$
21	9 16 20	syl2anc	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (y \cdot_{M} s \in LSpan (M) (S ∖ \{s\}) \leftrightarrow y \cdot_{M} s \in (M LinCo (S ∖ \{s\})))$
22	21	notbid	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (\neg y \cdot_{M} s \in LSpan (M) (S ∖ \{s\}) \leftrightarrow \neg y \cdot_{M} s \in (M LinCo (S ∖ \{s\})))$
23	17 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\}))))$
24	3	eqcomi	$⊢ 0_{R} = \underset{˙}{0}$
25	24	breq2i	$⊢ {finSupp}_{0_{R}} (g) \leftrightarrow {finSupp}_{\underset{˙}{0}} (g)$
26	25	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\}))$
27	26	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\}))$
28	27	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\})))$
29	23 28	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\}))))$
30	9 16 29	syl2anc	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {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\}))))$
31	30	notbid	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (\neg y \cdot_{M} s \in (M LinCo (S ∖ \{s\})) \leftrightarrow \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\}))))$
32		ianor	$⊢ \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\}))) \leftrightarrow (\neg y \cdot_{M} s \in {Base}_{M} \lor \neg \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
33		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\}))$
34		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\}))$
35	34	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\}))$
36	33 35	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\}))$
37	36	orbi2i	$⊢ (\neg y \cdot_{M} s \in {Base}_{M} \lor \neg \exists g \in (B^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (g) \land y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \leftrightarrow (\neg y \cdot_{M} s \in {Base}_{M} \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
38	32 37	bitri	$⊢ \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\}))) \leftrightarrow (\neg y \cdot_{M} s \in {Base}_{M} \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
39	31 38	bitrdi	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (\neg y \cdot_{M} s \in (M LinCo (S ∖ \{s\})) \leftrightarrow (\neg y \cdot_{M} s \in {Base}_{M} \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
40	22 39	bitrd	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (\neg y \cdot_{M} s \in LSpan (M) (S ∖ \{s\}) \leftrightarrow (\neg y \cdot_{M} s \in {Base}_{M} \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
41	40	2ralbidv	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (\forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \neg y \cdot_{M} s \in LSpan (M) (S ∖ \{s\}) \leftrightarrow \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) (\neg y \cdot_{M} s \in {Base}_{M} \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
42		simpllr	$⊢ (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to M \in LMod$
43		eldifi	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \to y \in B$
44	43	adantl	$⊢ (s \in S \land y \in (B ∖ \{\underset{˙}{0}\})) \to y \in B$
45	44	adantl	$⊢ (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to y \in B$
46		ssel2	$⊢ (S \subseteq {Base}_{M} \land s \in S) \to s \in {Base}_{M}$
47	46	ad2ant2lr	$⊢ (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to s \in {Base}_{M}$
48		eqid	$⊢ \cdot_{M} = \cdot_{M}$
49	17 1 48 2	lmodvscl	$⊢ (M \in LMod \land y \in B \land s \in {Base}_{M}) \to y \cdot_{M} s \in {Base}_{M}$
50	42 45 47 49	syl3anc	$⊢ (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to y \cdot_{M} s \in {Base}_{M}$
51	50	notnotd	$⊢ (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to \neg \neg y \cdot_{M} s \in {Base}_{M}$
52		nbfal	$⊢ \neg \neg y \cdot_{M} s \in {Base}_{M} \leftrightarrow (\neg y \cdot_{M} s \in {Base}_{M} \leftrightarrow ⊥)$
53	51 52	sylib	$⊢ (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to (\neg y \cdot_{M} s \in {Base}_{M} \leftrightarrow ⊥)$
54	53	orbi1d	$⊢ (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land (s \in S \land y \in (B ∖ \{\underset{˙}{0}\}))) \to ((\neg y \cdot_{M} s \in {Base}_{M} \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \leftrightarrow (⊥ \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
55	54	2ralbidva	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (\forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) (\neg y \cdot_{M} s \in {Base}_{M} \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \leftrightarrow \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) (⊥ \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))))$
56		r19.32v	$⊢ \forall y \in (B ∖ \{\underset{˙}{0}\}) (⊥ \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \leftrightarrow (⊥ \lor \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
57	56	ralbii	$⊢ \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) (⊥ \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \leftrightarrow \forall s \in S (⊥ \lor \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
58		r19.32v	$⊢ \forall s \in S (⊥ \lor \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \leftrightarrow (⊥ \lor \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
59	57 58	bitri	$⊢ \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) (⊥ \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \leftrightarrow (⊥ \lor \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})))$
60		falim	$⊢ ⊥ \to (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \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}))$
61		sneq	$⊢ s = x \to \{s\} = \{x\}$
62	61	difeq2d	$⊢ s = x \to S ∖ \{s\} = S ∖ \{x\}$
63	62	oveq2d	$⊢ s = x \to B^{(S ∖ \{s\})} = B^{(S ∖ \{x\})}$
64		oveq2	$⊢ s = x \to y \cdot_{M} s = y \cdot_{M} x$
65	62	oveq2d	$⊢ s = x \to g linC (M) (S ∖ \{s\}) = g linC (M) (S ∖ \{x\})$
66	64 65	eqeq12d	$⊢ s = x \to (y \cdot_{M} s = g linC (M) (S ∖ \{s\}) \leftrightarrow y \cdot_{M} x = g linC (M) (S ∖ \{x\}))$
67	66	notbid	$⊢ s = x \to (\neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}) \leftrightarrow \neg y \cdot_{M} x = g linC (M) (S ∖ \{x\}))$
68	67	orbi2d	$⊢ s = x \to ((\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \leftrightarrow (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} x = g linC (M) (S ∖ \{x\})))$
69	63 68	raleqbidv	$⊢ s = x \to (\forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \leftrightarrow \forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} x = g linC (M) (S ∖ \{x\})))$
70	69	ralbidv	$⊢ s = x \to (\forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \leftrightarrow \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} x = g linC (M) (S ∖ \{x\})))$
71	70	rspcva	$⊢ (x \in S \land \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \to \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} x = g linC (M) (S ∖ \{x\}))$
72	1 2 3 4	lindslinindsimp2lem5	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to ((f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to (\forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} x = g linC (M) (S ∖ \{x\})) \to f (x) = \underset{˙}{0}))$
73	72	expr	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (x \in S \to ((f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to (\forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} x = g linC (M) (S ∖ \{x\})) \to f (x) = \underset{˙}{0})))$
74	73	com14	$⊢ \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} x = g linC (M) (S ∖ \{x\})) \to (x \in S \to ((f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to f (x) = \underset{˙}{0})))$
75	71 74	syl	$⊢ (x \in S \land \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \to (x \in S \to ((f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to f (x) = \underset{˙}{0})))$
76	75	ex	$⊢ x \in S \to (\forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \to (x \in S \to ((f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to f (x) = \underset{˙}{0}))))$
77	76	pm2.43a	$⊢ x \in S \to (\forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \to ((f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to f (x) = \underset{˙}{0})))$
78	77	com14	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (\forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \to ((f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to (x \in S \to f (x) = \underset{˙}{0})))$
79	78	imp	$⊢ (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \to ((f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to (x \in S \to f (x) = \underset{˙}{0}))$
80	79	expdimp	$⊢ ((((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \land f \in (B^{S})) \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to (x \in S \to f (x) = \underset{˙}{0}))$
81	80	ralrimdv	$⊢ ((((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \land f \in (B^{S})) \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})$
82	81	ralrimiva	$⊢ (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \land \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg 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})$
83	82	expcom	$⊢ \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\})) \to (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \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}))$
84	60 83	jaoi	$⊢ (⊥ \lor \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} s = g linC (M) (S ∖ \{s\}))) \to (((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \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}))$
85	84	com12	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to ((⊥ \lor \forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg 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}))$
86	59 85	syl5bi	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (\forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) (⊥ \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg 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}))$
87	55 86	sylbid	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (\forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) (\neg y \cdot_{M} s \in {Base}_{M} \lor \forall g \in (B^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg 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}))$
88	41 87	sylbid	$⊢ ((S \in V \land M \in LMod) \land S \subseteq {Base}_{M}) \to (\forall s \in S \forall y \in (B ∖ \{\underset{˙}{0}\}) \neg y \cdot_{M} s \in LSpan (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}))$
89	88	impr	$⊢ ((S \in V \land M \in LMod) \land (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\}))) \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})$
90	8 89	jca	$⊢ ((S \in V \land M \in LMod) \land (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\}))) \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}))$
91	90	ex	$⊢ (S \in V \land M \in LMod) \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\})) \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})))$

Metamath Proof Explorer

Theorem lindslinindsimp2

Proof