Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ellcsrspsn.p	⊢ + = ( +g ‘ 𝑅 )
	ellcsrspsn.t	⊢ · = ( .r ‘ 𝑅 )
	ellcsrspsn.e	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
	ellcsrspsn.u	⊢ 𝑈 = ( 𝑅 /s ∼ )
	ellcsrspsn.i	⊢ 𝐼 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑀 } )
	ellcsrspsn.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ellcsrspsn.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
	ellcsrspsn.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑈 ) )
Assertion	ellcsrspsn	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ( 𝑋 = [ 𝑥 ] ∼ ∧ 𝑋 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		ellcsrspsn.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ellcsrspsn.p	⊢ + = ( +g ‘ 𝑅 )
3		ellcsrspsn.t	⊢ · = ( .r ‘ 𝑅 )
4		ellcsrspsn.e	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
5		ellcsrspsn.u	⊢ 𝑈 = ( 𝑅 /s ∼ )
6		ellcsrspsn.i	⊢ 𝐼 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑀 } )
7		ellcsrspsn.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		ellcsrspsn.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
9		ellcsrspsn.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑈 ) )
10	4 5 1	quselbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑋 ∈ ( Base ‘ 𝑈 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ ) )
11	7 9 10	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( Base ‘ 𝑈 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ ) )
12	9 11	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ )
13	7	ringgrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Grp )
15		eqid	⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
16	8	snssd	⊢ ( 𝜑 → { 𝑀 } ⊆ 𝐵 )
17	15 1 7 16	rspssbasd	⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑀 } ) ⊆ 𝐵 )
18	6 17	eqsstrid	⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐼 ⊆ 𝐵 )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
21	1 4 2	eqglact	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ∼ = ( ( 𝑖 ∈ 𝐵 ↦ ( 𝑥 + 𝑖 ) ) “ 𝐼 ) )
22	14 19 20 21	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ∼ = ( ( 𝑖 ∈ 𝐵 ↦ ( 𝑥 + 𝑖 ) ) “ 𝐼 ) )
23		eqid	⊢ ( 𝑖 ∈ 𝐵 ↦ ( 𝑥 + 𝑖 ) ) = ( 𝑖 ∈ 𝐵 ↦ ( 𝑥 + 𝑖 ) )
24		vex	⊢ 𝑧 ∈ V
25	24	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑧 ∈ V )
26	23 25 19	elimampt	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑧 ∈ ( ( 𝑖 ∈ 𝐵 ↦ ( 𝑥 + 𝑖 ) ) “ 𝐼 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑧 = ( 𝑥 + 𝑖 ) ) )
27		oveq2	⊢ ( 𝑖 = ( 𝑦 · 𝑀 ) → ( 𝑥 + 𝑖 ) = ( 𝑥 + ( 𝑦 · 𝑀 ) ) )
28	27	eqeq2d	⊢ ( 𝑖 = ( 𝑦 · 𝑀 ) → ( 𝑧 = ( 𝑥 + 𝑖 ) ↔ 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) ) )
29	6	eleq2i	⊢ ( 𝑖 ∈ 𝐼 ↔ 𝑖 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑀 } ) )
30	1 3 15	elrspsn	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑖 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑀 } ) ↔ ∃ 𝑦 ∈ 𝐵 𝑖 = ( 𝑦 · 𝑀 ) ) )
31	7 8 30	syl2anc	⊢ ( 𝜑 → ( 𝑖 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑀 } ) ↔ ∃ 𝑦 ∈ 𝐵 𝑖 = ( 𝑦 · 𝑀 ) ) )
32	29 31	bitrid	⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↔ ∃ 𝑦 ∈ 𝐵 𝑖 = ( 𝑦 · 𝑀 ) ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑖 ∈ 𝐼 ↔ ∃ 𝑦 ∈ 𝐵 𝑖 = ( 𝑦 · 𝑀 ) ) )
34		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑦 · 𝑀 ) ∈ V )
35	28 33 34	rexxfr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑖 ∈ 𝐼 𝑧 = ( 𝑥 + 𝑖 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) ) )
36	26 35	bitrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑧 ∈ ( ( 𝑖 ∈ 𝐵 ↦ ( 𝑥 + 𝑖 ) ) “ 𝐼 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) ) )
37	36	eqabdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝐵 ↦ ( 𝑥 + 𝑖 ) ) “ 𝐼 ) = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) } )
38	22 37	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ∼ = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) } )
39		eqeq1	⊢ ( 𝑋 = [ 𝑥 ] ∼ → ( 𝑋 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) } ↔ [ 𝑥 ] ∼ = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) } ) )
40	38 39	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 = [ 𝑥 ] ∼ → 𝑋 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) } ) )
41	40	ancld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 = [ 𝑥 ] ∼ → ( 𝑋 = [ 𝑥 ] ∼ ∧ 𝑋 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) } ) ) )
42	41	reximdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ → ∃ 𝑥 ∈ 𝐵 ( 𝑋 = [ 𝑥 ] ∼ ∧ 𝑋 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) } ) ) )
43	12 42	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ( 𝑋 = [ 𝑥 ] ∼ ∧ 𝑋 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 + ( 𝑦 · 𝑀 ) ) } ) )