lindslinindsimp2lem5

Description: Lemma 5 for lindslinindsimp2 . (Contributed by AV, 25-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	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}))$

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		ax-1	$⊢ f (x) = \underset{˙}{0} \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})$
6	5	2a1d	$⊢ f (x) = \underset{˙}{0} \to (((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})))$
7		elmapi	$⊢ f \in (B^{S}) \to f : S ⟶ B$
8		ffvelrn	$⊢ (f : S ⟶ B \land x \in S) \to f (x) \in B$
9	8	expcom	$⊢ x \in S \to (f : S ⟶ B \to f (x) \in B)$
10	9	adantl	$⊢ (S \subseteq {Base}_{M} \land x \in S) \to (f : S ⟶ B \to f (x) \in B)$
11	10	adantl	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to (f : S ⟶ B \to f (x) \in B)$
12	11	com12	$⊢ f : S ⟶ B \to (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to f (x) \in B)$
13	7 12	syl	$⊢ f \in (B^{S}) \to (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to f (x) \in B)$
14	13	adantr	$⊢ (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} \land x \in S)) \to f (x) \in B)$
15	14	impcom	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to f (x) \in B$
16	15	biantrurd	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (f (x) \neq \underset{˙}{0} \leftrightarrow (f (x) \in B \land f (x) \neq \underset{˙}{0}))$
17		df-ne	$⊢ f (x) \neq \underset{˙}{0} \leftrightarrow \neg f (x) = \underset{˙}{0}$
18	17	bicomi	$⊢ \neg f (x) = \underset{˙}{0} \leftrightarrow f (x) \neq \underset{˙}{0}$
19		eldifsn	$⊢ f (x) \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (f (x) \in B \land f (x) \neq \underset{˙}{0})$
20	16 18 19	3bitr4g	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (\neg f (x) = \underset{˙}{0} \leftrightarrow f (x) \in (B ∖ \{\underset{˙}{0}\}))$
21	1	lmodfgrp	$⊢ M \in LMod \to R \in Grp$
22	21	adantl	$⊢ (S \in V \land M \in LMod) \to R \in Grp$
23	22	adantr	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to R \in Grp$
24	23	adantr	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to R \in Grp$
25		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
26	2 3 25	grpinvnzcl	$⊢ (R \in Grp \land f (x) \in (B ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (R) (f (x)) \in (B ∖ \{\underset{˙}{0}\})$
27	24 26	sylan	$⊢ ((((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \land f (x) \in (B ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (R) (f (x)) \in (B ∖ \{\underset{˙}{0}\})$
28	27	ex	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (f (x) \in (B ∖ \{\underset{˙}{0}\}) \to {inv}_{g} (R) (f (x)) \in (B ∖ \{\underset{˙}{0}\}))$
29	20 28	sylbid	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (\neg f (x) = \underset{˙}{0} \to {inv}_{g} (R) (f (x)) \in (B ∖ \{\underset{˙}{0}\}))$
30		oveq1	$⊢ y = {inv}_{g} (R) (f (x)) \to y \cdot_{M} x = {inv}_{g} (R) (f (x)) \cdot_{M} x$
31	30	eqeq1d	$⊢ y = {inv}_{g} (R) (f (x)) \to (y \cdot_{M} x = g linC (M) (S ∖ \{x\}) \leftrightarrow {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\}))$
32	31	notbid	$⊢ y = {inv}_{g} (R) (f (x)) \to (\neg y \cdot_{M} x = g linC (M) (S ∖ \{x\}) \leftrightarrow \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\}))$
33	32	orbi2d	$⊢ y = {inv}_{g} (R) (f (x)) \to ((\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} x = g linC (M) (S ∖ \{x\})) \leftrightarrow (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\})))$
34	33	ralbidv	$⊢ y = {inv}_{g} (R) (f (x)) \to (\forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg y \cdot_{M} x = g linC (M) (S ∖ \{x\})) \leftrightarrow \forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\})))$
35	34	rspcva	$⊢ ({inv}_{g} (R) (f (x)) \in (B ∖ \{\underset{˙}{0}\}) \land \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 \forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\}))$
36		simpl	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to (S \in V \land M \in LMod)$
37	36	adantr	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (S \in V \land M \in LMod)$
38		simplrl	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to S \subseteq {Base}_{M}$
39		simplrr	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to x \in S$
40		simpl	$⊢ (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to f \in (B^{S})$
41	40	adantl	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to f \in (B^{S})$
42		eqid	$⊢ {inv}_{g} (R) (f (x)) = {inv}_{g} (R) (f (x))$
43		eqid	$⊢ {f ↾}_{(S ∖ \{x\})} = {f ↾}_{(S ∖ \{x\})}$
44	1 2 3 4 42 43	lindslinindimp2lem2	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S \land f \in (B^{S}))) \to {f ↾}_{(S ∖ \{x\})} \in (B^{(S ∖ \{x\})})$
45	37 38 39 41 44	syl13anc	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to {f ↾}_{(S ∖ \{x\})} \in (B^{(S ∖ \{x\})})$
46		id	$⊢ g = {f ↾}_{(S ∖ \{x\})} \to g = {f ↾}_{(S ∖ \{x\})}$
47	3	a1i	$⊢ g = {f ↾}_{(S ∖ \{x\})} \to \underset{˙}{0} = 0_{R}$
48	46 47	breq12d	$⊢ g = {f ↾}_{(S ∖ \{x\})} \to ({finSupp}_{\underset{˙}{0}} (g) \leftrightarrow {finSupp}_{0_{R}} (({f ↾}_{(S ∖ \{x\})})))$
49	48	notbid	$⊢ g = {f ↾}_{(S ∖ \{x\})} \to (\neg {finSupp}_{\underset{˙}{0}} (g) \leftrightarrow \neg {finSupp}_{0_{R}} (({f ↾}_{(S ∖ \{x\})})))$
50		oveq1	$⊢ g = {f ↾}_{(S ∖ \{x\})} \to g linC (M) (S ∖ \{x\}) = ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\})$
51	50	eqeq2d	$⊢ g = {f ↾}_{(S ∖ \{x\})} \to ({inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\}) \leftrightarrow {inv}_{g} (R) (f (x)) \cdot_{M} x = ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\}))$
52	51	notbid	$⊢ g = {f ↾}_{(S ∖ \{x\})} \to (\neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\}) \leftrightarrow \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\}))$
53	49 52	orbi12d	$⊢ g = {f ↾}_{(S ∖ \{x\})} \to ((\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\})) \leftrightarrow (\neg {finSupp}_{0_{R}} (({f ↾}_{(S ∖ \{x\})})) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\})))$
54	53	rspcva	$⊢ ({f ↾}_{(S ∖ \{x\})} \in (B^{(S ∖ \{x\})}) \land \forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\}))) \to (\neg {finSupp}_{0_{R}} (({f ↾}_{(S ∖ \{x\})})) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\}))$
55	3	breq2i	$⊢ {finSupp}_{\underset{˙}{0}} (f) \leftrightarrow {finSupp}_{0_{R}} (f)$
56	55	biimpi	$⊢ {finSupp}_{\underset{˙}{0}} (f) \to {finSupp}_{0_{R}} (f)$
57	56	adantr	$⊢ ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to {finSupp}_{0_{R}} (f)$
58	57	adantl	$⊢ (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to {finSupp}_{0_{R}} (f)$
59	58	adantl	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to {finSupp}_{0_{R}} (f)$
60		fvexd	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to 0_{R} \in V$
61	59 60	fsuppres	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to {finSupp}_{0_{R}} (({f ↾}_{(S ∖ \{x\})}))$
62	61	pm2.24d	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (\neg {finSupp}_{0_{R}} (({f ↾}_{(S ∖ \{x\})})) \to f (x) = \underset{˙}{0})$
63	62	com12	$⊢ \neg {finSupp}_{0_{R}} (({f ↾}_{(S ∖ \{x\})})) \to ((((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to f (x) = \underset{˙}{0})$
64		simplr	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to M \in LMod$
65	64	adantr	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to M \in LMod$
66	1	fveq2i	$⊢ {Base}_{R} = {Base}_{Scalar (M)}$
67	2 66	eqtr2i	$⊢ {Base}_{Scalar (M)} = B$
68	67	oveq1i	$⊢ {Base}_{Scalar (M)}^{(S ∖ \{x\})} = B^{(S ∖ \{x\})}$
69	45 68	eleqtrrdi	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to {f ↾}_{(S ∖ \{x\})} \in ({Base}_{Scalar (M)}^{(S ∖ \{x\})})$
70		ssdifss	$⊢ S \subseteq {Base}_{M} \to S ∖ \{x\} \subseteq {Base}_{M}$
71	70	adantr	$⊢ (S \subseteq {Base}_{M} \land x \in S) \to S ∖ \{x\} \subseteq {Base}_{M}$
72	71	adantl	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to S ∖ \{x\} \subseteq {Base}_{M}$
73		difexg	$⊢ S \in V \to S ∖ \{x\} \in V$
74	73	adantr	$⊢ (S \in V \land M \in LMod) \to S ∖ \{x\} \in V$
75	74	adantr	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to S ∖ \{x\} \in V$
76		elpwg	$⊢ S ∖ \{x\} \in V \to (S ∖ \{x\} \in 𝒫 {Base}_{M} \leftrightarrow S ∖ \{x\} \subseteq {Base}_{M})$
77	75 76	syl	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to (S ∖ \{x\} \in 𝒫 {Base}_{M} \leftrightarrow S ∖ \{x\} \subseteq {Base}_{M})$
78	72 77	mpbird	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \to S ∖ \{x\} \in 𝒫 {Base}_{M}$
79	78	adantr	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to S ∖ \{x\} \in 𝒫 {Base}_{M}$
80		lincval	$⊢ (M \in LMod \land {f ↾}_{(S ∖ \{x\})} \in ({Base}_{Scalar (M)}^{(S ∖ \{x\})}) \land S ∖ \{x\} \in 𝒫 {Base}_{M}) \to ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\}) = \underset{z \in S ∖ \{x\}}{\sum_{M}} (({f ↾}_{(S ∖ \{x\})}) (z) \cdot_{M} z)$
81	65 69 79 80	syl3anc	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\}) = \underset{z \in S ∖ \{x\}}{\sum_{M}} (({f ↾}_{(S ∖ \{x\})}) (z) \cdot_{M} z)$
82		fvres	$⊢ z \in (S ∖ \{x\}) \to ({f ↾}_{(S ∖ \{x\})}) (z) = f (z)$
83	82	adantl	$⊢ ((((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \land z \in (S ∖ \{x\})) \to ({f ↾}_{(S ∖ \{x\})}) (z) = f (z)$
84	83	oveq1d	$⊢ ((((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \land z \in (S ∖ \{x\})) \to ({f ↾}_{(S ∖ \{x\})}) (z) \cdot_{M} z = f (z) \cdot_{M} z$
85	84	mpteq2dva	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (z \in (S ∖ \{x\}) ⟼ ({f ↾}_{(S ∖ \{x\})}) (z) \cdot_{M} z) = (z \in (S ∖ \{x\}) ⟼ f (z) \cdot_{M} z)$
86	85	oveq2d	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to \underset{z \in S ∖ \{x\}}{\sum_{M}} (({f ↾}_{(S ∖ \{x\})}) (z) \cdot_{M} z) = \underset{z \in S ∖ \{x\}}{\sum_{M}} (f (z) \cdot_{M} z)$
87		simplr	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (S \subseteq {Base}_{M} \land x \in S)$
88		3anass	$⊢ (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \leftrightarrow (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))$
89	88	bicomi	$⊢ (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \leftrightarrow (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)$
90	89	biimpi	$⊢ (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)$
91	90	adantl	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)$
92	1 2 3 4 42 43	lindslinindimp2lem4	$⊢ ((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S) \land (f \in (B^{S}) \land {finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z)) \to \underset{z \in S ∖ \{x\}}{\sum_{M}} (f (z) \cdot_{M} z) = {inv}_{g} (R) (f (x)) \cdot_{M} x$
93	37 87 91 92	syl3anc	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to \underset{z \in S ∖ \{x\}}{\sum_{M}} (f (z) \cdot_{M} z) = {inv}_{g} (R) (f (x)) \cdot_{M} x$
94	81 86 93	3eqtrrd	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to {inv}_{g} (R) (f (x)) \cdot_{M} x = ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\})$
95	94	pm2.24d	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (\neg {inv}_{g} (R) (f (x)) \cdot_{M} x = ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\}) \to f (x) = \underset{˙}{0})$
96	95	com12	$⊢ \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\}) \to ((((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to f (x) = \underset{˙}{0})$
97	63 96	jaoi	$⊢ (\neg {finSupp}_{0_{R}} (({f ↾}_{(S ∖ \{x\})})) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = ({f ↾}_{(S ∖ \{x\})}) linC (M) (S ∖ \{x\})) \to ((((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to f (x) = \underset{˙}{0})$
98	54 97	syl	$⊢ ({f ↾}_{(S ∖ \{x\})} \in (B^{(S ∖ \{x\})}) \land \forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\}))) \to ((((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to f (x) = \underset{˙}{0})$
99	98	ex	$⊢ {f ↾}_{(S ∖ \{x\})} \in (B^{(S ∖ \{x\})}) \to (\forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\})) \to ((((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to f (x) = \underset{˙}{0}))$
100	99	com23	$⊢ {f ↾}_{(S ∖ \{x\})} \in (B^{(S ∖ \{x\})}) \to ((((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (\forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\})) \to f (x) = \underset{˙}{0}))$
101	45 100	mpcom	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (\forall g \in (B^{(S ∖ \{x\})}) (\neg {finSupp}_{\underset{˙}{0}} (g) \lor \neg {inv}_{g} (R) (f (x)) \cdot_{M} x = g linC (M) (S ∖ \{x\})) \to f (x) = \underset{˙}{0})$
102	35 101	syl5	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to (({inv}_{g} (R) (f (x)) \in (B ∖ \{\underset{˙}{0}\}) \land \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})$
103	102	expd	$⊢ (((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (f \in (B^{S}) \land ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z))) \to ({inv}_{g} (R) (f (x)) \in (B ∖ \{\underset{˙}{0}\}) \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}))$
104	29 103	syldc	$⊢ \neg f (x) = \underset{˙}{0} \to ((((S \in V \land M \in LMod) \land (S \subseteq {Base}_{M} \land x \in S)) \land (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}))$
105	104	expd	$⊢ \neg f (x) = \underset{˙}{0} \to (((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})))$
106	6 105	pm2.61i	$⊢ ((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}))$

Metamath Proof Explorer

Theorem lindslinindsimp2lem5

Proof