Theorem rngoidmlem

Description: Obsolete theorem, use ringidmlem instead. The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	uridm.1	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
	uridm.2	⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
	uridm.3	⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion	rngoidmlem	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		uridm.1	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
2		uridm.2	⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
3		uridm.3	⊢ 𝑈 = ( GId ‘ 𝐻 )
4	1	rngomndo	⊢ ( 𝑅 ∈ RingOps → 𝐻 ∈ MndOp )
5		mndomgmid	⊢ ( 𝐻 ∈ MndOp → 𝐻 ∈ ( Magma ∩ ExId ) )
6		eqid	⊢ ran 𝐻 = ran 𝐻
7	6 3	cmpidelt	⊢ ( ( 𝐻 ∈ ( Magma ∩ ExId ) ∧ 𝐴 ∈ ran 𝐻 ) → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) )
8	7	ex	⊢ ( 𝐻 ∈ ( Magma ∩ ExId ) → ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) )
9	4 5 8	3syl	⊢ ( 𝑅 ∈ RingOps → ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) )
10		eqid	⊢ ( 1st ‘ 𝑅 ) = ( 1st ‘ 𝑅 )
11	1 10	rngorn1eq	⊢ ( 𝑅 ∈ RingOps → ran ( 1st ‘ 𝑅 ) = ran 𝐻 )
12		eqtr	⊢ ( ( 𝑋 = ran ( 1st ‘ 𝑅 ) ∧ ran ( 1st ‘ 𝑅 ) = ran 𝐻 ) → 𝑋 = ran 𝐻 )
13		simpl	⊢ ( ( 𝑋 = ran 𝐻 ∧ 𝑅 ∈ RingOps ) → 𝑋 = ran 𝐻 )
14	13	eleq2d	⊢ ( ( 𝑋 = ran 𝐻 ∧ 𝑅 ∈ RingOps ) → ( 𝐴 ∈ 𝑋 ↔ 𝐴 ∈ ran 𝐻 ) )
15	14	imbi1d	⊢ ( ( 𝑋 = ran 𝐻 ∧ 𝑅 ∈ RingOps ) → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ↔ ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ) )
16	15	ex	⊢ ( 𝑋 = ran 𝐻 → ( 𝑅 ∈ RingOps → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ↔ ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ) ) )
17	12 16	syl	⊢ ( ( 𝑋 = ran ( 1st ‘ 𝑅 ) ∧ ran ( 1st ‘ 𝑅 ) = ran 𝐻 ) → ( 𝑅 ∈ RingOps → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ↔ ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ) ) )
18	2 17	mpan	⊢ ( ran ( 1st ‘ 𝑅 ) = ran 𝐻 → ( 𝑅 ∈ RingOps → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ↔ ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ) ) )
19	11 18	mpcom	⊢ ( 𝑅 ∈ RingOps → ( ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ↔ ( 𝐴 ∈ ran 𝐻 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) ) )
20	9 19	mpbird	⊢ ( 𝑅 ∈ RingOps → ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) )
21	20	imp	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) )