Metamath Proof Explorer


Theorem subrgmcl

Description: A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypothesis subrgmcl.p · ˙ = R
Assertion subrgmcl A SubRing R X A Y A X · ˙ Y A

Proof

Step Hyp Ref Expression
1 subrgmcl.p · ˙ = R
2 eqid R 𝑠 A = R 𝑠 A
3 2 subrgring A SubRing R R 𝑠 A Ring
4 3 3ad2ant1 A SubRing R X A Y A R 𝑠 A Ring
5 simp2 A SubRing R X A Y A X A
6 2 subrgbas A SubRing R A = Base R 𝑠 A
7 6 3ad2ant1 A SubRing R X A Y A A = Base R 𝑠 A
8 5 7 eleqtrd A SubRing R X A Y A X Base R 𝑠 A
9 simp3 A SubRing R X A Y A Y A
10 9 7 eleqtrd A SubRing R X A Y A Y Base R 𝑠 A
11 eqid Base R 𝑠 A = Base R 𝑠 A
12 eqid R 𝑠 A = R 𝑠 A
13 11 12 ringcl R 𝑠 A Ring X Base R 𝑠 A Y Base R 𝑠 A X R 𝑠 A Y Base R 𝑠 A
14 4 8 10 13 syl3anc A SubRing R X A Y A X R 𝑠 A Y Base R 𝑠 A
15 2 1 ressmulr A SubRing R · ˙ = R 𝑠 A
16 15 3ad2ant1 A SubRing R X A Y A · ˙ = R 𝑠 A
17 16 oveqd A SubRing R X A Y A X · ˙ Y = X R 𝑠 A Y
18 14 17 7 3eltr4d A SubRing R X A Y A X · ˙ Y A