Theorem rspsn

Description: Membership in principal ideals is closely related to divisibility. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	rspsn.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rspsn.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	rspsn.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
Assertion	rspsn	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐺 } ) = { 𝑥 ∣ 𝐺 ∥ 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		rspsn.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rspsn.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3		rspsn.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
4		eqcom	⊢ ( 𝑥 = ( 𝑎 ( .r ‘ 𝑅 ) 𝐺 ) ↔ ( 𝑎 ( .r ‘ 𝑅 ) 𝐺 ) = 𝑥 )
5	4	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝑥 = ( 𝑎 ( .r ‘ 𝑅 ) 𝐺 ) ↔ ( 𝑎 ( .r ‘ 𝑅 ) 𝐺 ) = 𝑥 ) )
6	5	rexbidv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( ∃ 𝑎 ∈ 𝐵 𝑥 = ( 𝑎 ( .r ‘ 𝑅 ) 𝐺 ) ↔ ∃ 𝑎 ∈ 𝐵 ( 𝑎 ( .r ‘ 𝑅 ) 𝐺 ) = 𝑥 ) )
7		rlmlmod	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
8		rlmsca2	⊢ ( I ‘ 𝑅 ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
9		baseid	⊢ Base = Slot ( Base ‘ ndx )
10	9 1	strfvi	⊢ 𝐵 = ( Base ‘ ( I ‘ 𝑅 ) )
11		rlmbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
12	1 11	eqtri	⊢ 𝐵 = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
13		rlmvsca	⊢ ( .r ‘ 𝑅 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
14		rspval	⊢ ( RSpan ‘ 𝑅 ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
15	2 14	eqtri	⊢ 𝐾 = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
16	8 10 12 13 15	lspsnel	⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐺 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝐺 } ) ↔ ∃ 𝑎 ∈ 𝐵 𝑥 = ( 𝑎 ( .r ‘ 𝑅 ) 𝐺 ) ) )
17	7 16	sylan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝐺 } ) ↔ ∃ 𝑎 ∈ 𝐵 𝑥 = ( 𝑎 ( .r ‘ 𝑅 ) 𝐺 ) ) )
18		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
19	1 3 18	dvdsr2	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐺 ∥ 𝑥 ↔ ∃ 𝑎 ∈ 𝐵 ( 𝑎 ( .r ‘ 𝑅 ) 𝐺 ) = 𝑥 ) )
20	19	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝐺 ∥ 𝑥 ↔ ∃ 𝑎 ∈ 𝐵 ( 𝑎 ( .r ‘ 𝑅 ) 𝐺 ) = 𝑥 ) )
21	6 17 20	3bitr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝐺 } ) ↔ 𝐺 ∥ 𝑥 ) )
22	21	abbi2dv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐺 } ) = { 𝑥 ∣ 𝐺 ∥ 𝑥 } )