prjsperref

Description: The relation in PrjSp is reflexive. (Contributed by Steven Nguyen, 30-Apr-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}$
Assertion	prjsperref	$⊢ V \in LMod \to (X \in B \leftrightarrow X \underset{˙}{\sim} X)$

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		eqid	$⊢ 1_{S} = 1_{S}$
7	3 5 6	lmod1cl	$⊢ V \in LMod \to 1_{S} \in K$
8	7	adantr	$⊢ (V \in LMod \land X \in B) \to 1_{S} \in K$
9		oveq1	$⊢ m = 1_{S} \to m \underset{˙}{\cdot} X = 1_{S} \underset{˙}{\cdot} X$
10	9	eqeq2d	$⊢ m = 1_{S} \to (X = m \underset{˙}{\cdot} X \leftrightarrow X = 1_{S} \underset{˙}{\cdot} X)$
11	10	adantl	$⊢ ((V \in LMod \land X \in B) \land m = 1_{S}) \to (X = m \underset{˙}{\cdot} X \leftrightarrow X = 1_{S} \underset{˙}{\cdot} X)$
12		eldifi	$⊢ X \in ({Base}_{V} ∖ \{0_{V}\}) \to X \in {Base}_{V}$
13	12 2	eleq2s	$⊢ X \in B \to X \in {Base}_{V}$
14		eqid	$⊢ {Base}_{V} = {Base}_{V}$
15	14 3 4 6	lmodvs1	$⊢ (V \in LMod \land X \in {Base}_{V}) \to 1_{S} \underset{˙}{\cdot} X = X$
16	13 15	sylan2	$⊢ (V \in LMod \land X \in B) \to 1_{S} \underset{˙}{\cdot} X = X$
17	16	eqcomd	$⊢ (V \in LMod \land X \in B) \to X = 1_{S} \underset{˙}{\cdot} X$
18	8 11 17	rspcedvd	$⊢ (V \in LMod \land X \in B) \to \exists m \in K X = m \underset{˙}{\cdot} X$
19	18	ex	$⊢ V \in LMod \to (X \in B \to \exists m \in K X = m \underset{˙}{\cdot} X)$
20	19	pm4.71d	$⊢ V \in LMod \to (X \in B \leftrightarrow (X \in B \land \exists m \in K X = m \underset{˙}{\cdot} X))$
21		pm4.24	$⊢ X \in B \leftrightarrow (X \in B \land X \in B)$
22	21	anbi1i	$⊢ (X \in B \land \exists m \in K X = m \underset{˙}{\cdot} X) \leftrightarrow ((X \in B \land X \in B) \land \exists m \in K X = m \underset{˙}{\cdot} X)$
23	1	prjsprel	$⊢ X \underset{˙}{\sim} X \leftrightarrow ((X \in B \land X \in B) \land \exists m \in K X = m \underset{˙}{\cdot} X)$
24	22 23	bitr4i	$⊢ (X \in B \land \exists m \in K X = m \underset{˙}{\cdot} X) \leftrightarrow X \underset{˙}{\sim} X$
25	20 24	bitrdi	$⊢ V \in LMod \to (X \in B \leftrightarrow X \underset{˙}{\sim} X)$

Metamath Proof Explorer

Theorem prjsperref

Proof