This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ellspsn ⊢ ( ( ( 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 eqabdv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐺 } ) = { 𝑥 ∣ 𝐺 ∥ 𝑥 } )