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	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
	prjspnnorm.j	$⊢ J = (b \in B ⟼ inf (\{i \in (0 \dots N) \| b (i) \neq 0_{K}\} ℝ <))$
	prjspnnorm.f	$⊢ F = (v \in B ⟼ I (v (J (v))) \underset{˙}{\cdot} v)$
	prjspnnorm.w	$⊢ W = K freeLMod (0 \dots N)$
	prjspnnorm.b	$⊢ B = {Base}_{W} ∖ \{0_{W}\}$
	prjspnnorm.s	$⊢ S = {Base}_{K}$
	prjspnnorm.i	$⊢ I = {inv}_{r} (K)$
	prjspnnorm.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	prjspnnorm.k	$⊢ φ \to K \in DivRing$
	prjspnnorm.n	$⊢ φ \to N \in ℕ_{0}$
	prjspnnorm.x	$⊢ φ \to X \in B$
	prjspnnorm.y	$⊢ φ \to Y \in B$
Assertion	prjspnnorm	$⊢ φ \to (X \underset{˙}{\sim} Y \leftrightarrow F (X) = F (Y))$

Proof

Step	Hyp	Ref	Expression
1		prjspnnorm.e	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
2		prjspnnorm.j	$⊢ J = (b \in B ⟼ inf (\{i \in (0 \dots N) \| b (i) \neq 0_{K}\} ℝ <))$
3		prjspnnorm.f	$⊢ F = (v \in B ⟼ I (v (J (v))) \underset{˙}{\cdot} v)$
4		prjspnnorm.w	$⊢ W = K freeLMod (0 \dots N)$
5		prjspnnorm.b	$⊢ B = {Base}_{W} ∖ \{0_{W}\}$
6		prjspnnorm.s	$⊢ S = {Base}_{K}$
7		prjspnnorm.i	$⊢ I = {inv}_{r} (K)$
8		prjspnnorm.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
9		prjspnnorm.k	$⊢ φ \to K \in DivRing$
10		prjspnnorm.n	$⊢ φ \to N \in ℕ_{0}$
11		prjspnnorm.x	$⊢ φ \to X \in B$
12		prjspnnorm.y	$⊢ φ \to Y \in B$
13		ovexd	$⊢ φ \to (0 \dots N) \in V$
14	4	frlmsca	$⊢ (K \in DivRing \land (0 \dots N) \in V) \to K = Scalar (W)$
15	9 13 14	syl2anc	$⊢ φ \to K = Scalar (W)$
16	15	fveq2d	$⊢ φ \to {Base}_{K} = {Base}_{Scalar (W)}$
17	6 16	eqtrid	$⊢ φ \to S = {Base}_{Scalar (W)}$
18	17	rexeqdv	$⊢ φ \to (\exists l \in S x = l \underset{˙}{\cdot} y \leftrightarrow \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)$
19	18	anbi2d	$⊢ φ \to (((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y) \leftrightarrow ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y))$
20	19	opabbidv	$⊢ φ \to \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\}$
21	1 20	eqtrid	$⊢ φ \to \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\}$
22	21	breqd	$⊢ φ \to (X \underset{˙}{\sim} Y \leftrightarrow X \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\} Y)$
23	4	frlmlvec	$⊢ (K \in DivRing \land (0 \dots N) \in V) \to W \in LVec$
24	9 13 23	syl2anc	$⊢ φ \to W \in LVec$
25		eqid	$⊢ \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\}$
26		eqid	$⊢ Scalar (W) = Scalar (W)$
27		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
28		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
29	25 5 26 8 27 28	prjspreln0	$⊢ W \in LVec \to (X \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) X = m \underset{˙}{\cdot} Y))$
30	24 29	syl	$⊢ φ \to (X \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in {Base}_{Scalar (W)} x = l \underset{˙}{\cdot} y)\} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) X = m \underset{˙}{\cdot} Y))$
31	22 30	bitrd	$⊢ φ \to (X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) X = m \underset{˙}{\cdot} Y))$
32	31	simplbda	$⊢ (φ \land X \underset{˙}{\sim} Y) \to \exists m \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) X = m \underset{˙}{\cdot} Y$
33		eldifsn	$⊢ m \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \leftrightarrow (m \in {Base}_{Scalar (W)} \land m \neq 0_{Scalar (W)})$
34	17	eqcomd	$⊢ φ \to {Base}_{Scalar (W)} = S$
35	34	eleq2d	$⊢ φ \to (m \in {Base}_{Scalar (W)} \leftrightarrow m \in S)$
36	15	eqcomd	$⊢ φ \to Scalar (W) = K$
37	36	fveq2d	$⊢ φ \to 0_{Scalar (W)} = 0_{K}$
38	37	neeq2d	$⊢ φ \to (m \neq 0_{Scalar (W)} \leftrightarrow m \neq 0_{K})$
39	35 38	anbi12d	$⊢ φ \to ((m \in {Base}_{Scalar (W)} \land m \neq 0_{Scalar (W)}) \leftrightarrow (m \in S \land m \neq 0_{K}))$
40	33 39	bitrid	$⊢ φ \to (m \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \leftrightarrow (m \in S \land m \neq 0_{K}))$
41		eqid	$⊢ {Base}_{W} = {Base}_{W}$
42		eqid	$⊢ \cdot_{Scalar (W)} = \cdot_{Scalar (W)}$
43	24	lveclmodd	$⊢ φ \to W \in LMod$
44	43	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to W \in LMod$
45		eqid	$⊢ 0_{K} = 0_{K}$
46	9	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to K \in DivRing$
47	9	drngringd	$⊢ φ \to K \in Ring$
48	47	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to K \in Ring$
49	10	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to N \in ℕ_{0}$
50		simprl	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to m \in S$
51		difss	$⊢ {Base}_{W} ∖ \{0_{W}\} \subseteq {Base}_{W}$
52	5 51	eqsstri	$⊢ B \subseteq {Base}_{W}$
53	52 12	sselid	$⊢ φ \to Y \in {Base}_{W}$
54	53	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to Y \in {Base}_{W}$
55	4 41 6 8 48 50 54	frlmvscl	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to m \underset{˙}{\cdot} Y \in {Base}_{W}$
56		simprr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to m \neq 0_{K}$
57	15	fveq2d	$⊢ φ \to 0_{K} = 0_{Scalar (W)}$
58	57	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to 0_{K} = 0_{Scalar (W)}$
59	56 58	neeqtrd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to m \neq 0_{Scalar (W)}$
60	12 5	eleqtrdi	$⊢ φ \to Y \in ({Base}_{W} ∖ \{0_{W}\})$
61	60	eldifsnbd	$⊢ φ \to Y \neq 0_{W}$
62	61	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to Y \neq 0_{W}$
63		eqid	$⊢ 0_{W} = 0_{W}$
64	24	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to W \in LVec$
65	17	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to S = {Base}_{Scalar (W)}$
66	50 65	eleqtrd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to m \in {Base}_{Scalar (W)}$
67	41 8 26 27 28 63 64 66 54	lvecvsn0	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to (m \underset{˙}{\cdot} Y \neq 0_{W} \leftrightarrow (m \neq 0_{Scalar (W)} \land Y \neq 0_{W}))$
68	59 62 67	mpbir2and	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to m \underset{˙}{\cdot} Y \neq 0_{W}$
69	55 68	eldifsnd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to m \underset{˙}{\cdot} Y \in ({Base}_{W} ∖ \{0_{W}\})$
70	69 5	eleqtrrdi	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to m \underset{˙}{\cdot} Y \in B$
71	2 4 5 48 49 70 6	frlmnzcoordcl2	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to (m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y)) \in S$
72	2 4 5 48 49 70	frlmnzcoordn0	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to (m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y)) \neq 0_{K}$
73	6 45 7 46 71 72	drnginvrcld	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) \in S$
74	73 65	eleqtrd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) \in {Base}_{Scalar (W)}$
75	41 26 8 27 42 44 74 66 54	lmodvsassd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to (I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) \cdot_{Scalar (W)} m) \underset{˙}{\cdot} Y = I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) \underset{˙}{\cdot} (m \underset{˙}{\cdot} Y)$
76	36	fveq2d	$⊢ φ \to \cdot_{Scalar (W)} = \cdot_{K}$
77	76	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to \cdot_{Scalar (W)} = \cdot_{K}$
78	12	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to Y \in B$
79	2 4 5 8 45 6 46 49 78 50 56	frlmnzcoordsca	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to J (m \underset{˙}{\cdot} Y) = J (Y)$
80	79	fveq2d	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to (m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y)) = (m \underset{˙}{\cdot} Y) (J (Y))$
81		ovexd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to (0 \dots N) \in V$
82	2 4 5 47 10 12	frlmnzcoordcl	$⊢ φ \to J (Y) \in (0 \dots N)$
83	82	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to J (Y) \in (0 \dots N)$
84		eqid	$⊢ \cdot_{K} = \cdot_{K}$
85	4 41 6 81 50 54 83 8 84	frlmvscaval	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to (m \underset{˙}{\cdot} Y) (J (Y)) = m \cdot_{K} Y (J (Y))$
86	80 85	eqtrd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to (m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y)) = m \cdot_{K} Y (J (Y))$
87	86	fveq2d	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) = I (m \cdot_{K} Y (J (Y)))$
88	2 4 5 47 10 12 6	frlmnzcoordcl2	$⊢ φ \to Y (J (Y)) \in S$
89	88	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to Y (J (Y)) \in S$
90	2 4 5 47 10 12	frlmnzcoordn0	$⊢ φ \to Y (J (Y)) \neq 0_{K}$
91	90	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to Y (J (Y)) \neq 0_{K}$
92	6 45 84 7 46 50 89 56 91	drnginvmuld	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I (m \cdot_{K} Y (J (Y))) = I (Y (J (Y))) \cdot_{K} I (m)$
93	87 92	eqtrd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) = I (Y (J (Y))) \cdot_{K} I (m)$
94		eqidd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to m = m$
95	77 93 94	oveq123d	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) \cdot_{Scalar (W)} m = (I (Y (J (Y))) \cdot_{K} I (m)) \cdot_{K} m$
96	6 45 7 9 88 90	drnginvrcld	$⊢ φ \to I (Y (J (Y))) \in S$
97	96	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I (Y (J (Y))) \in S$
98	6 45 7 46 50 56	drnginvrcld	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I (m) \in S$
99	6 84 48 97 98 50	ringassd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to (I (Y (J (Y))) \cdot_{K} I (m)) \cdot_{K} m = I (Y (J (Y))) \cdot_{K} (I (m) \cdot_{K} m)$
100		eqid	$⊢ 1_{K} = 1_{K}$
101	6 45 84 100 7 46 50 56	drnginvrld	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I (m) \cdot_{K} m = 1_{K}$
102	101	oveq2d	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I (Y (J (Y))) \cdot_{K} (I (m) \cdot_{K} m) = I (Y (J (Y))) \cdot_{K} 1_{K}$
103	6 84 100 48 97	ringridmd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I (Y (J (Y))) \cdot_{K} 1_{K} = I (Y (J (Y)))$
104	102 103	eqtrd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I (Y (J (Y))) \cdot_{K} (I (m) \cdot_{K} m) = I (Y (J (Y)))$
105	95 99 104	3eqtrd	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) \cdot_{Scalar (W)} m = I (Y (J (Y)))$
106	105	oveq1d	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to (I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) \cdot_{Scalar (W)} m) \underset{˙}{\cdot} Y = I (Y (J (Y))) \underset{˙}{\cdot} Y$
107	75 106	eqtr3d	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) \underset{˙}{\cdot} (m \underset{˙}{\cdot} Y) = I (Y (J (Y))) \underset{˙}{\cdot} Y$
108	3 70	prjspnnormval	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to F (m \underset{˙}{\cdot} Y) = I ((m \underset{˙}{\cdot} Y) (J (m \underset{˙}{\cdot} Y))) \underset{˙}{\cdot} (m \underset{˙}{\cdot} Y)$
109	3 12	prjspnnormval	$⊢ φ \to F (Y) = I (Y (J (Y))) \underset{˙}{\cdot} Y$
110	109	adantr	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to F (Y) = I (Y (J (Y))) \underset{˙}{\cdot} Y$
111	107 108 110	3eqtr4d	$⊢ (φ \land (m \in S \land m \neq 0_{K})) \to F (m \underset{˙}{\cdot} Y) = F (Y)$
112	40 111	sylbida	$⊢ (φ \land m \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to F (m \underset{˙}{\cdot} Y) = F (Y)$
113		fveqeq2	$⊢ X = m \underset{˙}{\cdot} Y \to (F (X) = F (Y) \leftrightarrow F (m \underset{˙}{\cdot} Y) = F (Y))$
114	112 113	syl5ibrcom	$⊢ (φ \land m \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})) \to (X = m \underset{˙}{\cdot} Y \to F (X) = F (Y))$
115	114	impr	$⊢ (φ \land (m \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \land X = m \underset{˙}{\cdot} Y)) \to F (X) = F (Y)$
116	115	adantlr	$⊢ ((φ \land X \underset{˙}{\sim} Y) \land (m \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \land X = m \underset{˙}{\cdot} Y)) \to F (X) = F (Y)$
117	32 116	rexlimddv	$⊢ (φ \land X \underset{˙}{\sim} Y) \to F (X) = F (Y)$
118	1 4 5 6 8 9	prjspner	$⊢ φ \to \underset{˙}{\sim} Er B$
119	118	adantr	$⊢ (φ \land F (X) = F (Y)) \to \underset{˙}{\sim} Er B$
120	1 2 3 4 5 6 7 8 9 10 11	prjspnequivnorm	$⊢ φ \to X \underset{˙}{\sim} F (X)$
121	120	adantr	$⊢ (φ \land F (X) = F (Y)) \to X \underset{˙}{\sim} F (X)$
122	1 2 3 4 5 6 7 8 9 10 12	prjspnequivnorm	$⊢ φ \to Y \underset{˙}{\sim} F (Y)$
123	122	adantr	$⊢ (φ \land F (X) = F (Y)) \to Y \underset{˙}{\sim} F (Y)$
124		simpr	$⊢ (φ \land F (X) = F (Y)) \to F (X) = F (Y)$
125	123 124	breqtrrd	$⊢ (φ \land F (X) = F (Y)) \to Y \underset{˙}{\sim} F (X)$
126	119 121 125	ertr4d	$⊢ (φ \land F (X) = F (Y)) \to X \underset{˙}{\sim} Y$
127	117 126	impbida	$⊢ φ \to (X \underset{˙}{\sim} Y \leftrightarrow F (X) = F (Y))$

Metamath Proof Explorer

Theorem prjspnnorm

Proof