Metamath Proof Explorer

Theorem prjspnnorm

Description: In a free module, two nonzero vectors are equivalent iff they have the same normalized representative. (Contributed by SN, 24-Sep-2026)

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

Proof

Step Hyp Ref Expression
1 prjspnnorm.e ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
2 prjspnnorm.j ⊢ 𝐽 = ( 𝑏 ∈ 𝐵 ↦ inf ( { 𝑖 ∈ ( 0 ... 𝑁 ) ∣ ( 𝑏 ‘ 𝑖 ) ≠ ( 0g ‘ 𝐾 ) } , ℝ , < ) )
3 prjspnnorm.f ⊢ 𝐹 = ( 𝑣 ∈ 𝐵 ↦ ( ( 𝐼 ‘ ( 𝑣 ‘ ( 𝐽 ‘ 𝑣 ) ) ) · 𝑣 ) )
4 prjspnnorm.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
5 prjspnnorm.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
6 prjspnnorm.s ⊢ 𝑆 = ( Base ‘ 𝐾 )
7 prjspnnorm.i ⊢ 𝐼 = ( invr ‘ 𝐾 )
8 prjspnnorm.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
9 prjspnnorm.k ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
10 prjspnnorm.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11 prjspnnorm.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
12 prjspnnorm.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
13 ovexd ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
14 4 frlmsca ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝐾 = ( Scalar ‘ 𝑊 ) )
15 9 13 14 syl2anc ⊢ ( 𝜑 → 𝐾 = ( Scalar ‘ 𝑊 ) )
16 15 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
17 6 16 eqtrid ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
18 17 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ↔ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) )
19 18 anbi2d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) ) )
20 19 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } )
21 1 20 eqtrid ⊢ ( 𝜑 → ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } )
22 21 breqd ⊢ ( 𝜑 → ( 𝑋 ∼ 𝑌 ↔ 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } 𝑌 ) )
23 4 frlmlvec ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝑊 ∈ LVec )
24 9 13 23 syl2anc ⊢ ( 𝜑 → 𝑊 ∈ LVec )
25 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) }
26 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
27 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
28 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
29 25 5 26 8 27 28 prjspreln0 ⊢ ( 𝑊 ∈ LVec → ( 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) ) )
30 24 29 syl ⊢ ( 𝜑 → ( 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) ) )
31 22 30 bitrd ⊢ ( 𝜑 → ( 𝑋 ∼ 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∃ 𝑚 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) 𝑋 = ( 𝑚 · 𝑌 ) ) ) )
32 31 simplbda ⊢ ( ( 𝜑 ∧ 𝑋 ∼ 𝑌 ) → ∃ 𝑚 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) 𝑋 = ( 𝑚 · 𝑌 ) )
33 eldifsn ⊢ ( 𝑚 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ↔ ( 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑚 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
34 17 eqcomd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = 𝑆 )
35 34 eleq2d ⊢ ( 𝜑 → ( 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↔ 𝑚 ∈ 𝑆 ) )
36 15 eqcomd ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) = 𝐾 )
37 36 fveq2d ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ 𝐾 ) )
38 37 neeq2d ⊢ ( 𝜑 → ( 𝑚 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) )
39 35 38 anbi12d ⊢ ( 𝜑 → ( ( 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑚 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) )
40 33 39 bitrid ⊢ ( 𝜑 → ( 𝑚 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ↔ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) )
41 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
42 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
43 24 lveclmodd ⊢ ( 𝜑 → 𝑊 ∈ LMod )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑊 ∈ LMod )
45 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
46 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝐾 ∈ DivRing )
47 9 drngringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
48 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝐾 ∈ Ring )
49 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑁 ∈ ℕ0 )
50 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑚 ∈ 𝑆 )
51 difss ⊢ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ⊆ ( Base ‘ 𝑊 )
52 5 51 eqsstri ⊢ 𝐵 ⊆ ( Base ‘ 𝑊 )
53 52 12 sselid ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑊 ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑌 ∈ ( Base ‘ 𝑊 ) )
55 4 41 6 8 48 50 54 frlmvscl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝑚 · 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
56 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑚 ≠ ( 0g ‘ 𝐾 ) )
57 15 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
58 57 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 0g ‘ 𝐾 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
59 56 58 neeqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑚 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
60 12 5 eleqtrdi ⊢ ( 𝜑 → 𝑌 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
61 60 eldifsnbd ⊢ ( 𝜑 → 𝑌 ≠ ( 0g ‘ 𝑊 ) )
62 61 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑌 ≠ ( 0g ‘ 𝑊 ) )
63 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
64 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑊 ∈ LVec )
65 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
66 50 65 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑚 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
67 41 8 26 27 28 63 64 66 54 lvecvsn0 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝑚 · 𝑌 ) ≠ ( 0g ‘ 𝑊 ) ↔ ( 𝑚 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ≠ ( 0g ‘ 𝑊 ) ) ) )
68 59 62 67 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝑚 · 𝑌 ) ≠ ( 0g ‘ 𝑊 ) )
69 55 68 eldifsnd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝑚 · 𝑌 ) ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
70 69 5 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝑚 · 𝑌 ) ∈ 𝐵 )
71 2 4 5 48 49 70 6 frlmnzcoordcl2 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ∈ 𝑆 )
72 2 4 5 48 49 70 frlmnzcoordn0 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ≠ ( 0g ‘ 𝐾 ) )
73 6 45 7 46 71 72 drnginvrcld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) ∈ 𝑆 )
74 73 65 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
75 41 26 8 27 42 44 74 66 54 lmodvsassd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑚 ) · 𝑌 ) = ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) · ( 𝑚 · 𝑌 ) ) )
76 36 fveq2d ⊢ ( 𝜑 → ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ 𝐾 ) )
77 76 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ 𝐾 ) )
78 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑌 ∈ 𝐵 )
79 2 4 5 8 45 6 46 49 78 50 56 frlmnzcoordsca ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) = ( 𝐽 ‘ 𝑌 ) )
80 79 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) = ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ 𝑌 ) ) )
81 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 0 ... 𝑁 ) ∈ V )
82 2 4 5 47 10 12 frlmnzcoordcl ⊢ ( 𝜑 → ( 𝐽 ‘ 𝑌 ) ∈ ( 0 ... 𝑁 ) )
83 82 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐽 ‘ 𝑌 ) ∈ ( 0 ... 𝑁 ) )
84 eqid ⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
85 4 41 6 81 50 54 83 8 84 frlmvscaval ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ 𝑌 ) ) = ( 𝑚 ( .r ‘ 𝐾 ) ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) )
86 80 85 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) = ( 𝑚 ( .r ‘ 𝐾 ) ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) )
87 86 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) = ( 𝐼 ‘ ( 𝑚 ( .r ‘ 𝐾 ) ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ) )
88 2 4 5 47 10 12 6 frlmnzcoordcl2 ⊢ ( 𝜑 → ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ∈ 𝑆 )
89 88 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ∈ 𝑆 )
90 2 4 5 47 10 12 frlmnzcoordn0 ⊢ ( 𝜑 → ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ≠ ( 0g ‘ 𝐾 ) )
91 90 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ≠ ( 0g ‘ 𝐾 ) )
92 6 45 84 7 46 50 89 56 91 drnginvmuld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐼 ‘ ( 𝑚 ( .r ‘ 𝐾 ) ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) )
93 87 92 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) )
94 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → 𝑚 = 𝑚 )
95 77 93 94 oveq123d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑚 ) = ( ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ( .r ‘ 𝐾 ) 𝑚 ) )
96 6 45 7 9 88 90 drnginvrcld ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ∈ 𝑆 )
97 96 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ∈ 𝑆 )
98 6 45 7 46 50 56 drnginvrcld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐼 ‘ 𝑚 ) ∈ 𝑆 )
99 6 84 48 97 98 50 ringassd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ( .r ‘ 𝐾 ) ( 𝐼 ‘ 𝑚 ) ) ( .r ‘ 𝐾 ) 𝑚 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ( .r ‘ 𝐾 ) ( ( 𝐼 ‘ 𝑚 ) ( .r ‘ 𝐾 ) 𝑚 ) ) )
100 eqid ⊢ ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐾 )
101 6 45 84 100 7 46 50 56 drnginvrld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝐼 ‘ 𝑚 ) ( .r ‘ 𝐾 ) 𝑚 ) = ( 1r ‘ 𝐾 ) )
102 101 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ( .r ‘ 𝐾 ) ( ( 𝐼 ‘ 𝑚 ) ( .r ‘ 𝐾 ) 𝑚 ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) )
103 6 84 100 48 97 ringridmd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ( .r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ) = ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) )
104 102 103 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) ( .r ‘ 𝐾 ) ( ( 𝐼 ‘ 𝑚 ) ( .r ‘ 𝐾 ) 𝑚 ) ) = ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) )
105 95 99 104 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑚 ) = ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) )
106 105 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑚 ) · 𝑌 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) · 𝑌 ) )
107 75 106 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) · ( 𝑚 · 𝑌 ) ) = ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) · 𝑌 ) )
108 3 70 prjspnnormval ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐹 ‘ ( 𝑚 · 𝑌 ) ) = ( ( 𝐼 ‘ ( ( 𝑚 · 𝑌 ) ‘ ( 𝐽 ‘ ( 𝑚 · 𝑌 ) ) ) ) · ( 𝑚 · 𝑌 ) ) )
109 3 12 prjspnnormval ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) · 𝑌 ) )
110 109 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐹 ‘ 𝑌 ) = ( ( 𝐼 ‘ ( 𝑌 ‘ ( 𝐽 ‘ 𝑌 ) ) ) · 𝑌 ) )
111 107 108 110 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑚 ≠ ( 0g ‘ 𝐾 ) ) ) → ( 𝐹 ‘ ( 𝑚 · 𝑌 ) ) = ( 𝐹 ‘ 𝑌 ) )
112 40 111 sylbida ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝐹 ‘ ( 𝑚 · 𝑌 ) ) = ( 𝐹 ‘ 𝑌 ) )
113 fveqeq2 ⊢ ( 𝑋 = ( 𝑚 · 𝑌 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( 𝑚 · 𝑌 ) ) = ( 𝐹 ‘ 𝑌 ) ) )
114 112 113 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝑋 = ( 𝑚 · 𝑌 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )
115 114 impr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
116 115 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∼ 𝑌 ) ∧ ( 𝑚 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∧ 𝑋 = ( 𝑚 · 𝑌 ) ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
117 32 116 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑋 ∼ 𝑌 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
118 1 4 5 6 8 9 prjspner ⊢ ( 𝜑 → ∼ Er 𝐵 )
119 118 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → ∼ Er 𝐵 )
120 1 2 3 4 5 6 7 8 9 10 11 prjspnequivnorm ⊢ ( 𝜑 → 𝑋 ∼ ( 𝐹 ‘ 𝑋 ) )
121 120 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → 𝑋 ∼ ( 𝐹 ‘ 𝑋 ) )
122 1 2 3 4 5 6 7 8 9 10 12 prjspnequivnorm ⊢ ( 𝜑 → 𝑌 ∼ ( 𝐹 ‘ 𝑌 ) )
123 122 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → 𝑌 ∼ ( 𝐹 ‘ 𝑌 ) )
124 simpr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
125 123 124 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → 𝑌 ∼ ( 𝐹 ‘ 𝑋 ) )
126 119 121 125 ertr4d ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → 𝑋 ∼ 𝑌 )
127 117 126 impbida ⊢ ( 𝜑 → ( 𝑋 ∼ 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )