rngo1cl

Description: The unit of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ring1cl.1	⊢ 𝑋 = ran ( 1^st ‘ 𝑅 )
	ring1cl.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
	ring1cl.3	⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion	rngo1cl	⊢ ( 𝑅 ∈ RingOps → 𝑈 ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ring1cl.1	⊢ 𝑋 = ran ( 1^st ‘ 𝑅 )
2		ring1cl.2	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
3		ring1cl.3	⊢ 𝑈 = ( GId ‘ 𝐻 )
4	2	rngomndo	⊢ ( 𝑅 ∈ RingOps → 𝐻 ∈ MndOp )
5	2	eleq1i	⊢ ( 𝐻 ∈ MndOp ↔ ( 2^nd ‘ 𝑅 ) ∈ MndOp )
6		mndoismgmOLD	⊢ ( ( 2^nd ‘ 𝑅 ) ∈ MndOp → ( 2^nd ‘ 𝑅 ) ∈ Magma )
7		mndoisexid	⊢ ( ( 2^nd ‘ 𝑅 ) ∈ MndOp → ( 2^nd ‘ 𝑅 ) ∈ ExId )
8	6 7	jca	⊢ ( ( 2^nd ‘ 𝑅 ) ∈ MndOp → ( ( 2^nd ‘ 𝑅 ) ∈ Magma ∧ ( 2^nd ‘ 𝑅 ) ∈ ExId ) )
9	5 8	sylbi	⊢ ( 𝐻 ∈ MndOp → ( ( 2^nd ‘ 𝑅 ) ∈ Magma ∧ ( 2^nd ‘ 𝑅 ) ∈ ExId ) )
10	4 9	syl	⊢ ( 𝑅 ∈ RingOps → ( ( 2^nd ‘ 𝑅 ) ∈ Magma ∧ ( 2^nd ‘ 𝑅 ) ∈ ExId ) )
11		elin	⊢ ( ( 2^nd ‘ 𝑅 ) ∈ ( Magma ∩ ExId ) ↔ ( ( 2^nd ‘ 𝑅 ) ∈ Magma ∧ ( 2^nd ‘ 𝑅 ) ∈ ExId ) )
12	10 11	sylibr	⊢ ( 𝑅 ∈ RingOps → ( 2^nd ‘ 𝑅 ) ∈ ( Magma ∩ ExId ) )
13		eqid	⊢ ran ( 2^nd ‘ 𝑅 ) = ran ( 2^nd ‘ 𝑅 )
14	2	fveq2i	⊢ ( GId ‘ 𝐻 ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) )
15	3 14	eqtri	⊢ 𝑈 = ( GId ‘ ( 2^nd ‘ 𝑅 ) )
16	13 15	iorlid	⊢ ( ( 2^nd ‘ 𝑅 ) ∈ ( Magma ∩ ExId ) → 𝑈 ∈ ran ( 2^nd ‘ 𝑅 ) )
17	12 16	syl	⊢ ( 𝑅 ∈ RingOps → 𝑈 ∈ ran ( 2^nd ‘ 𝑅 ) )
18		eqid	⊢ ( 2^nd ‘ 𝑅 ) = ( 2^nd ‘ 𝑅 )
19		eqid	⊢ ( 1^st ‘ 𝑅 ) = ( 1^st ‘ 𝑅 )
20	18 19	rngorn1eq	⊢ ( 𝑅 ∈ RingOps → ran ( 1^st ‘ 𝑅 ) = ran ( 2^nd ‘ 𝑅 ) )
21		eqtr	⊢ ( ( 𝑋 = ran ( 1^st ‘ 𝑅 ) ∧ ran ( 1^st ‘ 𝑅 ) = ran ( 2^nd ‘ 𝑅 ) ) → 𝑋 = ran ( 2^nd ‘ 𝑅 ) )
22	21	eleq2d	⊢ ( ( 𝑋 = ran ( 1^st ‘ 𝑅 ) ∧ ran ( 1^st ‘ 𝑅 ) = ran ( 2^nd ‘ 𝑅 ) ) → ( 𝑈 ∈ 𝑋 ↔ 𝑈 ∈ ran ( 2^nd ‘ 𝑅 ) ) )
23	1 20 22	sylancr	⊢ ( 𝑅 ∈ RingOps → ( 𝑈 ∈ 𝑋 ↔ 𝑈 ∈ ran ( 2^nd ‘ 𝑅 ) ) )
24	17 23	mpbird	⊢ ( 𝑅 ∈ RingOps → 𝑈 ∈ 𝑋 )

Metamath Proof Explorer

Theorem rngo1cl

Proof