ellcsrspsn

Description: Membership in a left coset in a quotient of a ring by the span of a singleton (that is, by the ideal generated by an element). This characterization comes from eqglact and elrspsn . (Contributed by SN, 19-Jun-2025)

	Ref	Expression
Hypotheses	ellcsrspsn.b	$⊢ B = {Base}_{R}$
	ellcsrspsn.p	$⊢ \underset{˙}{+} = +_{R}$
	ellcsrspsn.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ellcsrspsn.e	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
	ellcsrspsn.u	$⊢ U = R /_{𝑠} \underset{˙}{\sim}$
	ellcsrspsn.i	$⊢ I = RSpan (R) (\{M\})$
	ellcsrspsn.r	$⊢ φ \to R \in Ring$
	ellcsrspsn.m	$⊢ φ \to M \in B$
	ellcsrspsn.x	$⊢ φ \to X \in {Base}_{U}$
Assertion	ellcsrspsn	$⊢ φ \to \exists x \in B (X = [x] \underset{˙}{\sim} \land X = \{z \| \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M)\})$

Proof

Step	Hyp	Ref	Expression
1		ellcsrspsn.b	$⊢ B = {Base}_{R}$
2		ellcsrspsn.p	$⊢ \underset{˙}{+} = +_{R}$
3		ellcsrspsn.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		ellcsrspsn.e	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
5		ellcsrspsn.u	$⊢ U = R /_{𝑠} \underset{˙}{\sim}$
6		ellcsrspsn.i	$⊢ I = RSpan (R) (\{M\})$
7		ellcsrspsn.r	$⊢ φ \to R \in Ring$
8		ellcsrspsn.m	$⊢ φ \to M \in B$
9		ellcsrspsn.x	$⊢ φ \to X \in {Base}_{U}$
10	4 5 1	quselbas	$⊢ (R \in Ring \land X \in {Base}_{U}) \to (X \in {Base}_{U} \leftrightarrow \exists x \in B X = [x] \underset{˙}{\sim})$
11	7 9 10	syl2anc	$⊢ φ \to (X \in {Base}_{U} \leftrightarrow \exists x \in B X = [x] \underset{˙}{\sim})$
12	9 11	mpbid	$⊢ φ \to \exists x \in B X = [x] \underset{˙}{\sim}$
13	7	ringgrpd	$⊢ φ \to R \in Grp$
14	13	adantr	$⊢ (φ \land x \in B) \to R \in Grp$
15		eqid	$⊢ RSpan (R) = RSpan (R)$
16	8	snssd	$⊢ φ \to \{M\} \subseteq B$
17	15 1 7 16	rspssbasd	$⊢ φ \to RSpan (R) (\{M\}) \subseteq B$
18	6 17	eqsstrid	$⊢ φ \to I \subseteq B$
19	18	adantr	$⊢ (φ \land x \in B) \to I \subseteq B$
20		simpr	$⊢ (φ \land x \in B) \to x \in B$
21	1 4 2	eqglact	$⊢ (R \in Grp \land I \subseteq B \land x \in B) \to [x] \underset{˙}{\sim} = (i \in B ⟼ x \underset{˙}{+} i) [I]$
22	14 19 20 21	syl3anc	$⊢ (φ \land x \in B) \to [x] \underset{˙}{\sim} = (i \in B ⟼ x \underset{˙}{+} i) [I]$
23		eqid	$⊢ (i \in B ⟼ x \underset{˙}{+} i) = (i \in B ⟼ x \underset{˙}{+} i)$
24		vex	$⊢ z \in V$
25	24	a1i	$⊢ (φ \land x \in B) \to z \in V$
26	23 25 19	elimampt	$⊢ (φ \land x \in B) \to (z \in (i \in B ⟼ x \underset{˙}{+} i) [I] \leftrightarrow \exists i \in I z = x \underset{˙}{+} i)$
27		oveq2	$⊢ i = y \underset{˙}{\cdot} M \to x \underset{˙}{+} i = x \underset{˙}{+} (y \underset{˙}{\cdot} M)$
28	27	eqeq2d	$⊢ i = y \underset{˙}{\cdot} M \to (z = x \underset{˙}{+} i \leftrightarrow z = x \underset{˙}{+} (y \underset{˙}{\cdot} M))$
29	6	eleq2i	$⊢ i \in I \leftrightarrow i \in RSpan (R) (\{M\})$
30	1 3 15	elrspsn	$⊢ (R \in Ring \land M \in B) \to (i \in RSpan (R) (\{M\}) \leftrightarrow \exists y \in B i = y \underset{˙}{\cdot} M)$
31	7 8 30	syl2anc	$⊢ φ \to (i \in RSpan (R) (\{M\}) \leftrightarrow \exists y \in B i = y \underset{˙}{\cdot} M)$
32	29 31	bitrid	$⊢ φ \to (i \in I \leftrightarrow \exists y \in B i = y \underset{˙}{\cdot} M)$
33	32	adantr	$⊢ (φ \land x \in B) \to (i \in I \leftrightarrow \exists y \in B i = y \underset{˙}{\cdot} M)$
34		ovexd	$⊢ (φ \land x \in B) \to y \underset{˙}{\cdot} M \in V$
35	28 33 34	rexxfr3d	$⊢ (φ \land x \in B) \to (\exists i \in I z = x \underset{˙}{+} i \leftrightarrow \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M))$
36	26 35	bitrd	$⊢ (φ \land x \in B) \to (z \in (i \in B ⟼ x \underset{˙}{+} i) [I] \leftrightarrow \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M))$
37	36	eqabdv	$⊢ (φ \land x \in B) \to (i \in B ⟼ x \underset{˙}{+} i) [I] = \{z \| \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M)\}$
38	22 37	eqtrd	$⊢ (φ \land x \in B) \to [x] \underset{˙}{\sim} = \{z \| \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M)\}$
39		eqeq1	$⊢ X = [x] \underset{˙}{\sim} \to (X = \{z \| \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M)\} \leftrightarrow [x] \underset{˙}{\sim} = \{z \| \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M)\})$
40	38 39	syl5ibrcom	$⊢ (φ \land x \in B) \to (X = [x] \underset{˙}{\sim} \to X = \{z \| \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M)\})$
41	40	ancld	$⊢ (φ \land x \in B) \to (X = [x] \underset{˙}{\sim} \to (X = [x] \underset{˙}{\sim} \land X = \{z \| \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M)\}))$
42	41	reximdva	$⊢ φ \to (\exists x \in B X = [x] \underset{˙}{\sim} \to \exists x \in B (X = [x] \underset{˙}{\sim} \land X = \{z \| \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M)\}))$
43	12 42	mpd	$⊢ φ \to \exists x \in B (X = [x] \underset{˙}{\sim} \land X = \{z \| \exists y \in B z = x \underset{˙}{+} (y \underset{˙}{\cdot} M)\})$

Metamath Proof Explorer

Theorem ellcsrspsn

Proof