Metamath Proof Explorer

Theorem rngoass

Description: Associative law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ringi.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ringi.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
ringi.3 ⊢ 𝑋 = ran 𝐺
Assertion rngoass ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( 𝐴 𝐻 ( 𝐵 𝐻 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ringi.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ringi.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 ringi.3 ⊢ 𝑋 = ran 𝐺
4 1 2 3 rngoi ⊢ ( 𝑅 ∈ RingOps → ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
5 4 simprd ⊢ ( 𝑅 ∈ RingOps → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
6 5 simpld ⊢ ( 𝑅 ∈ RingOps → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) )
7 simp1 ⊢ ( ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
8 7 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) → ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
9 8 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
10 6 9 syl ⊢ ( 𝑅 ∈ RingOps → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
11 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐻 𝑦 ) = ( 𝐴 𝐻 𝑦 ) )
12 11 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( ( 𝐴 𝐻 𝑦 ) 𝐻 𝑧 ) )
13 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) = ( 𝐴 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
14 12 13 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ↔ ( ( 𝐴 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝐴 𝐻 ( 𝑦 𝐻 𝑧 ) ) ) )
15 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐻 𝑦 ) = ( 𝐴 𝐻 𝐵 ) )
16 15 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐻 𝑦 ) 𝐻 𝑧 ) = ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝑧 ) )
17 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝐻 𝑧 ) = ( 𝐵 𝐻 𝑧 ) )
18 17 oveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐻 ( 𝑦 𝐻 𝑧 ) ) = ( 𝐴 𝐻 ( 𝐵 𝐻 𝑧 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝐴 𝐻 ( 𝑦 𝐻 𝑧 ) ) ↔ ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝑧 ) = ( 𝐴 𝐻 ( 𝐵 𝐻 𝑧 ) ) ) )
20 oveq2 ⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝑧 ) = ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) )
21 oveq2 ⊢ ( 𝑧 = 𝐶 → ( 𝐵 𝐻 𝑧 ) = ( 𝐵 𝐻 𝐶 ) )
22 21 oveq2d ⊢ ( 𝑧 = 𝐶 → ( 𝐴 𝐻 ( 𝐵 𝐻 𝑧 ) ) = ( 𝐴 𝐻 ( 𝐵 𝐻 𝐶 ) ) )
23 20 22 eqeq12d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝑧 ) = ( 𝐴 𝐻 ( 𝐵 𝐻 𝑧 ) ) ↔ ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( 𝐴 𝐻 ( 𝐵 𝐻 𝐶 ) ) ) )
24 14 19 23 rspc3v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( 𝐴 𝐻 ( 𝐵 𝐻 𝐶 ) ) ) )
25 10 24 mpan9 ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 𝐶 ) = ( 𝐴 𝐻 ( 𝐵 𝐻 𝐶 ) ) )