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

Metamath Proof Explorer

Theorem rngosm

Description: Functionality of 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	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
		ringi.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
		ringi.3	⊢ 𝑋 = ran 𝐺
	Assertion	rngosm	⊢ ( 𝑅 ∈ RingOps → 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ringi.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		ringi.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
3		ringi.3	⊢ 𝑋 = ran 𝐺
4	1 2 3	rngoi	⊢ ( 𝑅 ∈ RingOps → ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
5	4	simpld	⊢ ( 𝑅 ∈ RingOps → ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
6	5	simprd	⊢ ( 𝑅 ∈ RingOps → 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )