This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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