Metamath Proof Explorer

Theorem isprrngo

Description: Obsolete theorem, use isprmrng instead. The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	isprrng.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
		isprrng.2	⊢ 𝑍 = ( GId ‘ 𝐺 )
	Assertion	isprrngo	⊢ ( 𝑅 ∈ PrRing ↔ ( 𝑅 ∈ RingOps ∧ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isprrng.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		isprrng.2	⊢ 𝑍 = ( GId ‘ 𝐺 )
3		fveq2	⊢ ( 𝑟 = 𝑅 → ( 1^st ‘ 𝑟 ) = ( 1^st ‘ 𝑅 ) )
4	3 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 1^st ‘ 𝑟 ) = 𝐺 )
5	4	fveq2d	⊢ ( 𝑟 = 𝑅 → ( GId ‘ ( 1^st ‘ 𝑟 ) ) = ( GId ‘ 𝐺 ) )
6	5 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( GId ‘ ( 1^st ‘ 𝑟 ) ) = 𝑍 )
7	6	sneqd	⊢ ( 𝑟 = 𝑅 → { ( GId ‘ ( 1^st ‘ 𝑟 ) ) } = { 𝑍 } )
8		fveq2	⊢ ( 𝑟 = 𝑅 → ( PrIdl ‘ 𝑟 ) = ( PrIdl ‘ 𝑅 ) )
9	7 8	eleq12d	⊢ ( 𝑟 = 𝑅 → ( { ( GId ‘ ( 1^st ‘ 𝑟 ) ) } ∈ ( PrIdl ‘ 𝑟 ) ↔ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) )
10		df-prrngo	⊢ PrRing = { 𝑟 ∈ RingOps ∣ { ( GId ‘ ( 1^st ‘ 𝑟 ) ) } ∈ ( PrIdl ‘ 𝑟 ) }
11	9 10	elrab2	⊢ ( 𝑅 ∈ PrRing ↔ ( 𝑅 ∈ RingOps ∧ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) )