Metamath Proof Explorer


Theorem qusmul2

Description: Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024)

Ref Expression
Hypotheses qusmul2.h Q = R / 𝑠 R ~ QG I
qusmul2.v B = Base R
qusmul2.p · ˙ = R
qusmul2.a × ˙ = Q
qusmul2.1 φ R Ring
qusmul2.2 φ I 2Ideal R
qusmul2.3 φ X B
qusmul2.4 φ Y B
Assertion qusmul2 φ X R ~ QG I × ˙ Y R ~ QG I = X · ˙ Y R ~ QG I

Proof

Step Hyp Ref Expression
1 qusmul2.h Q = R / 𝑠 R ~ QG I
2 qusmul2.v B = Base R
3 qusmul2.p · ˙ = R
4 qusmul2.a × ˙ = Q
5 qusmul2.1 φ R Ring
6 qusmul2.2 φ I 2Ideal R
7 qusmul2.3 φ X B
8 qusmul2.4 φ Y B
9 1 a1i φ Q = R / 𝑠 R ~ QG I
10 2 a1i φ B = Base R
11 6 2idllidld φ I LIdeal R
12 eqid LIdeal R = LIdeal R
13 12 lidlsubg R Ring I LIdeal R I SubGrp R
14 5 11 13 syl2anc φ I SubGrp R
15 eqid R ~ QG I = R ~ QG I
16 2 15 eqger I SubGrp R R ~ QG I Er B
17 14 16 syl φ R ~ QG I Er B
18 eqid 2Ideal R = 2Ideal R
19 2 15 18 3 2idlcpbl R Ring I 2Ideal R x R ~ QG I y z R ~ QG I t x · ˙ z R ~ QG I y · ˙ t
20 5 6 19 syl2anc φ x R ~ QG I y z R ~ QG I t x · ˙ z R ~ QG I y · ˙ t
21 2 3 ringcl R Ring p B q B p · ˙ q B
22 21 3expb R Ring p B q B p · ˙ q B
23 5 22 sylan φ p B q B p · ˙ q B
24 23 caovclg φ y B t B y · ˙ t B
25 9 10 17 5 20 24 3 4 qusmulval φ X B Y B X R ~ QG I × ˙ Y R ~ QG I = X · ˙ Y R ~ QG I
26 7 8 25 mpd3an23 φ X R ~ QG I × ˙ Y R ~ QG I = X · ˙ Y R ~ QG I