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