Theorem prjspner1

Description: Two vectors whose zeroth coordinate is nonzero are equivalent if and only if they have the same representative in the (n-1)-dimensional affine subspace { x_0 = 1 } . For example, vectors in 3D space whose x coordinate is nonzero are equivalent iff they intersect at the plane x = 1 at the same point (also see section header). (Contributed by SN, 13-Aug-2023)

	Ref	Expression
Hypotheses	prjspner01.e	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
	prjspner01.f	⊢ 𝐹 = ( 𝑏 ∈ 𝐵 ↦ if ( ( 𝑏 ‘ 0 ) = 0 , 𝑏 , ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) ) )
	prjspner01.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
	prjspner01.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
	prjspner01.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	prjspner01.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
	prjspner01.0	⊢ 0 = ( 0g ‘ 𝐾 )
	prjspner01.i	⊢ 𝐼 = ( invr ‘ 𝐾 )
	prjspner01.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
	prjspner01.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	prjspner01.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	prjspner1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	prjspner1.1	⊢ ( 𝜑 → ( 𝑋 ‘ 0 ) ≠ 0 )
	prjspner1.2	⊢ ( 𝜑 → ( 𝑌 ‘ 0 ) ≠ 0 )
Assertion	prjspner1	⊢ ( 𝜑 → ( 𝑋 ∼ 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prjspner01.e	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
2		prjspner01.f	⊢ 𝐹 = ( 𝑏 ∈ 𝐵 ↦ if ( ( 𝑏 ‘ 0 ) = 0 , 𝑏 , ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) ) )
3		prjspner01.b	⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
4		prjspner01.w	⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
5		prjspner01.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		prjspner01.s	⊢ 𝑆 = ( Base ‘ 𝐾 )
7		prjspner01.0	⊢ 0 = ( 0g ‘ 𝐾 )
8		prjspner01.i	⊢ 𝐼 = ( invr ‘ 𝐾 )
9		prjspner01.k	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
10		prjspner01.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11		prjspner01.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
12		prjspner1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
13		prjspner1.1	⊢ ( 𝜑 → ( 𝑋 ‘ 0 ) ≠ 0 )
14		prjspner1.2	⊢ ( 𝜑 → ( 𝑌 ‘ 0 ) ≠ 0 )
15	1	prjsprel	⊢ ( 𝑋 ∼ 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) )
16		fveq1	⊢ ( 𝑋 = ( 0g ‘ 𝑊 ) → ( 𝑋 ‘ 0 ) = ( ( 0g ‘ 𝑊 ) ‘ 0 ) )
17	9	drngringd	⊢ ( 𝜑 → 𝐾 ∈ Ring )
18		ovexd	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
19		0elfz	⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
20	10 19	syl	⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
21	4 7 17 18 20	frlm0vald	⊢ ( 𝜑 → ( ( 0g ‘ 𝑊 ) ‘ 0 ) = 0 )
22	16 21	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑊 ) ) → ( 𝑋 ‘ 0 ) = 0 )
23	13 22	mteqand	⊢ ( 𝜑 → 𝑋 ≠ ( 0g ‘ 𝑊 ) )
24	4	frlmsca	⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝐾 = ( Scalar ‘ 𝑊 ) )
25	9 18 24	syl2anc	⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝑊 ) )
26	25	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
27	7 26	eqtrid	⊢ ( 𝜑 → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
28	27	oveq1d	⊢ ( 𝜑 → ( 0 · 𝑌 ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) · 𝑌 ) )
29	4	frlmlvec	⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝑊 ∈ LVec )
30	9 18 29	syl2anc	⊢ ( 𝜑 → 𝑊 ∈ LVec )
31	30	lveclmodd	⊢ ( 𝜑 → 𝑊 ∈ LMod )
32	12 3	eleqtrdi	⊢ ( 𝜑 → 𝑌 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
33	32	eldifad	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑊 ) )
34		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
35		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
36		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
37		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
38	34 35 5 36 37	lmod0vs	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) · 𝑌 ) = ( 0g ‘ 𝑊 ) )
39	31 33 38	syl2anc	⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) · 𝑌 ) = ( 0g ‘ 𝑊 ) )
40	28 39	eqtrd	⊢ ( 𝜑 → ( 0 · 𝑌 ) = ( 0g ‘ 𝑊 ) )
41	23 40	neeqtrrd	⊢ ( 𝜑 → 𝑋 ≠ ( 0 · 𝑌 ) )
42	41	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) → 𝑋 ≠ ( 0 · 𝑌 ) )
43		oveq1	⊢ ( 𝑚 = 0 → ( 𝑚 · 𝑌 ) = ( 0 · 𝑌 ) )
44	43	neeq2d	⊢ ( 𝑚 = 0 → ( 𝑋 ≠ ( 𝑚 · 𝑌 ) ↔ 𝑋 ≠ ( 0 · 𝑌 ) ) )
45	42 44	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) → ( 𝑚 = 0 → 𝑋 ≠ ( 𝑚 · 𝑌 ) ) )
46	45	necon2d	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) → ( 𝑋 = ( 𝑚 · 𝑌 ) → 𝑚 ≠ 0 ) )
47	46	ancrd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) → ( 𝑋 = ( 𝑚 · 𝑌 ) → ( 𝑚 ≠ 0 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) )
48		ovexd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( 0 ... 𝑁 ) ∈ V )
49		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → 𝑚 ∈ 𝑆 )
50	33	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → 𝑌 ∈ ( Base ‘ 𝑊 ) )
51	20	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → 0 ∈ ( 0 ... 𝑁 ) )
52		eqid	⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
53	4 34 6 48 49 50 51 5 52	frlmvscaval	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( 𝑚 · 𝑌 ) ‘ 0 ) = ( 𝑚 ( .r ‘ 𝐾 ) ( 𝑌 ‘ 0 ) ) )
54	53	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ 0 ) ) = ( 𝐼 ‘ ( 𝑚 ( .r ‘ 𝐾 ) ( 𝑌 ‘ 0 ) ) ) )
55	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → 𝐾 ∈ DivRing )
56	4 6 34	frlmbasf	⊢ ( ( ( 0 ... 𝑁 ) ∈ V ∧ 𝑌 ∈ ( Base ‘ 𝑊 ) ) → 𝑌 : ( 0 ... 𝑁 ) ⟶ 𝑆 )
57	18 33 56	syl2anc	⊢ ( 𝜑 → 𝑌 : ( 0 ... 𝑁 ) ⟶ 𝑆 )
58	57 20	ffvelcdmd	⊢ ( 𝜑 → ( 𝑌 ‘ 0 ) ∈ 𝑆 )
59	58	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( 𝑌 ‘ 0 ) ∈ 𝑆 )
60		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → 𝑚 ≠ 0 )
61	14	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( 𝑌 ‘ 0 ) ≠ 0 )
62	6 7 52 8 55 49 59 60 61	drnginvmuld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( 𝐼 ‘ ( 𝑚 ( .r ‘ 𝐾 ) ( 𝑌 ‘ 0 ) ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) )
63	54 62	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ 0 ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) )
64	63	oveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ 0 ) ) · ( 𝑚 · 𝑌 ) ) = ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) · ( 𝑚 · 𝑌 ) ) )
65	31	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → 𝑊 ∈ LMod )
66	17	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → 𝐾 ∈ Ring )
67	6 7 8 55 59 61	drnginvrcld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ∈ 𝑆 )
68	6 7 8 55 49 60	drnginvrcld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( 𝐼 ‘ 𝑚 ) ∈ 𝑆 )
69	6 52 66 67 68	ringcld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ∈ 𝑆 )
70	25	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
71	6 70	eqtrid	⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
72	71	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
73	69 72	eleqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
74	49 72	eleqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
75		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
76		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
77	34 35 5 75 76	lmodvsass	⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑚 ) · 𝑌 ) = ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) · ( 𝑚 · 𝑌 ) ) )
78	65 73 74 50 77	syl13anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑚 ) · 𝑌 ) = ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) · ( 𝑚 · 𝑌 ) ) )
79	6 52 66 67 68 49	ringassd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ( .r ‘ 𝐾 ) 𝑚 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( ( 𝐼 ‘ 𝑚 ) ( .r ‘ 𝐾 ) 𝑚 ) ) )
80	55 48 24	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → 𝐾 = ( Scalar ‘ 𝑊 ) )
81	80	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( .r ‘ 𝐾 ) = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
82	81	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ( .r ‘ 𝐾 ) 𝑚 ) = ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑚 ) )
83		eqid	⊢ ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐾 )
84	6 7 52 83 8 55 49 60	drnginvrld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( 𝐼 ‘ 𝑚 ) ( .r ‘ 𝐾 ) 𝑚 ) = ( 1r ‘ 𝐾 ) )
85	84	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( ( 𝐼 ‘ 𝑚 ) ( .r ‘ 𝐾 ) 𝑚 ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) )
86	6 52 83 66 67	ringridmd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) = ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) )
87	85 86	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( ( 𝐼 ‘ 𝑚 ) ( .r ‘ 𝐾 ) 𝑚 ) ) = ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) )
88	79 82 87	3eqtr3d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑚 ) = ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) )
89	88	oveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑚 ) · 𝑌 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) )
90	64 78 89	3eqtr2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ 0 ) ) · ( 𝑚 · 𝑌 ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) )
91		fveq1	⊢ ( 𝑋 = ( 𝑚 · 𝑌 ) → ( 𝑋 ‘ 0 ) = ( ( 𝑚 · 𝑌 ) ‘ 0 ) )
92	91	fveq2d	⊢ ( 𝑋 = ( 𝑚 · 𝑌 ) → ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) = ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ 0 ) ) )
93		id	⊢ ( 𝑋 = ( 𝑚 · 𝑌 ) → 𝑋 = ( 𝑚 · 𝑌 ) )
94	92 93	oveq12d	⊢ ( 𝑋 = ( 𝑚 · 𝑌 ) → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) = ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ 0 ) ) · ( 𝑚 · 𝑌 ) ) )
95	94	eqeq1d	⊢ ( 𝑋 = ( 𝑚 · 𝑌 ) → ( ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ↔ ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ 0 ) ) · ( 𝑚 · 𝑌 ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) )
96	90 95	syl5ibrcom	⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑚 ≠ 0 ) → ( 𝑋 = ( 𝑚 · 𝑌 ) → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) )
97	96	expimpd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) → ( ( 𝑚 ≠ 0 ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) )
98	47 97	syld	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑚 ∈ 𝑆 ) → ( 𝑋 = ( 𝑚 · 𝑌 ) → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) )
99	98	rexlimdva	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) )
100	99	impr	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) )
101	13	neneqd	⊢ ( 𝜑 → ¬ ( 𝑋 ‘ 0 ) = 0 )
102	101	iffalsed	⊢ ( 𝜑 → if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) = ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) )
103	102	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) = ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) )
104	14	neneqd	⊢ ( 𝜑 → ¬ ( 𝑌 ‘ 0 ) = 0 )
105	104	iffalsed	⊢ ( 𝜑 → if ( ( 𝑌 ‘ 0 ) = 0 , 𝑌 , ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) )
106	105	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → if ( ( 𝑌 ‘ 0 ) = 0 , 𝑌 , ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) )
107	100 103 106	3eqtr4d	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) = if ( ( 𝑌 ‘ 0 ) = 0 , 𝑌 , ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) )
108		fveq1	⊢ ( 𝑏 = 𝑋 → ( 𝑏 ‘ 0 ) = ( 𝑋 ‘ 0 ) )
109	108	eqeq1d	⊢ ( 𝑏 = 𝑋 → ( ( 𝑏 ‘ 0 ) = 0 ↔ ( 𝑋 ‘ 0 ) = 0 ) )
110		id	⊢ ( 𝑏 = 𝑋 → 𝑏 = 𝑋 )
111	108	fveq2d	⊢ ( 𝑏 = 𝑋 → ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) = ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) )
112	111 110	oveq12d	⊢ ( 𝑏 = 𝑋 → ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) = ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) )
113	109 110 112	ifbieq12d	⊢ ( 𝑏 = 𝑋 → if ( ( 𝑏 ‘ 0 ) = 0 , 𝑏 , ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) ) = if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) )
114		simprll	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → 𝑋 ∈ 𝐵 )
115		ovexd	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ∈ V )
116	114 115	ifexd	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) ∈ V )
117	2 113 114 116	fvmptd3	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → ( 𝐹 ‘ 𝑋 ) = if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) )
118		fveq1	⊢ ( 𝑏 = 𝑌 → ( 𝑏 ‘ 0 ) = ( 𝑌 ‘ 0 ) )
119	118	eqeq1d	⊢ ( 𝑏 = 𝑌 → ( ( 𝑏 ‘ 0 ) = 0 ↔ ( 𝑌 ‘ 0 ) = 0 ) )
120		id	⊢ ( 𝑏 = 𝑌 → 𝑏 = 𝑌 )
121	118	fveq2d	⊢ ( 𝑏 = 𝑌 → ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) = ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) )
122	121 120	oveq12d	⊢ ( 𝑏 = 𝑌 → ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) )
123	119 120 122	ifbieq12d	⊢ ( 𝑏 = 𝑌 → if ( ( 𝑏 ‘ 0 ) = 0 , 𝑏 , ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) ) = if ( ( 𝑌 ‘ 0 ) = 0 , 𝑌 , ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) )
124		simprlr	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → 𝑌 ∈ 𝐵 )
125		ovexd	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ∈ V )
126	124 125	ifexd	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → if ( ( 𝑌 ‘ 0 ) = 0 , 𝑌 , ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) ∈ V )
127	2 123 124 126	fvmptd3	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → ( 𝐹 ‘ 𝑌 ) = if ( ( 𝑌 ‘ 0 ) = 0 , 𝑌 , ( ( 𝐼 ‘ ( 𝑌 ‘ 0 ) ) · 𝑌 ) ) )
128	107 117 127	3eqtr4d	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ 𝑆 𝑋 = ( 𝑚 · 𝑌 ) ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
129	15 128	sylan2b	⊢ ( ( 𝜑 ∧ 𝑋 ∼ 𝑌 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
130	1 4 3 6 5 9	prjspner	⊢ ( 𝜑 → ∼ Er 𝐵 )
131	130	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → ∼ Er 𝐵 )
132	1 2 3 4 5 6 7 8 9 10 11	prjspner01	⊢ ( 𝜑 → 𝑋 ∼ ( 𝐹 ‘ 𝑋 ) )
133	132	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → 𝑋 ∼ ( 𝐹 ‘ 𝑋 ) )
134	130 132	ercl2	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
135	134	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
136	131 135	erref	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) ∼ ( 𝐹 ‘ 𝑋 ) )
137		breq2	⊢ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → ( ( 𝐹 ‘ 𝑋 ) ∼ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) ∼ ( 𝐹 ‘ 𝑌 ) ) )
138	137	adantl	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∼ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) ∼ ( 𝐹 ‘ 𝑌 ) ) )
139	136 138	mpbid	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) ∼ ( 𝐹 ‘ 𝑌 ) )
140	1 2 3 4 5 6 7 8 9 10 12	prjspner01	⊢ ( 𝜑 → 𝑌 ∼ ( 𝐹 ‘ 𝑌 ) )
141	140	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → 𝑌 ∼ ( 𝐹 ‘ 𝑌 ) )
142	131 139 141	ertr4d	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) ∼ 𝑌 )
143	131 133 142	ertrd	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → 𝑋 ∼ 𝑌 )
144	129 143	impbida	⊢ ( 𝜑 → ( 𝑋 ∼ 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )