Theorem 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	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
	0prjspnrel.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
	0prjspnrel.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
	0prjspnrel.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
	0prjspnrel.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 0 ) )
	0prjspnrel.1	⊢ 1 = ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 )
Assertion	0prjspnrel	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∼ 1 )

Proof

Step	Hyp	Ref	Expression
1		0prjspnrel.e	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
2		0prjspnrel.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
3		0prjspnrel.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		0prjspnrel.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
5		0prjspnrel.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 0 ) )
6		0prjspnrel.1	⊢ 1 = ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 )
7		simpr	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
8	2 5 6	0prjspnlem	⊢ ( 𝐾 ∈ DivRing → 1 ∈ 𝐵 )
9	8	adantr	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 1 ∈ 𝐵 )
10		ovexd	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → ( 0 ... 0 ) ∈ V )
11		difss	⊢ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ⊆ ( Base ‘ 𝑊 )
12	2 11	eqsstri	⊢ 𝐵 ⊆ ( Base ‘ 𝑊 )
13	12	sseli	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
14	13	adantl	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
15		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
16		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
17	5 15 16	frlmbasf	⊢ ( ( ( 0 ... 0 ) ∈ V ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → 𝑋 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) )
18	10 14 17	syl2anc	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) )
19		c0ex	⊢ 0 ∈ V
20	19	snid	⊢ 0 ∈ { 0 }
21		fz0sn	⊢ ( 0 ... 0 ) = { 0 }
22	20 21	eleqtrri	⊢ 0 ∈ ( 0 ... 0 )
23	22	a1i	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ ( 0 ... 0 ) )
24	18 23	ffvelcdmd	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ‘ 0 ) ∈ ( Base ‘ 𝐾 ) )
25		sneq	⊢ ( 𝑛 = ( 𝑋 ‘ 0 ) → { 𝑛 } = { ( 𝑋 ‘ 0 ) } )
26	25	xpeq2d	⊢ ( 𝑛 = ( 𝑋 ‘ 0 ) → ( ( 0 ... 0 ) × { 𝑛 } ) = ( ( 0 ... 0 ) × { ( 𝑋 ‘ 0 ) } ) )
27	26	eqeq2d	⊢ ( 𝑛 = ( 𝑋 ‘ 0 ) → ( 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ↔ 𝑋 = ( ( 0 ... 0 ) × { ( 𝑋 ‘ 0 ) } ) ) )
28	27	adantl	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑋 ‘ 0 ) ) → ( 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ↔ 𝑋 = ( ( 0 ... 0 ) × { ( 𝑋 ‘ 0 ) } ) ) )
29	5 15 16	frlmbasmap	⊢ ( ( ( 0 ... 0 ) ∈ V ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → 𝑋 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 0 ) ) )
30	10 14 29	syl2anc	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 0 ) ) )
31		fvex	⊢ ( Base ‘ 𝐾 ) ∈ V
32	21 31 19	mapsnconst	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 0 ) ) → 𝑋 = ( ( 0 ... 0 ) × { ( 𝑋 ‘ 0 ) } ) )
33	30 32	syl	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 = ( ( 0 ... 0 ) × { ( 𝑋 ‘ 0 ) } ) )
34	24 28 33	rspcedvd	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑛 ∈ ( Base ‘ 𝐾 ) 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) )
35		simprl	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑛 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) ) → 𝑛 ∈ ( Base ‘ 𝐾 ) )
36	35 4	eleqtrrdi	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑛 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) ) → 𝑛 ∈ 𝑆 )
37		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 · 1 ) = ( 𝑛 · 1 ) )
38	37	eqeq2d	⊢ ( 𝑚 = 𝑛 → ( 𝑋 = ( 𝑚 · 1 ) ↔ 𝑋 = ( 𝑛 · 1 ) ) )
39	38	adantl	⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑛 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) ) ∧ 𝑚 = 𝑛 ) → ( 𝑋 = ( 𝑚 · 1 ) ↔ 𝑋 = ( 𝑛 · 1 ) ) )
40		ovexd	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 0 ... 0 ) ∈ V )
41		simpr	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 𝑛 ∈ ( Base ‘ 𝐾 ) )
42	8	ad2antrr	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 1 ∈ 𝐵 )
43	12 42	sselid	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 1 ∈ ( Base ‘ 𝑊 ) )
44		eqid	⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
45	5 16 15 40 41 43 3 44	frlmvscafval	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑛 · 1 ) = ( ( ( 0 ... 0 ) × { 𝑛 } ) ∘f ( .r ‘ 𝐾 ) 1 ) )
46	5 15 16	frlmbasf	⊢ ( ( ( 0 ... 0 ) ∈ V ∧ 1 ∈ ( Base ‘ 𝑊 ) ) → 1 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) )
47	40 43 46	syl2anc	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 1 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) )
48		drngring	⊢ ( 𝐾 ∈ DivRing → 𝐾 ∈ Ring )
49		eqid	⊢ ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐾 )
50	15 49	ringidcl	⊢ ( 𝐾 ∈ Ring → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
51	48 50	syl	⊢ ( 𝐾 ∈ DivRing → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
52	51	ad2antrr	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 1r ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
53	52	snssd	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → { ( 1r ‘ 𝐾 ) } ⊆ ( Base ‘ 𝐾 ) )
54	6	a1i	⊢ ( 𝑑 ∈ ( 0 ... 0 ) → 1 = ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) )
55		elfz1eq	⊢ ( 𝑑 ∈ ( 0 ... 0 ) → 𝑑 = 0 )
56	54 55	fveq12d	⊢ ( 𝑑 ∈ ( 0 ... 0 ) → ( 1 ‘ 𝑑 ) = ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) )
57	56	adantl	⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → ( 1 ‘ 𝑑 ) = ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) )
58		eqid	⊢ ( 𝐾 unitVec ( 0 ... 0 ) ) = ( 𝐾 unitVec ( 0 ... 0 ) )
59		simplll	⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → 𝐾 ∈ DivRing )
60		ovexd	⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → ( 0 ... 0 ) ∈ V )
61	22	a1i	⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → 0 ∈ ( 0 ... 0 ) )
62	58 59 60 61 49	uvcvv1	⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) = ( 1r ‘ 𝐾 ) )
63		fvex	⊢ ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) ∈ V
64	63	elsn	⊢ ( ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) ∈ { ( 1r ‘ 𝐾 ) } ↔ ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) = ( 1r ‘ 𝐾 ) )
65	62 64	sylibr	⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ‘ 0 ) ∈ { ( 1r ‘ 𝐾 ) } )
66	57 65	eqeltrd	⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑑 ∈ ( 0 ... 0 ) ) → ( 1 ‘ 𝑑 ) ∈ { ( 1r ‘ 𝐾 ) } )
67	66	ralrimiva	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ∀ 𝑑 ∈ ( 0 ... 0 ) ( 1 ‘ 𝑑 ) ∈ { ( 1r ‘ 𝐾 ) } )
68		fcdmssb	⊢ ( ( { ( 1r ‘ 𝐾 ) } ⊆ ( Base ‘ 𝐾 ) ∧ ∀ 𝑑 ∈ ( 0 ... 0 ) ( 1 ‘ 𝑑 ) ∈ { ( 1r ‘ 𝐾 ) } ) → ( 1 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) ↔ 1 : ( 0 ... 0 ) ⟶ { ( 1r ‘ 𝐾 ) } ) )
69	53 67 68	syl2anc	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 1 : ( 0 ... 0 ) ⟶ ( Base ‘ 𝐾 ) ↔ 1 : ( 0 ... 0 ) ⟶ { ( 1r ‘ 𝐾 ) } ) )
70	47 69	mpbid	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 1 : ( 0 ... 0 ) ⟶ { ( 1r ‘ 𝐾 ) } )
71		vex	⊢ 𝑛 ∈ V
72	71	a1i	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 𝑛 ∈ V )
73		elsni	⊢ ( 𝑐 ∈ { ( 1r ‘ 𝐾 ) } → 𝑐 = ( 1r ‘ 𝐾 ) )
74	73	oveq2d	⊢ ( 𝑐 ∈ { ( 1r ‘ 𝐾 ) } → ( 𝑛 ( .r ‘ 𝐾 ) 𝑐 ) = ( 𝑛 ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) )
75	48	ad2antrr	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ Ring )
76	15 44 49	ringridm	⊢ ( ( 𝐾 ∈ Ring ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑛 ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) = 𝑛 )
77	75 41 76	syl2anc	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑛 ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) = 𝑛 )
78	74 77	sylan9eqr	⊢ ( ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑐 ∈ { ( 1r ‘ 𝐾 ) } ) → ( 𝑛 ( .r ‘ 𝐾 ) 𝑐 ) = 𝑛 )
79	40 70 72 72 78	caofid2	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 0 ... 0 ) × { 𝑛 } ) ∘f ( .r ‘ 𝐾 ) 1 ) = ( ( 0 ... 0 ) × { 𝑛 } ) )
80	45 79	eqtrd	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑛 · 1 ) = ( ( 0 ... 0 ) × { 𝑛 } ) )
81	80	eqeq2d	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 = ( 𝑛 · 1 ) ↔ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) )
82	81	biimprd	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) → 𝑋 = ( 𝑛 · 1 ) ) )
83	82	impr	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑛 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) ) → 𝑋 = ( 𝑛 · 1 ) )
84	36 39 83	rspcedvd	⊢ ( ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑛 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 = ( ( 0 ... 0 ) × { 𝑛 } ) ) ) → ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 1 ) )
85	34 84	rexlimddv	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 1 ) )
86	1	prjsprel	⊢ ( 𝑋 ∼ 1 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 1 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 1 ) ) )
87	7 9 85 86	syl21anbrc	⊢ ( ( 𝐾 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∼ 1 )