snlindsntorlem

	Ref	Expression
Hypotheses	snlindsntor.b	$⊢ B = {Base}_{M}$
	snlindsntor.r	$⊢ R = Scalar (M)$
	snlindsntor.s	$⊢ S = {Base}_{R}$
	snlindsntor.0	$⊢ \underset{˙}{0} = 0_{R}$
	snlindsntor.z	$⊢ Z = 0_{M}$
	snlindsntor.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
Assertion	snlindsntorlem	$⊢ (M \in LMod \land X \in B) \to (\forall f \in (S^{\{X\}}) (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}) \to \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		snlindsntor.b	$⊢ B = {Base}_{M}$
2		snlindsntor.r	$⊢ R = Scalar (M)$
3		snlindsntor.s	$⊢ S = {Base}_{R}$
4		snlindsntor.0	$⊢ \underset{˙}{0} = 0_{R}$
5		snlindsntor.z	$⊢ Z = 0_{M}$
6		snlindsntor.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
7		eqidd	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to \{⟨X, s⟩\} = \{⟨X, s⟩\}$
8		fsng	$⊢ (X \in B \land s \in S) \to (\{⟨X, s⟩\} : \{X\} ⟶ \{s\} \leftrightarrow \{⟨X, s⟩\} = \{⟨X, s⟩\})$
9	8	adantll	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to (\{⟨X, s⟩\} : \{X\} ⟶ \{s\} \leftrightarrow \{⟨X, s⟩\} = \{⟨X, s⟩\})$
10	7 9	mpbird	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to \{⟨X, s⟩\} : \{X\} ⟶ \{s\}$
11		snssi	$⊢ s \in S \to \{s\} \subseteq S$
12	11	adantl	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to \{s\} \subseteq S$
13	10 12	fssd	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to \{⟨X, s⟩\} : \{X\} ⟶ S$
14	3	fvexi	$⊢ S \in V$
15		snex	$⊢ \{X\} \in V$
16	14 15	pm3.2i	$⊢ (S \in V \land \{X\} \in V)$
17		elmapg	$⊢ (S \in V \land \{X\} \in V) \to (\{⟨X, s⟩\} \in (S^{\{X\}}) \leftrightarrow \{⟨X, s⟩\} : \{X\} ⟶ S)$
18	16 17	mp1i	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to (\{⟨X, s⟩\} \in (S^{\{X\}}) \leftrightarrow \{⟨X, s⟩\} : \{X\} ⟶ S)$
19	13 18	mpbird	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to \{⟨X, s⟩\} \in (S^{\{X\}})$
20		oveq1	$⊢ f = \{⟨X, s⟩\} \to f linC (M) \{X\} = \{⟨X, s⟩\} linC (M) \{X\}$
21	20	eqeq1d	$⊢ f = \{⟨X, s⟩\} \to (f linC (M) \{X\} = Z \leftrightarrow \{⟨X, s⟩\} linC (M) \{X\} = Z)$
22		fveq1	$⊢ f = \{⟨X, s⟩\} \to f (X) = \{⟨X, s⟩\} (X)$
23	22	eqeq1d	$⊢ f = \{⟨X, s⟩\} \to (f (X) = \underset{˙}{0} \leftrightarrow \{⟨X, s⟩\} (X) = \underset{˙}{0})$
24	21 23	imbi12d	$⊢ f = \{⟨X, s⟩\} \to ((f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}) \leftrightarrow (\{⟨X, s⟩\} linC (M) \{X\} = Z \to \{⟨X, s⟩\} (X) = \underset{˙}{0}))$
25	1 2 3 6	lincvalsng	$⊢ (M \in LMod \land X \in B \land s \in S) \to \{⟨X, s⟩\} linC (M) \{X\} = s \underset{˙}{\cdot} X$
26	25	3expa	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to \{⟨X, s⟩\} linC (M) \{X\} = s \underset{˙}{\cdot} X$
27	26	eqeq1d	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to (\{⟨X, s⟩\} linC (M) \{X\} = Z \leftrightarrow s \underset{˙}{\cdot} X = Z)$
28		fvsng	$⊢ (X \in B \land s \in S) \to \{⟨X, s⟩\} (X) = s$
29	28	adantll	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to \{⟨X, s⟩\} (X) = s$
30	29	eqeq1d	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to (\{⟨X, s⟩\} (X) = \underset{˙}{0} \leftrightarrow s = \underset{˙}{0})$
31	27 30	imbi12d	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to ((\{⟨X, s⟩\} linC (M) \{X\} = Z \to \{⟨X, s⟩\} (X) = \underset{˙}{0}) \leftrightarrow (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))$
32	24 31	sylan9bbr	$⊢ (((M \in LMod \land X \in B) \land s \in S) \land f = \{⟨X, s⟩\}) \to ((f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}) \leftrightarrow (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))$
33	19 32	rspcdv	$⊢ ((M \in LMod \land X \in B) \land s \in S) \to (\forall f \in (S^{\{X\}}) (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}) \to (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))$
34	33	ralrimdva	$⊢ (M \in LMod \land X \in B) \to (\forall f \in (S^{\{X\}}) (f linC (M) \{X\} = Z \to f (X) = \underset{˙}{0}) \to \forall s \in S (s \underset{˙}{\cdot} X = Z \to s = \underset{˙}{0}))$

Metamath Proof Explorer

Theorem snlindsntorlem

Proof