prjspersym

Description: The relation in PrjSp is symmetric. (Contributed by Steven Nguyen, 1-May-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	prjspersym	$⊢ (V \in LVec \land X \underset{˙}{\sim} Y) \to Y \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		simpllr	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to X \underset{˙}{\sim} Y$
7	1	prjsprel	$⊢ X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y)$
8		pm3.22	$⊢ (X \in B \land Y \in B) \to (Y \in B \land X \in B)$
9	8	adantr	$⊢ ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y) \to (Y \in B \land X \in B)$
10	7 9	sylbi	$⊢ X \underset{˙}{\sim} Y \to (Y \in B \land X \in B)$
11	6 10	syl	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to (Y \in B \land X \in B)$
12		oveq1	$⊢ n = {inv}_{r} (S) (m) \to n \underset{˙}{\cdot} X = {inv}_{r} (S) (m) \underset{˙}{\cdot} X$
13	12	eqeq2d	$⊢ n = {inv}_{r} (S) (m) \to (Y = n \underset{˙}{\cdot} X \leftrightarrow Y = {inv}_{r} (S) (m) \underset{˙}{\cdot} X)$
14		simplll	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to V \in LVec$
15	3	lvecdrng	$⊢ V \in LVec \to S \in DivRing$
16	14 15	syl	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to S \in DivRing$
17		simplr	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to m \in K$
18		simpll	$⊢ ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y) \to X \in B$
19	7 18	sylbi	$⊢ X \underset{˙}{\sim} Y \to X \in B$
20		eldifsni	$⊢ X \in ({Base}_{V} ∖ \{0_{V}\}) \to X \neq 0_{V}$
21	20 2	eleq2s	$⊢ X \in B \to X \neq 0_{V}$
22	6 19 21	3syl	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to X \neq 0_{V}$
23		simplr	$⊢ ((((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \land m = 0_{S}) \to X = m \underset{˙}{\cdot} Y$
24		simpr	$⊢ ((((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \land m = 0_{S}) \to m = 0_{S}$
25	24	oveq1d	$⊢ ((((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \land m = 0_{S}) \to m \underset{˙}{\cdot} Y = 0_{S} \underset{˙}{\cdot} Y$
26		lveclmod	$⊢ V \in LVec \to V \in LMod$
27	26	ad4antr	$⊢ ((((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \land m = 0_{S}) \to V \in LMod$
28		simplr	$⊢ ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y) \to Y \in B$
29	7 28	sylbi	$⊢ X \underset{˙}{\sim} Y \to Y \in B$
30		eldifi	$⊢ Y \in ({Base}_{V} ∖ \{0_{V}\}) \to Y \in {Base}_{V}$
31	30 2	eleq2s	$⊢ Y \in B \to Y \in {Base}_{V}$
32	6 29 31	3syl	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to Y \in {Base}_{V}$
33	32	adantr	$⊢ ((((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \land m = 0_{S}) \to Y \in {Base}_{V}$
34		eqid	$⊢ {Base}_{V} = {Base}_{V}$
35		eqid	$⊢ 0_{S} = 0_{S}$
36		eqid	$⊢ 0_{V} = 0_{V}$
37	34 3 4 35 36	lmod0vs	$⊢ (V \in LMod \land Y \in {Base}_{V}) \to 0_{S} \underset{˙}{\cdot} Y = 0_{V}$
38	27 33 37	syl2anc	$⊢ ((((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \land m = 0_{S}) \to 0_{S} \underset{˙}{\cdot} Y = 0_{V}$
39	23 25 38	3eqtrd	$⊢ ((((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \land m = 0_{S}) \to X = 0_{V}$
40	22 39	mteqand	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to m \neq 0_{S}$
41		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
42	5 35 41	drnginvrcl	$⊢ (S \in DivRing \land m \in K \land m \neq 0_{S}) \to {inv}_{r} (S) (m) \in K$
43	16 17 40 42	syl3anc	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to {inv}_{r} (S) (m) \in K$
44		simpr	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to X = m \underset{˙}{\cdot} Y$
45		nelsn	$⊢ m \neq 0_{S} \to \neg m \in \{0_{S}\}$
46	40 45	syl	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to \neg m \in \{0_{S}\}$
47	17 46	eldifd	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to m \in (K ∖ \{0_{S}\})$
48		eldifi	$⊢ X \in ({Base}_{V} ∖ \{0_{V}\}) \to X \in {Base}_{V}$
49	48 2	eleq2s	$⊢ X \in B \to X \in {Base}_{V}$
50	6 19 49	3syl	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to X \in {Base}_{V}$
51	34 4 3 5 35 41 14 47 50 32	lvecinv	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to (X = m \underset{˙}{\cdot} Y \leftrightarrow Y = {inv}_{r} (S) (m) \underset{˙}{\cdot} X)$
52	44 51	mpbid	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to Y = {inv}_{r} (S) (m) \underset{˙}{\cdot} X$
53	13 43 52	rspcedvdw	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to \exists n \in K Y = n \underset{˙}{\cdot} X$
54	1	prjsprel	$⊢ Y \underset{˙}{\sim} X \leftrightarrow ((Y \in B \land X \in B) \land \exists n \in K Y = n \underset{˙}{\cdot} X)$
55	11 53 54	sylanbrc	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to Y \underset{˙}{\sim} X$
56		simpr	$⊢ ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y) \to \exists m \in K X = m \underset{˙}{\cdot} Y$
57	7 56	sylbi	$⊢ X \underset{˙}{\sim} Y \to \exists m \in K X = m \underset{˙}{\cdot} Y$
58	57	adantl	$⊢ (V \in LVec \land X \underset{˙}{\sim} Y) \to \exists m \in K X = m \underset{˙}{\cdot} Y$
59	55 58	r19.29a	$⊢ (V \in LVec \land X \underset{˙}{\sim} Y) \to Y \underset{˙}{\sim} X$

Metamath Proof Explorer

Theorem prjspersym

Proof