Metamath Proof Explorer

Theorem crngm4

Description: Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses crngm.1 ⊢G=1st⁡R
crngm.2 ⊢H=2nd⁡R
crngm.3 ⊢X=ran⁡G
Assertion crngm4 ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHBHCHD=AHCHBHD

Proof

Step Hyp Ref Expression
1 crngm.1 ⊢G=1st⁡R
2 crngm.2 ⊢H=2nd⁡R
3 crngm.3 ⊢X=ran⁡G
4 df-3an ⊢A∈X∧B∈X∧C∈X↔A∈X∧B∈X∧C∈X
5 1 2 3 crngm23 ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X→AHBHC=AHCHB
6 4 5 sylan2br ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X→AHBHC=AHCHB
7 6 adantrrr ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHBHC=AHCHB
8 7 oveq1d ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHBHCHD=AHCHBHD
9 crngorngo ⊢R∈CRingOps→R∈RingOps
10 1 2 3 rngocl ⊢R∈RingOps∧A∈X∧B∈X→AHB∈X
11 10 3expb ⊢R∈RingOps∧A∈X∧B∈X→AHB∈X
12 11 adantrr ⊢R∈RingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHB∈X
13 simprrl ⊢R∈RingOps∧A∈X∧B∈X∧C∈X∧D∈X→C∈X
14 simprrr ⊢R∈RingOps∧A∈X∧B∈X∧C∈X∧D∈X→D∈X
15 12 13 14 3jca ⊢R∈RingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHB∈X∧C∈X∧D∈X
16 1 2 3 rngoass ⊢R∈RingOps∧AHB∈X∧C∈X∧D∈X→AHBHCHD=AHBHCHD
17 15 16 syldan ⊢R∈RingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHBHCHD=AHBHCHD
18 9 17 sylan ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHBHCHD=AHBHCHD
19 1 2 3 rngocl ⊢R∈RingOps∧A∈X∧C∈X→AHC∈X
20 19 3expb ⊢R∈RingOps∧A∈X∧C∈X→AHC∈X
21 20 adantrlr ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→AHC∈X
22 21 adantrrr ⊢R∈RingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHC∈X
23 simprlr ⊢R∈RingOps∧A∈X∧B∈X∧C∈X∧D∈X→B∈X
24 22 23 14 3jca ⊢R∈RingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHC∈X∧B∈X∧D∈X
25 1 2 3 rngoass ⊢R∈RingOps∧AHC∈X∧B∈X∧D∈X→AHCHBHD=AHCHBHD
26 24 25 syldan ⊢R∈RingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHCHBHD=AHCHBHD
27 9 26 sylan ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHCHBHD=AHCHBHD
28 8 18 27 3eqtr3d ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHBHCHD=AHCHBHD
29 28 3impb ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X∧D∈X→AHBHCHD=AHCHBHD