Metamath Proof Explorer

Theorem crngm4

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

Ref Expression
Hypotheses crngm.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
crngm.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
crngm.3 ⊢ 𝑋 = ran 𝐺
Assertion crngm4 ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝐶 𝐻 𝐷 ) ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 ( 𝐵 𝐻 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 crngm.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 crngm.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 crngm.3 ⊢ 𝑋 = ran 𝐺
4 df-3an ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐶 ∈ 𝑋 ) )
5 1 2 3 crngm23 ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) )
6 4 5 sylan2br ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) )
7 6 adantrrr ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) )
8 7 oveq1d ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) 𝐻 𝐷 ) = ( ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) 𝐻 𝐷 ) )
9 crngorngo ⊢ ( 𝑅 ∈ CRingOps → 𝑅 ∈ RingOps )
10 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
11 10 3expb ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
12 11 adantrr ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
13 simprrl ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐶 ∈ 𝑋 )
14 simprrr ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐷 ∈ 𝑋 )
15 12 13 14 3jca ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) )
16 1 2 3 rngoass ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) 𝐻 𝐷 ) = ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝐶 𝐻 𝐷 ) ) )
17 15 16 syldan ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) 𝐻 𝐷 ) = ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝐶 𝐻 𝐷 ) ) )
18 9 17 sylan ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) 𝐻 𝐷 ) = ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝐶 𝐻 𝐷 ) ) )
19 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐻 𝐶 ) ∈ 𝑋 )
20 19 3expb ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐶 ) ∈ 𝑋 )
21 20 adantrlr ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐶 ) ∈ 𝑋 )
22 21 adantrrr ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( 𝐴 𝐻 𝐶 ) ∈ 𝑋 )
23 simprlr ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐵 ∈ 𝑋 )
24 22 23 14 3jca ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐻 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) )
25 1 2 3 rngoass ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 𝐻 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) 𝐻 𝐷 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 ( 𝐵 𝐻 𝐷 ) ) )
26 24 25 syldan ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) 𝐻 𝐷 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 ( 𝐵 𝐻 𝐷 ) ) )
27 9 26 sylan ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) 𝐻 𝐷 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 ( 𝐵 𝐻 𝐷 ) ) )
28 8 18 27 3eqtr3d ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝐶 𝐻 𝐷 ) ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 ( 𝐵 𝐻 𝐷 ) ) )
29 28 3impb ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝐶 𝐻 𝐷 ) ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 ( 𝐵 𝐻 𝐷 ) ) )