0prjspnrel

Description: In the zero-dimensional projective space, all vectors are equivalent to the unit vector. (Contributed by Steven Nguyen, 7-Jun-2023)

	Ref	Expression
Hypotheses	0prjspnrel.e	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
	0prjspnrel.b	$⊢ B = {Base}_{W} ∖ \{0_{W}\}$
	0prjspnrel.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	0prjspnrel.s	$⊢ S = {Base}_{K}$
	0prjspnrel.w	$⊢ W = K freeLMod (0 \dots 0)$
	0prjspnrel.1	$⊢ \underset{˙}{1} = (K unitVec (0 \dots 0)) (0)$
Assertion	0prjspnrel	$⊢ (K \in DivRing \land X \in B) \to X \underset{˙}{\sim} \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		0prjspnrel.e	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
2		0prjspnrel.b	$⊢ B = {Base}_{W} ∖ \{0_{W}\}$
3		0prjspnrel.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		0prjspnrel.s	$⊢ S = {Base}_{K}$
5		0prjspnrel.w	$⊢ W = K freeLMod (0 \dots 0)$
6		0prjspnrel.1	$⊢ \underset{˙}{1} = (K unitVec (0 \dots 0)) (0)$
7		simpr	$⊢ (K \in DivRing \land X \in B) \to X \in B$
8	2 5 6	0prjspnlem	$⊢ K \in DivRing \to \underset{˙}{1} \in B$
9	8	adantr	$⊢ (K \in DivRing \land X \in B) \to \underset{˙}{1} \in B$
10		ovexd	$⊢ (K \in DivRing \land X \in B) \to (0 \dots 0) \in V$
11		difss	$⊢ {Base}_{W} ∖ \{0_{W}\} \subseteq {Base}_{W}$
12	2 11	eqsstri	$⊢ B \subseteq {Base}_{W}$
13	12	sseli	$⊢ X \in B \to X \in {Base}_{W}$
14	13	adantl	$⊢ (K \in DivRing \land X \in B) \to X \in {Base}_{W}$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16		eqid	$⊢ {Base}_{W} = {Base}_{W}$
17	5 15 16	frlmbasf	$⊢ ((0 \dots 0) \in V \land X \in {Base}_{W}) \to X : (0 \dots 0) ⟶ {Base}_{K}$
18	10 14 17	syl2anc	$⊢ (K \in DivRing \land X \in B) \to X : (0 \dots 0) ⟶ {Base}_{K}$
19		c0ex	$⊢ 0 \in V$
20	19	snid	$⊢ 0 \in \{0\}$
21		fz0sn	$⊢ (0 \dots 0) = \{0\}$
22	20 21	eleqtrri	$⊢ 0 \in (0 \dots 0)$
23	22	a1i	$⊢ (K \in DivRing \land X \in B) \to 0 \in (0 \dots 0)$
24	18 23	ffvelrnd	$⊢ (K \in DivRing \land X \in B) \to X (0) \in {Base}_{K}$
25		sneq	$⊢ n = X (0) \to \{n\} = \{X (0)\}$
26	25	xpeq2d	$⊢ n = X (0) \to (0 \dots 0) \times \{n\} = (0 \dots 0) \times \{X (0)\}$
27	26	eqeq2d	$⊢ n = X (0) \to (X = (0 \dots 0) \times \{n\} \leftrightarrow X = (0 \dots 0) \times \{X (0)\})$
28	27	adantl	$⊢ ((K \in DivRing \land X \in B) \land n = X (0)) \to (X = (0 \dots 0) \times \{n\} \leftrightarrow X = (0 \dots 0) \times \{X (0)\})$
29	5 15 16	frlmbasmap	$⊢ ((0 \dots 0) \in V \land X \in {Base}_{W}) \to X \in ({Base}_{K}^{(0 \dots 0)})$
30	10 14 29	syl2anc	$⊢ (K \in DivRing \land X \in B) \to X \in ({Base}_{K}^{(0 \dots 0)})$
31		fvex	$⊢ {Base}_{K} \in V$
32	21 31 19	mapsnconst	$⊢ X \in ({Base}_{K}^{(0 \dots 0)}) \to X = (0 \dots 0) \times \{X (0)\}$
33	30 32	syl	$⊢ (K \in DivRing \land X \in B) \to X = (0 \dots 0) \times \{X (0)\}$
34	24 28 33	rspcedvd	$⊢ (K \in DivRing \land X \in B) \to \exists n \in {Base}_{K} X = (0 \dots 0) \times \{n\}$
35		simprl	$⊢ ((K \in DivRing \land X \in B) \land (n \in {Base}_{K} \land X = (0 \dots 0) \times \{n\})) \to n \in {Base}_{K}$
36	35 4	eleqtrrdi	$⊢ ((K \in DivRing \land X \in B) \land (n \in {Base}_{K} \land X = (0 \dots 0) \times \{n\})) \to n \in S$
37		oveq1	$⊢ m = n \to m \underset{˙}{\cdot} \underset{˙}{1} = n \underset{˙}{\cdot} \underset{˙}{1}$
38	37	eqeq2d	$⊢ m = n \to (X = m \underset{˙}{\cdot} \underset{˙}{1} \leftrightarrow X = n \underset{˙}{\cdot} \underset{˙}{1})$
39	38	adantl	$⊢ (((K \in DivRing \land X \in B) \land (n \in {Base}_{K} \land X = (0 \dots 0) \times \{n\})) \land m = n) \to (X = m \underset{˙}{\cdot} \underset{˙}{1} \leftrightarrow X = n \underset{˙}{\cdot} \underset{˙}{1})$
40		ovexd	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to (0 \dots 0) \in V$
41		simpr	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to n \in {Base}_{K}$
42	8	ad2antrr	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \underset{˙}{1} \in B$
43	12 42	sselid	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \underset{˙}{1} \in {Base}_{W}$
44		eqid	$⊢ \cdot_{K} = \cdot_{K}$
45	5 16 15 40 41 43 3 44	frlmvscafval	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to n \underset{˙}{\cdot} \underset{˙}{1} = ((0 \dots 0) \times \{n\}) {\cdot_{K}}_{f} \underset{˙}{1}$
46	5 15 16	frlmbasf	$⊢ ((0 \dots 0) \in V \land \underset{˙}{1} \in {Base}_{W}) \to \underset{˙}{1} : (0 \dots 0) ⟶ {Base}_{K}$
47	40 43 46	syl2anc	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \underset{˙}{1} : (0 \dots 0) ⟶ {Base}_{K}$
48		drngring	$⊢ K \in DivRing \to K \in Ring$
49		eqid	$⊢ 1_{K} = 1_{K}$
50	15 49	ringidcl	$⊢ K \in Ring \to 1_{K} \in {Base}_{K}$
51	48 50	syl	$⊢ K \in DivRing \to 1_{K} \in {Base}_{K}$
52	51	ad2antrr	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to 1_{K} \in {Base}_{K}$
53	52	snssd	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \{1_{K}\} \subseteq {Base}_{K}$
54	6	a1i	$⊢ d \in (0 \dots 0) \to \underset{˙}{1} = (K unitVec (0 \dots 0)) (0)$
55		elfz1eq	$⊢ d \in (0 \dots 0) \to d = 0$
56	54 55	fveq12d	$⊢ d \in (0 \dots 0) \to \underset{˙}{1} (d) = (K unitVec (0 \dots 0)) (0) (0)$
57	56	adantl	$⊢ (((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \land d \in (0 \dots 0)) \to \underset{˙}{1} (d) = (K unitVec (0 \dots 0)) (0) (0)$
58		eqid	$⊢ K unitVec (0 \dots 0) = K unitVec (0 \dots 0)$
59		simplll	$⊢ (((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \land d \in (0 \dots 0)) \to K \in DivRing$
60		ovexd	$⊢ (((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \land d \in (0 \dots 0)) \to (0 \dots 0) \in V$
61	22	a1i	$⊢ (((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \land d \in (0 \dots 0)) \to 0 \in (0 \dots 0)$
62	58 59 60 61 49	uvcvv1	$⊢ (((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \land d \in (0 \dots 0)) \to (K unitVec (0 \dots 0)) (0) (0) = 1_{K}$
63		fvex	$⊢ (K unitVec (0 \dots 0)) (0) (0) \in V$
64	63	elsn	$⊢ (K unitVec (0 \dots 0)) (0) (0) \in \{1_{K}\} \leftrightarrow (K unitVec (0 \dots 0)) (0) (0) = 1_{K}$
65	62 64	sylibr	$⊢ (((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \land d \in (0 \dots 0)) \to (K unitVec (0 \dots 0)) (0) (0) \in \{1_{K}\}$
66	57 65	eqeltrd	$⊢ (((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \land d \in (0 \dots 0)) \to \underset{˙}{1} (d) \in \{1_{K}\}$
67	66	ralrimiva	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \forall d \in (0 \dots 0) \underset{˙}{1} (d) \in \{1_{K}\}$
68		frnssb	$⊢ (\{1_{K}\} \subseteq {Base}_{K} \land \forall d \in (0 \dots 0) \underset{˙}{1} (d) \in \{1_{K}\}) \to (\underset{˙}{1} : (0 \dots 0) ⟶ {Base}_{K} \leftrightarrow \underset{˙}{1} : (0 \dots 0) ⟶ \{1_{K}\})$
69	53 67 68	syl2anc	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to (\underset{˙}{1} : (0 \dots 0) ⟶ {Base}_{K} \leftrightarrow \underset{˙}{1} : (0 \dots 0) ⟶ \{1_{K}\})$
70	47 69	mpbid	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \underset{˙}{1} : (0 \dots 0) ⟶ \{1_{K}\}$
71		vex	$⊢ n \in V$
72	71	a1i	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to n \in V$
73		elsni	$⊢ c \in \{1_{K}\} \to c = 1_{K}$
74	73	oveq2d	$⊢ c \in \{1_{K}\} \to n \cdot_{K} c = n \cdot_{K} 1_{K}$
75	48	ad2antrr	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to K \in Ring$
76	15 44 49	ringridm	$⊢ (K \in Ring \land n \in {Base}_{K}) \to n \cdot_{K} 1_{K} = n$
77	75 41 76	syl2anc	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to n \cdot_{K} 1_{K} = n$
78	74 77	sylan9eqr	$⊢ (((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \land c \in \{1_{K}\}) \to n \cdot_{K} c = n$
79	40 70 72 72 78	caofid2	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to ((0 \dots 0) \times \{n\}) {\cdot_{K}}_{f} \underset{˙}{1} = (0 \dots 0) \times \{n\}$
80	45 79	eqtrd	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to n \underset{˙}{\cdot} \underset{˙}{1} = (0 \dots 0) \times \{n\}$
81	80	eqeq2d	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to (X = n \underset{˙}{\cdot} \underset{˙}{1} \leftrightarrow X = (0 \dots 0) \times \{n\})$
82	81	biimprd	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to (X = (0 \dots 0) \times \{n\} \to X = n \underset{˙}{\cdot} \underset{˙}{1})$
83	82	impr	$⊢ ((K \in DivRing \land X \in B) \land (n \in {Base}_{K} \land X = (0 \dots 0) \times \{n\})) \to X = n \underset{˙}{\cdot} \underset{˙}{1}$
84	36 39 83	rspcedvd	$⊢ ((K \in DivRing \land X \in B) \land (n \in {Base}_{K} \land X = (0 \dots 0) \times \{n\})) \to \exists m \in S X = m \underset{˙}{\cdot} \underset{˙}{1}$
85	34 84	rexlimddv	$⊢ (K \in DivRing \land X \in B) \to \exists m \in S X = m \underset{˙}{\cdot} \underset{˙}{1}$
86	1	prjsprel	$⊢ X \underset{˙}{\sim} \underset{˙}{1} \leftrightarrow ((X \in B \land \underset{˙}{1} \in B) \land \exists m \in S X = m \underset{˙}{\cdot} \underset{˙}{1})$
87	7 9 85 86	syl21anbrc	$⊢ (K \in DivRing \land X \in B) \to X \underset{˙}{\sim} \underset{˙}{1}$

Metamath Proof Explorer

Theorem 0prjspnrel

Proof