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

Metamath Proof Explorer

Theorem srasubrg

Description: A subring of the original structure is also a subring of the constructed subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023)

Ref Expression
Hypotheses srasubrg.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
srasubrg.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝑊 ) )
srasubrg.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
Assertion srasubrg ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 srasubrg.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2 srasubrg.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝑊 ) )
3 srasubrg.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
4 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
5 1 3 srabase ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ 𝐴 ) )
6 1 3 sraaddg ⊢ ( 𝜑 → ( +g ‘ 𝑊 ) = ( +g ‘ 𝐴 ) )
7 6 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
8 1 3 sramulr ⊢ ( 𝜑 → ( .r ‘ 𝑊 ) = ( .r ‘ 𝐴 ) )
9 8 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) )
10 4 5 7 9 subrgpropd ⊢ ( 𝜑 → ( SubRing ‘ 𝑊 ) = ( SubRing ‘ 𝐴 ) )
11 2 10 eleqtrd ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐴 ) )