prjspeclsp

Description: The vectors equivalent to a vector X are the nonzero vectors in the span of X . (Contributed by Steven Nguyen, 6-Jun-2023)

	Ref	Expression
Hypotheses	prjsprel.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
	prjspertr.b	$⊢ B = {Base}_{V} ∖ \{0_{V}\}$
	prjspertr.s	$⊢ S = Scalar (V)$
	prjspertr.x	$⊢ \underset{˙}{\cdot} = \cdot_{V}$
	prjspertr.k	$⊢ K = {Base}_{S}$
	prjsprellsp.n	$⊢ N = LSpan (V)$
Assertion	prjspeclsp	$⊢ (V \in LVec \land X \in B) \to [X] \underset{˙}{\sim} = N (\{X\}) ∖ \{0_{V}\}$

Proof

Step	Hyp	Ref	Expression
1		prjsprel.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
2		prjspertr.b	$⊢ B = {Base}_{V} ∖ \{0_{V}\}$
3		prjspertr.s	$⊢ S = Scalar (V)$
4		prjspertr.x	$⊢ \underset{˙}{\cdot} = \cdot_{V}$
5		prjspertr.k	$⊢ K = {Base}_{S}$
6		prjsprellsp.n	$⊢ N = LSpan (V)$
7	1	cnveqi	$⊢ {\underset{˙}{\sim}}^{-1} = {\{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}}^{-1}$
8		cnvopab	$⊢ {\{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}}^{-1} = \{⟨y, x⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
9	7 8	eqtri	$⊢ {\underset{˙}{\sim}}^{-1} = \{⟨y, x⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
10	9	eceq2i	$⊢ [X] {\underset{˙}{\sim}}^{-1} = [X] \{⟨y, x⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
11		df-ec	$⊢ [X] \{⟨y, x⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\} = \{⟨y, x⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\} [\{X\}]$
12	11	a1i	$⊢ (V \in LVec \land X \in B) \to [X] \{⟨y, x⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\} = \{⟨y, x⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\} [\{X\}]$
13		imaopab	$⊢ \{⟨y, x⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\} [\{X\}] = \{x \| \exists y \in \{X\} ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
14	13	a1i	$⊢ (V \in LVec \land X \in B) \to \{⟨y, x⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\} [\{X\}] = \{x \| \exists y \in \{X\} ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
15		df-rex	$⊢ \exists y \in \{X\} ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y) \leftrightarrow \exists y (y \in \{X\} \land ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y))$
16		velsn	$⊢ y \in \{X\} \leftrightarrow y = X$
17	16	anbi1i	$⊢ (y \in \{X\} \land ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)) \leftrightarrow (y = X \land ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y))$
18		eleq1	$⊢ y = X \to (y \in B \leftrightarrow X \in B)$
19	18	anbi2d	$⊢ y = X \to ((x \in B \land y \in B) \leftrightarrow (x \in B \land X \in B))$
20		oveq2	$⊢ y = X \to l \underset{˙}{\cdot} y = l \underset{˙}{\cdot} X$
21	20	eqeq2d	$⊢ y = X \to (x = l \underset{˙}{\cdot} y \leftrightarrow x = l \underset{˙}{\cdot} X)$
22	21	rexbidv	$⊢ y = X \to (\exists l \in K x = l \underset{˙}{\cdot} y \leftrightarrow \exists l \in K x = l \underset{˙}{\cdot} X)$
23	19 22	anbi12d	$⊢ y = X \to (((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y) \leftrightarrow ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X))$
24	23	pm5.32i	$⊢ (y = X \land ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)) \leftrightarrow (y = X \land ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X))$
25	17 24	bitri	$⊢ (y \in \{X\} \land ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)) \leftrightarrow (y = X \land ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X))$
26	25	exbii	$⊢ \exists y (y \in \{X\} \land ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)) \leftrightarrow \exists y (y = X \land ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X))$
27		19.41v	$⊢ \exists y (y = X \land ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X)) \leftrightarrow (\exists y y = X \land ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X))$
28		elisset	$⊢ X \in B \to \exists y y = X$
29	28	ad2antlr	$⊢ ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X) \to \exists y y = X$
30	29	pm4.71ri	$⊢ ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X) \leftrightarrow (\exists y y = X \land ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X))$
31	27 30	bitr4i	$⊢ \exists y (y = X \land ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X)) \leftrightarrow ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X)$
32	15 26 31	3bitri	$⊢ \exists y \in \{X\} ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y) \leftrightarrow ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X)$
33	32	abbii	$⊢ \{x \| \exists y \in \{X\} ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\} = \{x \| ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X)\}$
34		iba	$⊢ X \in B \to (x \in B \leftrightarrow (x \in B \land X \in B))$
35	34	bicomd	$⊢ X \in B \to ((x \in B \land X \in B) \leftrightarrow x \in B)$
36	35	anbi1d	$⊢ X \in B \to (((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X) \leftrightarrow (x \in B \land \exists l \in K x = l \underset{˙}{\cdot} X))$
37	36	abbidv	$⊢ X \in B \to \{x \| ((x \in B \land X \in B) \land \exists l \in K x = l \underset{˙}{\cdot} X)\} = \{x \| (x \in B \land \exists l \in K x = l \underset{˙}{\cdot} X)\}$
38	33 37	syl5eq	$⊢ X \in B \to \{x \| \exists y \in \{X\} ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\} = \{x \| (x \in B \land \exists l \in K x = l \underset{˙}{\cdot} X)\}$
39	38	adantl	$⊢ (V \in LVec \land X \in B) \to \{x \| \exists y \in \{X\} ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\} = \{x \| (x \in B \land \exists l \in K x = l \underset{˙}{\cdot} X)\}$
40	12 14 39	3eqtrd	$⊢ (V \in LVec \land X \in B) \to [X] \{⟨y, x⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\} = \{x \| (x \in B \land \exists l \in K x = l \underset{˙}{\cdot} X)\}$
41	10 40	syl5eq	$⊢ (V \in LVec \land X \in B) \to [X] {\underset{˙}{\sim}}^{-1} = \{x \| (x \in B \land \exists l \in K x = l \underset{˙}{\cdot} X)\}$
42		df-rab	$⊢ \{x \in B \| \exists l \in K x = l \underset{˙}{\cdot} X\} = \{x \| (x \in B \land \exists l \in K x = l \underset{˙}{\cdot} X)\}$
43	42	a1i	$⊢ (V \in LVec \land X \in B) \to \{x \in B \| \exists l \in K x = l \underset{˙}{\cdot} X\} = \{x \| (x \in B \land \exists l \in K x = l \underset{˙}{\cdot} X)\}$
44	2	rabeqi	$⊢ \{x \in B \| \exists l \in K x = l \underset{˙}{\cdot} X\} = \{x \in ({Base}_{V} ∖ \{0_{V}\}) \| \exists l \in K x = l \underset{˙}{\cdot} X\}$
45		rabdif	$⊢ \{x \in {Base}_{V} \| \exists l \in K x = l \underset{˙}{\cdot} X\} ∖ \{0_{V}\} = \{x \in ({Base}_{V} ∖ \{0_{V}\}) \| \exists l \in K x = l \underset{˙}{\cdot} X\}$
46	45	a1i	$⊢ (V \in LVec \land X \in B) \to \{x \in {Base}_{V} \| \exists l \in K x = l \underset{˙}{\cdot} X\} ∖ \{0_{V}\} = \{x \in ({Base}_{V} ∖ \{0_{V}\}) \| \exists l \in K x = l \underset{˙}{\cdot} X\}$
47	44 46	eqtr4id	$⊢ (V \in LVec \land X \in B) \to \{x \in B \| \exists l \in K x = l \underset{˙}{\cdot} X\} = \{x \in {Base}_{V} \| \exists l \in K x = l \underset{˙}{\cdot} X\} ∖ \{0_{V}\}$
48	41 43 47	3eqtr2d	$⊢ (V \in LVec \land X \in B) \to [X] {\underset{˙}{\sim}}^{-1} = \{x \in {Base}_{V} \| \exists l \in K x = l \underset{˙}{\cdot} X\} ∖ \{0_{V}\}$
49	1 2 3 4 5	prjsper	$⊢ V \in LVec \to \underset{˙}{\sim} Er B$
50	49	adantr	$⊢ (V \in LVec \land X \in B) \to \underset{˙}{\sim} Er B$
51		ercnv	$⊢ \underset{˙}{\sim} Er B \to {\underset{˙}{\sim}}^{-1} = \underset{˙}{\sim}$
52	51	eqcomd	$⊢ \underset{˙}{\sim} Er B \to \underset{˙}{\sim} = {\underset{˙}{\sim}}^{-1}$
53	50 52	syl	$⊢ (V \in LVec \land X \in B) \to \underset{˙}{\sim} = {\underset{˙}{\sim}}^{-1}$
54	53	eceq2d	$⊢ (V \in LVec \land X \in B) \to [X] \underset{˙}{\sim} = [X] {\underset{˙}{\sim}}^{-1}$
55		lveclmod	$⊢ V \in LVec \to V \in LMod$
56		difss	$⊢ {Base}_{V} ∖ \{0_{V}\} \subseteq {Base}_{V}$
57	2 56	eqsstri	$⊢ B \subseteq {Base}_{V}$
58	57	sseli	$⊢ X \in B \to X \in {Base}_{V}$
59		eqid	$⊢ {Base}_{V} = {Base}_{V}$
60	3 5 59 4 6	lspsn	$⊢ (V \in LMod \land X \in {Base}_{V}) \to N (\{X\}) = \{x \| \exists l \in K x = l \underset{˙}{\cdot} X\}$
61	55 58 60	syl2an	$⊢ (V \in LVec \land X \in B) \to N (\{X\}) = \{x \| \exists l \in K x = l \underset{˙}{\cdot} X\}$
62		simpr	$⊢ (((V \in LVec \land X \in B) \land l \in K) \land x = l \underset{˙}{\cdot} X) \to x = l \underset{˙}{\cdot} X$
63	55	adantr	$⊢ (V \in LVec \land X \in B) \to V \in LMod$
64	63	adantr	$⊢ ((V \in LVec \land X \in B) \land l \in K) \to V \in LMod$
65		simpr	$⊢ ((V \in LVec \land X \in B) \land l \in K) \to l \in K$
66	58	ad2antlr	$⊢ ((V \in LVec \land X \in B) \land l \in K) \to X \in {Base}_{V}$
67	59 3 4 5	lmodvscl	$⊢ (V \in LMod \land l \in K \land X \in {Base}_{V}) \to l \underset{˙}{\cdot} X \in {Base}_{V}$
68	64 65 66 67	syl3anc	$⊢ ((V \in LVec \land X \in B) \land l \in K) \to l \underset{˙}{\cdot} X \in {Base}_{V}$
69	68	adantr	$⊢ (((V \in LVec \land X \in B) \land l \in K) \land x = l \underset{˙}{\cdot} X) \to l \underset{˙}{\cdot} X \in {Base}_{V}$
70	62 69	eqeltrd	$⊢ (((V \in LVec \land X \in B) \land l \in K) \land x = l \underset{˙}{\cdot} X) \to x \in {Base}_{V}$
71	70	rexlimdva2	$⊢ (V \in LVec \land X \in B) \to (\exists l \in K x = l \underset{˙}{\cdot} X \to x \in {Base}_{V})$
72	71	pm4.71rd	$⊢ (V \in LVec \land X \in B) \to (\exists l \in K x = l \underset{˙}{\cdot} X \leftrightarrow (x \in {Base}_{V} \land \exists l \in K x = l \underset{˙}{\cdot} X))$
73	72	abbidv	$⊢ (V \in LVec \land X \in B) \to \{x \| \exists l \in K x = l \underset{˙}{\cdot} X\} = \{x \| (x \in {Base}_{V} \land \exists l \in K x = l \underset{˙}{\cdot} X)\}$
74		df-rab	$⊢ \{x \in {Base}_{V} \| \exists l \in K x = l \underset{˙}{\cdot} X\} = \{x \| (x \in {Base}_{V} \land \exists l \in K x = l \underset{˙}{\cdot} X)\}$
75	73 74	eqtr4di	$⊢ (V \in LVec \land X \in B) \to \{x \| \exists l \in K x = l \underset{˙}{\cdot} X\} = \{x \in {Base}_{V} \| \exists l \in K x = l \underset{˙}{\cdot} X\}$
76	61 75	eqtrd	$⊢ (V \in LVec \land X \in B) \to N (\{X\}) = \{x \in {Base}_{V} \| \exists l \in K x = l \underset{˙}{\cdot} X\}$
77	76	difeq1d	$⊢ (V \in LVec \land X \in B) \to N (\{X\}) ∖ \{0_{V}\} = \{x \in {Base}_{V} \| \exists l \in K x = l \underset{˙}{\cdot} X\} ∖ \{0_{V}\}$
78	48 54 77	3eqtr4d	$⊢ (V \in LVec \land X \in B) \to [X] \underset{˙}{\sim} = N (\{X\}) ∖ \{0_{V}\}$

Metamath Proof Explorer

Theorem prjspeclsp

Proof