Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 ∼ 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )