Metamath Proof Explorer

Theorem rngodir

Description: Distributive law for the multiplication operation of a ring (right-distributivity). (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 rngodir ( ( 𝑅 ∈ 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 simp3 ⊢ ( ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) )
8 7 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) → ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) )
9 8 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) )
10 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐺 𝑦 ) = ( 𝐴 𝐺 𝑦 ) )
11 10 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝐴 𝐺 𝑦 ) 𝐻 𝑧 ) )
12 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐻 𝑧 ) = ( 𝐴 𝐻 𝑧 ) )
13 12 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) = ( ( 𝐴 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) )
14 11 13 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ↔ ( ( 𝐴 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝐴 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) )
15 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 𝑦 ) = ( 𝐴 𝐺 𝐵 ) )
16 15 oveq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐻 𝑧 ) )
17 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝐻 𝑧 ) = ( 𝐵 𝐻 𝑧 ) )
18 17 oveq2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) = ( ( 𝐴 𝐻 𝑧 ) 𝐺 ( 𝐵 𝐻 𝑧 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝐴 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ↔ ( ( 𝐴 𝐺 𝐵 ) 𝐻 𝑧 ) = ( ( 𝐴 𝐻 𝑧 ) 𝐺 ( 𝐵 𝐻 𝑧 ) ) ) )
20 oveq2 ⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 𝐺 𝐵 ) 𝐻 𝑧 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐻 𝐶 ) )
21 oveq2 ⊢ ( 𝑧 = 𝐶 → ( 𝐴 𝐻 𝑧 ) = ( 𝐴 𝐻 𝐶 ) )
22 oveq2 ⊢ ( 𝑧 = 𝐶 → ( 𝐵 𝐻 𝑧 ) = ( 𝐵 𝐻 𝐶 ) )
23 21 22 oveq12d ⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 𝐻 𝑧 ) 𝐺 ( 𝐵 𝐻 𝑧 ) ) = ( ( 𝐴 𝐻 𝐶 ) 𝐺 ( 𝐵 𝐻 𝐶 ) ) )
24 20 23 eqeq12d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 𝐺 𝐵 ) 𝐻 𝑧 ) = ( ( 𝐴 𝐻 𝑧 ) 𝐺 ( 𝐵 𝐻 𝑧 ) ) ↔ ( ( 𝐴 𝐺 𝐵 ) 𝐻 𝐶 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐺 ( 𝐵 𝐻 𝐶 ) ) ) )
25 14 19 24 rspc3v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐻 𝐶 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐺 ( 𝐵 𝐻 𝐶 ) ) ) )
26 9 25 syl5 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐻 𝐶 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐺 ( 𝐵 𝐻 𝐶 ) ) ) )
27 6 26 mpan9 ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐻 𝐶 ) = ( ( 𝐴 𝐻 𝐶 ) 𝐺 ( 𝐵 𝐻 𝐶 ) ) )