divrngpr

Description: A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011)

		Ref	Expression
	Assertion	divrngpr	⊢ ( 𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing )

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 1^st ‘ 𝑅 ) = ( 1^st ‘ 𝑅 )
2		eqid	⊢ ( 2^nd ‘ 𝑅 ) = ( 2^nd ‘ 𝑅 )
3		eqid	⊢ ( GId ‘ ( 1^st ‘ 𝑅 ) ) = ( GId ‘ ( 1^st ‘ 𝑅 ) )
4		eqid	⊢ ran ( 1^st ‘ 𝑅 ) = ran ( 1^st ‘ 𝑅 )
5	1 2 3 4	isdrngo1	⊢ ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( ( 2^nd ‘ 𝑅 ) ↾ ( ( ran ( 1^st ‘ 𝑅 ) ∖ { ( GId ‘ ( 1^st ‘ 𝑅 ) ) } ) × ( ran ( 1^st ‘ 𝑅 ) ∖ { ( GId ‘ ( 1^st ‘ 𝑅 ) ) } ) ) ) ∈ GrpOp ) )
6	5	simplbi	⊢ ( 𝑅 ∈ DivRingOps → 𝑅 ∈ RingOps )
7		eqid	⊢ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) )
8	1 2 4 3 7	dvrunz	⊢ ( 𝑅 ∈ DivRingOps → ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ≠ ( GId ‘ ( 1^st ‘ 𝑅 ) ) )
9	1 2 4 3	divrngidl	⊢ ( 𝑅 ∈ DivRingOps → ( Idl ‘ 𝑅 ) = { { ( GId ‘ ( 1^st ‘ 𝑅 ) ) } , ran ( 1^st ‘ 𝑅 ) } )
10	1 2 4 3 7	smprngopr	⊢ ( ( 𝑅 ∈ RingOps ∧ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ≠ ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∧ ( Idl ‘ 𝑅 ) = { { ( GId ‘ ( 1^st ‘ 𝑅 ) ) } , ran ( 1^st ‘ 𝑅 ) } ) → 𝑅 ∈ PrRing )
11	6 8 9 10	syl3anc	⊢ ( 𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing )

Metamath Proof Explorer