issrng

Description: The predicate "is a star ring". (Contributed by NM, 22-Sep-2011) (Revised by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Hypotheses	issrng.o	⊢ 𝑂 = ( opp_r ‘ 𝑅 )
	issrng.i	⊢ ∗ = ( *_rf ‘ 𝑅 )
Assertion	issrng	⊢ ( 𝑅 ∈ *-Ring ↔ ( ∗ ∈ ( 𝑅 RingHom 𝑂 ) ∧ ∗ = ^◡ ∗ ) )

Proof

Step	Hyp	Ref	Expression
1		issrng.o	⊢ 𝑂 = ( opp_r ‘ 𝑅 )
2		issrng.i	⊢ ∗ = ( *_rf ‘ 𝑅 )
3		df-srng	⊢ -Ring = { 𝑟 ∣ [ ( _rf ‘ 𝑟 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑟 RingHom ( opp_r ‘ 𝑟 ) ) ∧ 𝑖 = ^◡ 𝑖 ) }
4	3	eleq2i	⊢ ( 𝑅 ∈ -Ring ↔ 𝑅 ∈ { 𝑟 ∣ [ ( _rf ‘ 𝑟 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑟 RingHom ( opp_r ‘ 𝑟 ) ) ∧ 𝑖 = ^◡ 𝑖 ) } )
5		rhmrcl1	⊢ ( ∗ ∈ ( 𝑅 RingHom 𝑂 ) → 𝑅 ∈ Ring )
6	5	adantr	⊢ ( ( ∗ ∈ ( 𝑅 RingHom 𝑂 ) ∧ ∗ = ^◡ ∗ ) → 𝑅 ∈ Ring )
7		fvexd	⊢ ( 𝑟 = 𝑅 → ( *_rf ‘ 𝑟 ) ∈ V )
8		id	⊢ ( 𝑖 = ( _rf ‘ 𝑟 ) → 𝑖 = ( _rf ‘ 𝑟 ) )
9		fveq2	⊢ ( 𝑟 = 𝑅 → ( _rf ‘ 𝑟 ) = ( _rf ‘ 𝑅 ) )
10	9 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( *_rf ‘ 𝑟 ) = ∗ )
11	8 10	sylan9eqr	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = ( *_rf ‘ 𝑟 ) ) → 𝑖 = ∗ )
12		simpl	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = ( *_rf ‘ 𝑟 ) ) → 𝑟 = 𝑅 )
13	12	fveq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = ( *_rf ‘ 𝑟 ) ) → ( opp_r ‘ 𝑟 ) = ( opp_r ‘ 𝑅 ) )
14	13 1	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = ( *_rf ‘ 𝑟 ) ) → ( opp_r ‘ 𝑟 ) = 𝑂 )
15	12 14	oveq12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = ( *_rf ‘ 𝑟 ) ) → ( 𝑟 RingHom ( opp_r ‘ 𝑟 ) ) = ( 𝑅 RingHom 𝑂 ) )
16	11 15	eleq12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = ( *_rf ‘ 𝑟 ) ) → ( 𝑖 ∈ ( 𝑟 RingHom ( opp_r ‘ 𝑟 ) ) ↔ ∗ ∈ ( 𝑅 RingHom 𝑂 ) ) )
17	11	cnveqd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = ( *_rf ‘ 𝑟 ) ) → ^◡ 𝑖 = ^◡ ∗ )
18	11 17	eqeq12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = ( *_rf ‘ 𝑟 ) ) → ( 𝑖 = ^◡ 𝑖 ↔ ∗ = ^◡ ∗ ) )
19	16 18	anbi12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = ( *_rf ‘ 𝑟 ) ) → ( ( 𝑖 ∈ ( 𝑟 RingHom ( opp_r ‘ 𝑟 ) ) ∧ 𝑖 = ^◡ 𝑖 ) ↔ ( ∗ ∈ ( 𝑅 RingHom 𝑂 ) ∧ ∗ = ^◡ ∗ ) ) )
20	7 19	sbcied	⊢ ( 𝑟 = 𝑅 → ( [ ( *_rf ‘ 𝑟 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑟 RingHom ( opp_r ‘ 𝑟 ) ) ∧ 𝑖 = ^◡ 𝑖 ) ↔ ( ∗ ∈ ( 𝑅 RingHom 𝑂 ) ∧ ∗ = ^◡ ∗ ) ) )
21	6 20	elab3	⊢ ( 𝑅 ∈ { 𝑟 ∣ [ ( *_rf ‘ 𝑟 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑟 RingHom ( opp_r ‘ 𝑟 ) ) ∧ 𝑖 = ^◡ 𝑖 ) } ↔ ( ∗ ∈ ( 𝑅 RingHom 𝑂 ) ∧ ∗ = ^◡ ∗ ) )
22	4 21	bitri	⊢ ( 𝑅 ∈ *-Ring ↔ ( ∗ ∈ ( 𝑅 RingHom 𝑂 ) ∧ ∗ = ^◡ ∗ ) )

Metamath Proof Explorer

Theorem issrng

Proof