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		simplll	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to V \in LVec$
13	3	lvecdrng	$⊢ V \in LVec \to S \in DivRing$
14	12 13	syl	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to S \in DivRing$
15		simplr	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to m \in K$
16		simpll	$⊢ ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y) \to X \in B$
17	7 16	sylbi	$⊢ X \underset{˙}{\sim} Y \to X \in B$
18		eldifsni	$⊢ X \in ({Base}_{V} ∖ \{0_{V}\}) \to X \neq 0_{V}$
19	18 2	eleq2s	$⊢ X \in B \to X \neq 0_{V}$
20	6 17 19	3syl	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to X \neq 0_{V}$
21		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$
22		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}$
23	22	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$
24		lveclmod	$⊢ V \in LVec \to V \in LMod$
25	24	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$
26		simplr	$⊢ ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y) \to Y \in B$
27	7 26	sylbi	$⊢ X \underset{˙}{\sim} Y \to Y \in B$
28		eldifi	$⊢ Y \in ({Base}_{V} ∖ \{0_{V}\}) \to Y \in {Base}_{V}$
29	28 2	eleq2s	$⊢ Y \in B \to Y \in {Base}_{V}$
30	6 27 29	3syl	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to Y \in {Base}_{V}$
31	30	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}$
32		eqid	$⊢ {Base}_{V} = {Base}_{V}$
33		eqid	$⊢ 0_{S} = 0_{S}$
34		eqid	$⊢ 0_{V} = 0_{V}$
35	32 3 4 33 34	lmod0vs	$⊢ (V \in LMod \land Y \in {Base}_{V}) \to 0_{S} \underset{˙}{\cdot} Y = 0_{V}$
36	25 31 35	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}$
37	21 23 36	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}$
38	20 37	mteqand	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to m \neq 0_{S}$
39		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
40	5 33 39	drnginvrcl	$⊢ (S \in DivRing \land m \in K \land m \neq 0_{S}) \to {inv}_{r} (S) (m) \in K$
41	14 15 38 40	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$
42		oveq1	$⊢ n = {inv}_{r} (S) (m) \to n \underset{˙}{\cdot} X = {inv}_{r} (S) (m) \underset{˙}{\cdot} X$
43	42	eqeq2d	$⊢ n = {inv}_{r} (S) (m) \to (Y = n \underset{˙}{\cdot} X \leftrightarrow Y = {inv}_{r} (S) (m) \underset{˙}{\cdot} X)$
44	43	adantl	$⊢ ((((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \land n = {inv}_{r} (S) (m)) \to (Y = n \underset{˙}{\cdot} X \leftrightarrow Y = {inv}_{r} (S) (m) \underset{˙}{\cdot} X)$
45		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$
46		nelsn	$⊢ m \neq 0_{S} \to \neg m \in \{0_{S}\}$
47	38 46	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}\}$
48	15 47	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}\})$
49		eldifi	$⊢ X \in ({Base}_{V} ∖ \{0_{V}\}) \to X \in {Base}_{V}$
50	49 2	eleq2s	$⊢ X \in B \to X \in {Base}_{V}$
51	6 17 50	3syl	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to X \in {Base}_{V}$
52	32 4 3 5 33 39 12 48 51 30	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)$
53	45 52	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$
54	41 44 53	rspcedvd	$⊢ (((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$
55	1	prjsprel	$⊢ Y \underset{˙}{\sim} X \leftrightarrow ((Y \in B \land X \in B) \land \exists n \in K Y = n \underset{˙}{\cdot} X)$
56	11 54 55	sylanbrc	$⊢ (((V \in LVec \land X \underset{˙}{\sim} Y) \land m \in K) \land X = m \underset{˙}{\cdot} Y) \to Y \underset{˙}{\sim} X$
57		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$
58	7 57	sylbi	$⊢ X \underset{˙}{\sim} Y \to \exists m \in K X = m \underset{˙}{\cdot} Y$
59	58	adantl	$⊢ (V \in LVec \land X \underset{˙}{\sim} Y) \to \exists m \in K X = m \underset{˙}{\cdot} Y$
60	56 59	r19.29a	$⊢ (V \in LVec \land X \underset{˙}{\sim} Y) \to Y \underset{˙}{\sim} X$

Metamath Proof Explorer

Theorem prjspersym

Proof