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

Proof

Step	Hyp	Ref	Expression
1		prjspner01.e	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in S x = l \underset{˙}{\cdot} y)\}$
2		prjspner01.f	$⊢ F = (b \in B ⟼ if (b (0) = \underset{˙}{0}, b, I (b (0)) \underset{˙}{\cdot} b))$
3		prjspner01.b	$⊢ B = {Base}_{W} ∖ \{0_{W}\}$
4		prjspner01.w	$⊢ W = K freeLMod (0 \dots N)$
5		prjspner01.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		prjspner01.s	$⊢ S = {Base}_{K}$
7		prjspner01.0	$⊢ \underset{˙}{0} = 0_{K}$
8		prjspner01.i	$⊢ I = {inv}_{r} (K)$
9		prjspner01.k	$⊢ φ \to K \in DivRing$
10		prjspner01.n	$⊢ φ \to N \in ℕ_{0}$
11		prjspner01.x	$⊢ φ \to X \in B$
12		prjspner1.y	$⊢ φ \to Y \in B$
13		prjspner1.1	$⊢ φ \to X (0) \neq \underset{˙}{0}$
14		prjspner1.2	$⊢ φ \to Y (0) \neq \underset{˙}{0}$
15	1	prjsprel	$⊢ X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)$
16		fveq1	$⊢ X = 0_{W} \to X (0) = 0_{W} (0)$
17	9	drngringd	$⊢ φ \to K \in Ring$
18		ovexd	$⊢ φ \to (0 \dots N) \in V$
19		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
20	10 19	syl	$⊢ φ \to 0 \in (0 \dots N)$
21	4 7 17 18 20	frlm0vald	$⊢ φ \to 0_{W} (0) = \underset{˙}{0}$
22	16 21	sylan9eqr	$⊢ (φ \land X = 0_{W}) \to X (0) = \underset{˙}{0}$
23	13 22	mteqand	$⊢ φ \to X \neq 0_{W}$
24	4	frlmsca	$⊢ (K \in DivRing \land (0 \dots N) \in V) \to K = Scalar (W)$
25	9 18 24	syl2anc	$⊢ φ \to K = Scalar (W)$
26	25	fveq2d	$⊢ φ \to 0_{K} = 0_{Scalar (W)}$
27	7 26	syl5eq	$⊢ φ \to \underset{˙}{0} = 0_{Scalar (W)}$
28	27	oveq1d	$⊢ φ \to \underset{˙}{0} \underset{˙}{\cdot} Y = 0_{Scalar (W)} \underset{˙}{\cdot} Y$
29	4	frlmlvec	$⊢ (K \in DivRing \land (0 \dots N) \in V) \to W \in LVec$
30	9 18 29	syl2anc	$⊢ φ \to W \in LVec$
31	30	lveclmodd	$⊢ φ \to W \in LMod$
32	12 3	eleqtrdi	$⊢ φ \to Y \in ({Base}_{W} ∖ \{0_{W}\})$
33	32	eldifad	$⊢ φ \to Y \in {Base}_{W}$
34		eqid	$⊢ {Base}_{W} = {Base}_{W}$
35		eqid	$⊢ Scalar (W) = Scalar (W)$
36		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
37		eqid	$⊢ 0_{W} = 0_{W}$
38	34 35 5 36 37	lmod0vs	$⊢ (W \in LMod \land Y \in {Base}_{W}) \to 0_{Scalar (W)} \underset{˙}{\cdot} Y = 0_{W}$
39	31 33 38	syl2anc	$⊢ φ \to 0_{Scalar (W)} \underset{˙}{\cdot} Y = 0_{W}$
40	28 39	eqtrd	$⊢ φ \to \underset{˙}{0} \underset{˙}{\cdot} Y = 0_{W}$
41	23 40	neeqtrrd	$⊢ φ \to X \neq \underset{˙}{0} \underset{˙}{\cdot} Y$
42	41	ad2antrr	$⊢ ((φ \land (X \in B \land Y \in B)) \land m \in S) \to X \neq \underset{˙}{0} \underset{˙}{\cdot} Y$
43		oveq1	$⊢ m = \underset{˙}{0} \to m \underset{˙}{\cdot} Y = \underset{˙}{0} \underset{˙}{\cdot} Y$
44	43	neeq2d	$⊢ m = \underset{˙}{0} \to (X \neq m \underset{˙}{\cdot} Y \leftrightarrow X \neq \underset{˙}{0} \underset{˙}{\cdot} Y)$
45	42 44	syl5ibrcom	$⊢ ((φ \land (X \in B \land Y \in B)) \land m \in S) \to (m = \underset{˙}{0} \to X \neq m \underset{˙}{\cdot} Y)$
46	45	necon2d	$⊢ ((φ \land (X \in B \land Y \in B)) \land m \in S) \to (X = m \underset{˙}{\cdot} Y \to m \neq \underset{˙}{0})$
47	46	ancrd	$⊢ ((φ \land (X \in B \land Y \in B)) \land m \in S) \to (X = m \underset{˙}{\cdot} Y \to (m \neq \underset{˙}{0} \land X = m \underset{˙}{\cdot} Y))$
48		ovexd	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to (0 \dots N) \in V$
49		simplr	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to m \in S$
50	33	ad3antrrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to Y \in {Base}_{W}$
51	20	ad3antrrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to 0 \in (0 \dots N)$
52		eqid	$⊢ \cdot_{K} = \cdot_{K}$
53	4 34 6 48 49 50 51 5 52	frlmvscaval	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to (m \underset{˙}{\cdot} Y) (0) = m \cdot_{K} Y (0)$
54	53	fveq2d	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I ((m \underset{˙}{\cdot} Y) (0)) = I (m \cdot_{K} Y (0))$
55	9	ad3antrrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to K \in DivRing$
56	4 6 34	frlmbasf	$⊢ ((0 \dots N) \in V \land Y \in {Base}_{W}) \to Y : (0 \dots N) ⟶ S$
57	18 33 56	syl2anc	$⊢ φ \to Y : (0 \dots N) ⟶ S$
58	57 20	ffvelrnd	$⊢ φ \to Y (0) \in S$
59	58	ad3antrrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to Y (0) \in S$
60		simpr	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to m \neq \underset{˙}{0}$
61	14	ad3antrrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to Y (0) \neq \underset{˙}{0}$
62	6 7 52 8 55 49 59 60 61	drnginvmuld	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I (m \cdot_{K} Y (0)) = I (Y (0)) \cdot_{K} I (m)$
63	54 62	eqtrd	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I ((m \underset{˙}{\cdot} Y) (0)) = I (Y (0)) \cdot_{K} I (m)$
64	63	oveq1d	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I ((m \underset{˙}{\cdot} Y) (0)) \underset{˙}{\cdot} (m \underset{˙}{\cdot} Y) = (I (Y (0)) \cdot_{K} I (m)) \underset{˙}{\cdot} (m \underset{˙}{\cdot} Y)$
65	31	ad3antrrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to W \in LMod$
66	17	ad3antrrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to K \in Ring$
67	6 7 8 55 59 61	drnginvrcld	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I (Y (0)) \in S$
68	6 7 8 55 49 60	drnginvrcld	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I (m) \in S$
69	6 52 66 67 68	ringcld	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I (Y (0)) \cdot_{K} I (m) \in S$
70	25	fveq2d	$⊢ φ \to {Base}_{K} = {Base}_{Scalar (W)}$
71	6 70	syl5eq	$⊢ φ \to S = {Base}_{Scalar (W)}$
72	71	ad3antrrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to S = {Base}_{Scalar (W)}$
73	69 72	eleqtrd	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I (Y (0)) \cdot_{K} I (m) \in {Base}_{Scalar (W)}$
74	49 72	eleqtrd	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to m \in {Base}_{Scalar (W)}$
75		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
76		eqid	$⊢ \cdot_{Scalar (W)} = \cdot_{Scalar (W)}$
77	34 35 5 75 76	lmodvsass	$⊢ (W \in LMod \land (I (Y (0)) \cdot_{K} I (m) \in {Base}_{Scalar (W)} \land m \in {Base}_{Scalar (W)} \land Y \in {Base}_{W})) \to ((I (Y (0)) \cdot_{K} I (m)) \cdot_{Scalar (W)} m) \underset{˙}{\cdot} Y = (I (Y (0)) \cdot_{K} I (m)) \underset{˙}{\cdot} (m \underset{˙}{\cdot} Y)$
78	65 73 74 50 77	syl13anc	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to ((I (Y (0)) \cdot_{K} I (m)) \cdot_{Scalar (W)} m) \underset{˙}{\cdot} Y = (I (Y (0)) \cdot_{K} I (m)) \underset{˙}{\cdot} (m \underset{˙}{\cdot} Y)$
79	6 52 66 67 68 49	ringassd	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to (I (Y (0)) \cdot_{K} I (m)) \cdot_{K} m = I (Y (0)) \cdot_{K} (I (m) \cdot_{K} m)$
80	55 48 24	syl2anc	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to K = Scalar (W)$
81	80	fveq2d	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to \cdot_{K} = \cdot_{Scalar (W)}$
82	81	oveqd	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to (I (Y (0)) \cdot_{K} I (m)) \cdot_{K} m = (I (Y (0)) \cdot_{K} I (m)) \cdot_{Scalar (W)} m$
83		eqid	$⊢ 1_{K} = 1_{K}$
84	6 7 52 83 8 55 49 60	drnginvrld	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I (m) \cdot_{K} m = 1_{K}$
85	84	oveq2d	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I (Y (0)) \cdot_{K} (I (m) \cdot_{K} m) = I (Y (0)) \cdot_{K} 1_{K}$
86	6 52 83 66 67	ringridmd	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I (Y (0)) \cdot_{K} 1_{K} = I (Y (0))$
87	85 86	eqtrd	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I (Y (0)) \cdot_{K} (I (m) \cdot_{K} m) = I (Y (0))$
88	79 82 87	3eqtr3d	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to (I (Y (0)) \cdot_{K} I (m)) \cdot_{Scalar (W)} m = I (Y (0))$
89	88	oveq1d	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to ((I (Y (0)) \cdot_{K} I (m)) \cdot_{Scalar (W)} m) \underset{˙}{\cdot} Y = I (Y (0)) \underset{˙}{\cdot} Y$
90	64 78 89	3eqtr2d	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to I ((m \underset{˙}{\cdot} Y) (0)) \underset{˙}{\cdot} (m \underset{˙}{\cdot} Y) = I (Y (0)) \underset{˙}{\cdot} Y$
91		fveq1	$⊢ X = m \underset{˙}{\cdot} Y \to X (0) = (m \underset{˙}{\cdot} Y) (0)$
92	91	fveq2d	$⊢ X = m \underset{˙}{\cdot} Y \to I (X (0)) = I ((m \underset{˙}{\cdot} Y) (0))$
93		id	$⊢ X = m \underset{˙}{\cdot} Y \to X = m \underset{˙}{\cdot} Y$
94	92 93	oveq12d	$⊢ X = m \underset{˙}{\cdot} Y \to I (X (0)) \underset{˙}{\cdot} X = I ((m \underset{˙}{\cdot} Y) (0)) \underset{˙}{\cdot} (m \underset{˙}{\cdot} Y)$
95	94	eqeq1d	$⊢ X = m \underset{˙}{\cdot} Y \to (I (X (0)) \underset{˙}{\cdot} X = I (Y (0)) \underset{˙}{\cdot} Y \leftrightarrow I ((m \underset{˙}{\cdot} Y) (0)) \underset{˙}{\cdot} (m \underset{˙}{\cdot} Y) = I (Y (0)) \underset{˙}{\cdot} Y)$
96	90 95	syl5ibrcom	$⊢ (((φ \land (X \in B \land Y \in B)) \land m \in S) \land m \neq \underset{˙}{0}) \to (X = m \underset{˙}{\cdot} Y \to I (X (0)) \underset{˙}{\cdot} X = I (Y (0)) \underset{˙}{\cdot} Y)$
97	96	expimpd	$⊢ ((φ \land (X \in B \land Y \in B)) \land m \in S) \to ((m \neq \underset{˙}{0} \land X = m \underset{˙}{\cdot} Y) \to I (X (0)) \underset{˙}{\cdot} X = I (Y (0)) \underset{˙}{\cdot} Y)$
98	47 97	syld	$⊢ ((φ \land (X \in B \land Y \in B)) \land m \in S) \to (X = m \underset{˙}{\cdot} Y \to I (X (0)) \underset{˙}{\cdot} X = I (Y (0)) \underset{˙}{\cdot} Y)$
99	98	rexlimdva	$⊢ (φ \land (X \in B \land Y \in B)) \to (\exists m \in S X = m \underset{˙}{\cdot} Y \to I (X (0)) \underset{˙}{\cdot} X = I (Y (0)) \underset{˙}{\cdot} Y)$
100	99	impr	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to I (X (0)) \underset{˙}{\cdot} X = I (Y (0)) \underset{˙}{\cdot} Y$
101	13	neneqd	$⊢ φ \to \neg X (0) = \underset{˙}{0}$
102	101	iffalsed	$⊢ φ \to if (X (0) = \underset{˙}{0}, X, I (X (0)) \underset{˙}{\cdot} X) = I (X (0)) \underset{˙}{\cdot} X$
103	102	adantr	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to if (X (0) = \underset{˙}{0}, X, I (X (0)) \underset{˙}{\cdot} X) = I (X (0)) \underset{˙}{\cdot} X$
104	14	neneqd	$⊢ φ \to \neg Y (0) = \underset{˙}{0}$
105	104	iffalsed	$⊢ φ \to if (Y (0) = \underset{˙}{0}, Y, I (Y (0)) \underset{˙}{\cdot} Y) = I (Y (0)) \underset{˙}{\cdot} Y$
106	105	adantr	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to if (Y (0) = \underset{˙}{0}, Y, I (Y (0)) \underset{˙}{\cdot} Y) = I (Y (0)) \underset{˙}{\cdot} Y$
107	100 103 106	3eqtr4d	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to if (X (0) = \underset{˙}{0}, X, I (X (0)) \underset{˙}{\cdot} X) = if (Y (0) = \underset{˙}{0}, Y, I (Y (0)) \underset{˙}{\cdot} Y)$
108		fveq1	$⊢ b = X \to b (0) = X (0)$
109	108	eqeq1d	$⊢ b = X \to (b (0) = \underset{˙}{0} \leftrightarrow X (0) = \underset{˙}{0})$
110		id	$⊢ b = X \to b = X$
111	108	fveq2d	$⊢ b = X \to I (b (0)) = I (X (0))$
112	111 110	oveq12d	$⊢ b = X \to I (b (0)) \underset{˙}{\cdot} b = I (X (0)) \underset{˙}{\cdot} X$
113	109 110 112	ifbieq12d	$⊢ b = X \to if (b (0) = \underset{˙}{0}, b, I (b (0)) \underset{˙}{\cdot} b) = if (X (0) = \underset{˙}{0}, X, I (X (0)) \underset{˙}{\cdot} X)$
114		simprll	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to X \in B$
115		ovexd	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to I (X (0)) \underset{˙}{\cdot} X \in V$
116	114 115	ifexd	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to if (X (0) = \underset{˙}{0}, X, I (X (0)) \underset{˙}{\cdot} X) \in V$
117	2 113 114 116	fvmptd3	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to F (X) = if (X (0) = \underset{˙}{0}, X, I (X (0)) \underset{˙}{\cdot} X)$
118		fveq1	$⊢ b = Y \to b (0) = Y (0)$
119	118	eqeq1d	$⊢ b = Y \to (b (0) = \underset{˙}{0} \leftrightarrow Y (0) = \underset{˙}{0})$
120		id	$⊢ b = Y \to b = Y$
121	118	fveq2d	$⊢ b = Y \to I (b (0)) = I (Y (0))$
122	121 120	oveq12d	$⊢ b = Y \to I (b (0)) \underset{˙}{\cdot} b = I (Y (0)) \underset{˙}{\cdot} Y$
123	119 120 122	ifbieq12d	$⊢ b = Y \to if (b (0) = \underset{˙}{0}, b, I (b (0)) \underset{˙}{\cdot} b) = if (Y (0) = \underset{˙}{0}, Y, I (Y (0)) \underset{˙}{\cdot} Y)$
124		simprlr	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to Y \in B$
125		ovexd	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to I (Y (0)) \underset{˙}{\cdot} Y \in V$
126	124 125	ifexd	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to if (Y (0) = \underset{˙}{0}, Y, I (Y (0)) \underset{˙}{\cdot} Y) \in V$
127	2 123 124 126	fvmptd3	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to F (Y) = if (Y (0) = \underset{˙}{0}, Y, I (Y (0)) \underset{˙}{\cdot} Y)$
128	107 117 127	3eqtr4d	$⊢ (φ \land ((X \in B \land Y \in B) \land \exists m \in S X = m \underset{˙}{\cdot} Y)) \to F (X) = F (Y)$
129	15 128	sylan2b	$⊢ (φ \land X \underset{˙}{\sim} Y) \to F (X) = F (Y)$
130	1 4 3 6 5 9	prjspner	$⊢ φ \to \underset{˙}{\sim} Er B$
131	130	adantr	$⊢ (φ \land F (X) = F (Y)) \to \underset{˙}{\sim} Er B$
132	1 2 3 4 5 6 7 8 9 10 11	prjspner01	$⊢ φ \to X \underset{˙}{\sim} F (X)$
133	132	adantr	$⊢ (φ \land F (X) = F (Y)) \to X \underset{˙}{\sim} F (X)$
134	130 132	ercl2	$⊢ φ \to F (X) \in B$
135	134	adantr	$⊢ (φ \land F (X) = F (Y)) \to F (X) \in B$
136	131 135	erref	$⊢ (φ \land F (X) = F (Y)) \to F (X) \underset{˙}{\sim} F (X)$
137		breq2	$⊢ F (X) = F (Y) \to (F (X) \underset{˙}{\sim} F (X) \leftrightarrow F (X) \underset{˙}{\sim} F (Y))$
138	137	adantl	$⊢ (φ \land F (X) = F (Y)) \to (F (X) \underset{˙}{\sim} F (X) \leftrightarrow F (X) \underset{˙}{\sim} F (Y))$
139	136 138	mpbid	$⊢ (φ \land F (X) = F (Y)) \to F (X) \underset{˙}{\sim} F (Y)$
140	1 2 3 4 5 6 7 8 9 10 12	prjspner01	$⊢ φ \to Y \underset{˙}{\sim} F (Y)$
141	140	adantr	$⊢ (φ \land F (X) = F (Y)) \to Y \underset{˙}{\sim} F (Y)$
142	131 139 141	ertr4d	$⊢ (φ \land F (X) = F (Y)) \to F (X) \underset{˙}{\sim} Y$
143	131 133 142	ertrd	$⊢ (φ \land F (X) = F (Y)) \to X \underset{˙}{\sim} Y$
144	129 143	impbida	$⊢ φ \to (X \underset{˙}{\sim} Y \leftrightarrow F (X) = F (Y))$

Metamath Proof Explorer

Theorem prjspner1

Proof