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

Metamath Proof Explorer

Theorem subrgdvds

Description: If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses subrgdvds.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
subrgdvds.2 ⊢ ∥ = ( ∥r ‘ 𝑅 )
subrgdvds.3 ⊢ 𝐸 = ( ∥r ‘ 𝑆 )
Assertion subrgdvds ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐸 ⊆ ∥ )

Proof

Step Hyp Ref Expression
1 subrgdvds.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 subrgdvds.2 ⊢ ∥ = ( ∥r ‘ 𝑅 )
3 subrgdvds.3 ⊢ 𝐸 = ( ∥r ‘ 𝑆 )
4 3 reldvdsr ⊢ Rel 𝐸
5 4 a1i ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → Rel 𝐸 )
6 1 subrgbas ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 7 subrgss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
9 6 8 eqsstrrd ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑅 ) )
10 9 sseld ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑥 ∈ ( Base ‘ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
11 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12 1 11 ressmulr ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
13 12 oveqd ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑧 ( .r ‘ 𝑆 ) 𝑥 ) )
14 13 eqeq1d ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ↔ ( 𝑧 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑦 ) )
15 14 rexbidv ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ∃ 𝑧 ∈ ( Base ‘ 𝑆 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ↔ ∃ 𝑧 ∈ ( Base ‘ 𝑆 ) ( 𝑧 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑦 ) )
16 ssrexv ⊢ ( ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑅 ) → ( ∃ 𝑧 ∈ ( Base ‘ 𝑆 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 → ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
17 9 16 syl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ∃ 𝑧 ∈ ( Base ‘ 𝑆 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 → ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
18 15 17 sylbird ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ∃ 𝑧 ∈ ( Base ‘ 𝑆 ) ( 𝑧 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑦 → ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
19 10 18 anim12d ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑆 ) ( 𝑧 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑦 ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
20 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
21 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
22 20 3 21 dvdsr ⊢ ( 𝑥 𝐸 𝑦 ↔ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑆 ) ( 𝑧 ( .r ‘ 𝑆 ) 𝑥 ) = 𝑦 ) )
23 7 2 11 dvdsr ⊢ ( 𝑥 ∥ 𝑦 ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
24 19 22 23 3imtr4g ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑥 𝐸 𝑦 → 𝑥 ∥ 𝑦 ) )
25 df-br ⊢ ( 𝑥 𝐸 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐸 )
26 df-br ⊢ ( 𝑥 ∥ 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∥ )
27 24 25 26 3imtr3g ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐸 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∥ ) )
28 5 27 relssdv ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐸 ⊆ ∥ )