Theorem crngm23

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	crngm23	⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		crngm.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		crngm.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3		crngm.3	⊢ 𝑋 = ran 𝐺
4	1 2 3	crngocom	⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝐻 𝐶 ) = ( 𝐶 𝐻 𝐵 ) )
5	4	3adant3r1	⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐻 𝐶 ) = ( 𝐶 𝐻 𝐵 ) )
6	5	oveq2d	⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐻 ( 𝐵 𝐻 𝐶 ) ) = ( 𝐴 𝐻 ( 𝐶 𝐻 𝐵 ) ) )
7		crngorngo	⊢ ( 𝑅 ∈ CRingOps → 𝑅 ∈ RingOps )
8	1 2 3	rngoass	⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( 𝐴 𝐻 ( 𝐵 𝐻 𝐶 ) ) )
9	7 8	sylan	⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( 𝐴 𝐻 ( 𝐵 𝐻 𝐶 ) ) )
10	1 2 3	rngoass	⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) = ( 𝐴 𝐻 ( 𝐶 𝐻 𝐵 ) ) )
11	10	3exp2	⊢ ( 𝑅 ∈ RingOps → ( 𝐴 ∈ 𝑋 → ( 𝐶 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) = ( 𝐴 𝐻 ( 𝐶 𝐻 𝐵 ) ) ) ) ) )
12	11	com34	⊢ ( 𝑅 ∈ RingOps → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐶 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) = ( 𝐴 𝐻 ( 𝐶 𝐻 𝐵 ) ) ) ) ) )
13	12	3imp2	⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) = ( 𝐴 𝐻 ( 𝐶 𝐻 𝐵 ) ) )
14	7 13	sylan	⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) = ( 𝐴 𝐻 ( 𝐶 𝐻 𝐵 ) ) )
15	6 9 14	3eqtr4d	⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐻 𝐵 ) )