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		sneq	$⊢ n = X (0) \to \{n\} = \{X (0)\}$
11	10	xpeq2d	$⊢ n = X (0) \to (0 \dots 0) \times \{n\} = (0 \dots 0) \times \{X (0)\}$
12	11	eqeq2d	$⊢ n = X (0) \to (X = (0 \dots 0) \times \{n\} \leftrightarrow X = (0 \dots 0) \times \{X (0)\})$
13		ovexd	$⊢ (K \in DivRing \land X \in B) \to (0 \dots 0) \in V$
14		difss	$⊢ {Base}_{W} ∖ \{0_{W}\} \subseteq {Base}_{W}$
15	2 14	eqsstri	$⊢ B \subseteq {Base}_{W}$
16	15	sseli	$⊢ X \in B \to X \in {Base}_{W}$
17	16	adantl	$⊢ (K \in DivRing \land X \in B) \to X \in {Base}_{W}$
18		eqid	$⊢ {Base}_{K} = {Base}_{K}$
19		eqid	$⊢ {Base}_{W} = {Base}_{W}$
20	5 18 19	frlmbasf	$⊢ ((0 \dots 0) \in V \land X \in {Base}_{W}) \to X : (0 \dots 0) ⟶ {Base}_{K}$
21	13 17 20	syl2anc	$⊢ (K \in DivRing \land X \in B) \to X : (0 \dots 0) ⟶ {Base}_{K}$
22		c0ex	$⊢ 0 \in V$
23	22	snid	$⊢ 0 \in \{0\}$
24		fz0sn	$⊢ (0 \dots 0) = \{0\}$
25	23 24	eleqtrri	$⊢ 0 \in (0 \dots 0)$
26	25	a1i	$⊢ (K \in DivRing \land X \in B) \to 0 \in (0 \dots 0)$
27	21 26	ffvelcdmd	$⊢ (K \in DivRing \land X \in B) \to X (0) \in {Base}_{K}$
28	5 18 19	frlmbasmap	$⊢ ((0 \dots 0) \in V \land X \in {Base}_{W}) \to X \in ({Base}_{K}^{(0 \dots 0)})$
29	13 17 28	syl2anc	$⊢ (K \in DivRing \land X \in B) \to X \in ({Base}_{K}^{(0 \dots 0)})$
30		fvex	$⊢ {Base}_{K} \in V$
31	24 30 22	mapsnconst	$⊢ X \in ({Base}_{K}^{(0 \dots 0)}) \to X = (0 \dots 0) \times \{X (0)\}$
32	29 31	syl	$⊢ (K \in DivRing \land X \in B) \to X = (0 \dots 0) \times \{X (0)\}$
33	12 27 32	rspcedvdw	$⊢ (K \in DivRing \land X \in B) \to \exists n \in {Base}_{K} X = (0 \dots 0) \times \{n\}$
34		oveq1	$⊢ m = n \to m \underset{˙}{\cdot} \underset{˙}{1} = n \underset{˙}{\cdot} \underset{˙}{1}$
35	34	eqeq2d	$⊢ m = n \to (X = m \underset{˙}{\cdot} \underset{˙}{1} \leftrightarrow X = n \underset{˙}{\cdot} \underset{˙}{1})$
36		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}$
37	36 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$
38		ovexd	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to (0 \dots 0) \in V$
39		simpr	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to n \in {Base}_{K}$
40	8	ad2antrr	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \underset{˙}{1} \in B$
41	15 40	sselid	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \underset{˙}{1} \in {Base}_{W}$
42		eqid	$⊢ \cdot_{K} = \cdot_{K}$
43	5 19 18 38 39 41 3 42	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}$
44	5 18 19	frlmbasf	$⊢ ((0 \dots 0) \in V \land \underset{˙}{1} \in {Base}_{W}) \to \underset{˙}{1} : (0 \dots 0) ⟶ {Base}_{K}$
45	38 41 44	syl2anc	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \underset{˙}{1} : (0 \dots 0) ⟶ {Base}_{K}$
46		drngring	$⊢ K \in DivRing \to K \in Ring$
47		eqid	$⊢ 1_{K} = 1_{K}$
48	18 47	ringidcl	$⊢ K \in Ring \to 1_{K} \in {Base}_{K}$
49	46 48	syl	$⊢ K \in DivRing \to 1_{K} \in {Base}_{K}$
50	49	ad2antrr	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to 1_{K} \in {Base}_{K}$
51	50	snssd	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \{1_{K}\} \subseteq {Base}_{K}$
52	6	a1i	$⊢ d \in (0 \dots 0) \to \underset{˙}{1} = (K unitVec (0 \dots 0)) (0)$
53		elfz1eq	$⊢ d \in (0 \dots 0) \to d = 0$
54	52 53	fveq12d	$⊢ d \in (0 \dots 0) \to \underset{˙}{1} (d) = (K unitVec (0 \dots 0)) (0) (0)$
55	54	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)$
56		eqid	$⊢ K unitVec (0 \dots 0) = K unitVec (0 \dots 0)$
57		simplll	$⊢ (((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \land d \in (0 \dots 0)) \to K \in DivRing$
58		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$
59	25	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)$
60	56 57 58 59 47	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}$
61		fvex	$⊢ (K unitVec (0 \dots 0)) (0) (0) \in V$
62	61	elsn	$⊢ (K unitVec (0 \dots 0)) (0) (0) \in \{1_{K}\} \leftrightarrow (K unitVec (0 \dots 0)) (0) (0) = 1_{K}$
63	60 62	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}\}$
64	55 63	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}\}$
65	64	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}\}$
66		fcdmssb	$⊢ (\{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}\})$
67	51 65 66	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}\})$
68	45 67	mpbid	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to \underset{˙}{1} : (0 \dots 0) ⟶ \{1_{K}\}$
69		vex	$⊢ n \in V$
70	69	a1i	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to n \in V$
71		elsni	$⊢ c \in \{1_{K}\} \to c = 1_{K}$
72	71	oveq2d	$⊢ c \in \{1_{K}\} \to n \cdot_{K} c = n \cdot_{K} 1_{K}$
73	46	ad2antrr	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to K \in Ring$
74	18 42 47 73 39	ringridmd	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to n \cdot_{K} 1_{K} = n$
75	72 74	sylan9eqr	$⊢ (((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \land c \in \{1_{K}\}) \to n \cdot_{K} c = n$
76	38 68 70 70 75	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\}$
77	43 76	eqtrd	$⊢ ((K \in DivRing \land X \in B) \land n \in {Base}_{K}) \to n \underset{˙}{\cdot} \underset{˙}{1} = (0 \dots 0) \times \{n\}$
78	77	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\})$
79	78	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})$
80	79	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}$
81	35 37 80	rspcedvdw	$⊢ ((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}$
82	33 81	rexlimddv	$⊢ (K \in DivRing \land X \in B) \to \exists m \in S X = m \underset{˙}{\cdot} \underset{˙}{1}$
83	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})$
84	7 9 82 83	syl21anbrc	$⊢ (K \in DivRing \land X \in B) \to X \underset{˙}{\sim} \underset{˙}{1}$

Metamath Proof Explorer

Theorem 0prjspnrel

Proof