lspsnvs

Description: A nonzero scalar product does not change the span of a singleton. ( spansncol analog.) (Contributed by NM, 23-Apr-2014)

	Ref	Expression
Hypotheses	lspsnvs.v	$⊢ V = {Base}_{W}$
	lspsnvs.f	$⊢ F = Scalar (W)$
	lspsnvs.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lspsnvs.k	$⊢ K = {Base}_{F}$
	lspsnvs.o	$⊢ \underset{˙}{0} = 0_{F}$
	lspsnvs.n	$⊢ N = LSpan (W)$
Assertion	lspsnvs	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to N (\{R \underset{˙}{\cdot} X\}) = N (\{X\})$

Proof

Step	Hyp	Ref	Expression
1		lspsnvs.v	$⊢ V = {Base}_{W}$
2		lspsnvs.f	$⊢ F = Scalar (W)$
3		lspsnvs.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lspsnvs.k	$⊢ K = {Base}_{F}$
5		lspsnvs.o	$⊢ \underset{˙}{0} = 0_{F}$
6		lspsnvs.n	$⊢ N = LSpan (W)$
7		lveclmod	$⊢ W \in LVec \to W \in LMod$
8	7	3ad2ant1	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to W \in LMod$
9		simp2l	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to R \in K$
10		simp3	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to X \in V$
11	2 4 1 3 6	lspsnvsi	$⊢ (W \in LMod \land R \in K \land X \in V) \to N (\{R \underset{˙}{\cdot} X\}) \subseteq N (\{X\})$
12	8 9 10 11	syl3anc	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to N (\{R \underset{˙}{\cdot} X\}) \subseteq N (\{X\})$
13	2	lvecdrng	$⊢ W \in LVec \to F \in DivRing$
14	13	3ad2ant1	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to F \in DivRing$
15		simp2r	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to R \neq \underset{˙}{0}$
16		eqid	$⊢ \cdot_{F} = \cdot_{F}$
17		eqid	$⊢ 1_{F} = 1_{F}$
18		eqid	$⊢ {inv}_{r} (F) = {inv}_{r} (F)$
19	4 5 16 17 18	drnginvrl	$⊢ (F \in DivRing \land R \in K \land R \neq \underset{˙}{0}) \to {inv}_{r} (F) (R) \cdot_{F} R = 1_{F}$
20	14 9 15 19	syl3anc	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to {inv}_{r} (F) (R) \cdot_{F} R = 1_{F}$
21	20	oveq1d	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to ({inv}_{r} (F) (R) \cdot_{F} R) \underset{˙}{\cdot} X = 1_{F} \underset{˙}{\cdot} X$
22	4 5 18	drnginvrcl	$⊢ (F \in DivRing \land R \in K \land R \neq \underset{˙}{0}) \to {inv}_{r} (F) (R) \in K$
23	14 9 15 22	syl3anc	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to {inv}_{r} (F) (R) \in K$
24	1 2 3 4 16	lmodvsass	$⊢ (W \in LMod \land ({inv}_{r} (F) (R) \in K \land R \in K \land X \in V)) \to ({inv}_{r} (F) (R) \cdot_{F} R) \underset{˙}{\cdot} X = {inv}_{r} (F) (R) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$
25	8 23 9 10 24	syl13anc	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to ({inv}_{r} (F) (R) \cdot_{F} R) \underset{˙}{\cdot} X = {inv}_{r} (F) (R) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$
26	1 2 3 17	lmodvs1	$⊢ (W \in LMod \land X \in V) \to 1_{F} \underset{˙}{\cdot} X = X$
27	8 10 26	syl2anc	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to 1_{F} \underset{˙}{\cdot} X = X$
28	21 25 27	3eqtr3d	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to {inv}_{r} (F) (R) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X) = X$
29	28	sneqd	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to \{{inv}_{r} (F) (R) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)\} = \{X\}$
30	29	fveq2d	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to N (\{{inv}_{r} (F) (R) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)\}) = N (\{X\})$
31	1 2 3 4	lmodvscl	$⊢ (W \in LMod \land R \in K \land X \in V) \to R \underset{˙}{\cdot} X \in V$
32	8 9 10 31	syl3anc	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to R \underset{˙}{\cdot} X \in V$
33	2 4 1 3 6	lspsnvsi	$⊢ (W \in LMod \land {inv}_{r} (F) (R) \in K \land R \underset{˙}{\cdot} X \in V) \to N (\{{inv}_{r} (F) (R) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)\}) \subseteq N (\{R \underset{˙}{\cdot} X\})$
34	8 23 32 33	syl3anc	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to N (\{{inv}_{r} (F) (R) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)\}) \subseteq N (\{R \underset{˙}{\cdot} X\})$
35	30 34	eqsstrrd	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to N (\{X\}) \subseteq N (\{R \underset{˙}{\cdot} X\})$
36	12 35	eqssd	$⊢ (W \in LVec \land (R \in K \land R \neq \underset{˙}{0}) \land X \in V) \to N (\{R \underset{˙}{\cdot} X\}) = N (\{X\})$

Metamath Proof Explorer

Theorem lspsnvs

Proof