Theorem rngoi

Description: The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007) (Proof shortened by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ringi.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	ringi.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
	ringi.3	⊢ 𝑋 = ran 𝐺
Assertion	rngoi	⊢ ( 𝑅 ∈ RingOps → ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ringi.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		ringi.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3		ringi.3	⊢ 𝑋 = ran 𝐺
4	1 2	opeq12i	⊢ ⟨ 𝐺 , 𝐻 ⟩ = ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩
5		relrngo	⊢ Rel RingOps
6		1st2nd	⊢ ( ( Rel RingOps ∧ 𝑅 ∈ RingOps ) → 𝑅 = ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ )
7	5 6	mpan	⊢ ( 𝑅 ∈ RingOps → 𝑅 = ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ )
8	4 7	eqtr4id	⊢ ( 𝑅 ∈ RingOps → ⟨ 𝐺 , 𝐻 ⟩ = 𝑅 )
9		id	⊢ ( 𝑅 ∈ RingOps → 𝑅 ∈ RingOps )
10	8 9	eqeltrd	⊢ ( 𝑅 ∈ RingOps → ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps )
11	2	fvexi	⊢ 𝐻 ∈ V
12	3	isrngo	⊢ ( 𝐻 ∈ V → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) )
13	11 12	ax-mp	⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
14	10 13	sylib	⊢ ( 𝑅 ∈ RingOps → ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )