Theorem rngorn1eq

Description: In a unital ring the range of the addition equals the range of the multiplication. (Contributed by FL, 24-Jan-2010) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rnplrnml0.1	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
	rnplrnml0.2	⊢ 𝐺 = ( 1st ‘ 𝑅 )
Assertion	rngorn1eq	⊢ ( 𝑅 ∈ RingOps → ran 𝐺 = ran 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		rnplrnml0.1	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
2		rnplrnml0.2	⊢ 𝐺 = ( 1st ‘ 𝑅 )
3		eqid	⊢ ran 𝐺 = ran 𝐺
4	2 1 3	rngosm	⊢ ( 𝑅 ∈ RingOps → 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 )
5	2 1 3	rngoi	⊢ ( 𝑅 ∈ RingOps → ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) ∧ ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
6	5	simprrd	⊢ ( 𝑅 ∈ RingOps → ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) )
7		rngmgmbs4	⊢ ( ( 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) → ran 𝐻 = ran 𝐺 )
8	4 6 7	syl2anc	⊢ ( 𝑅 ∈ RingOps → ran 𝐻 = ran 𝐺 )
9	8	eqcomd	⊢ ( 𝑅 ∈ RingOps → ran 𝐺 = ran 𝐻 )