Metamath Proof Explorer


Theorem 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 𝑂 = ( oppr𝑅 )
issrng.i = ( *rf𝑅 )
Assertion issrng ( 𝑅 ∈ *-Ring ↔ ( ∈ ( 𝑅 RingHom 𝑂 ) ∧ = ) )

Proof

Step Hyp Ref Expression
1 issrng.o 𝑂 = ( oppr𝑅 )
2 issrng.i = ( *rf𝑅 )
3 df-srng *-Ring = { 𝑟[ ( *rf𝑟 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑟 RingHom ( oppr𝑟 ) ) ∧ 𝑖 = 𝑖 ) }
4 3 eleq2i ( 𝑅 ∈ *-Ring ↔ 𝑅 ∈ { 𝑟[ ( *rf𝑟 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑟 RingHom ( oppr𝑟 ) ) ∧ 𝑖 = 𝑖 ) } )
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𝑟 ) ) → ( oppr𝑟 ) = ( oppr𝑅 ) )
14 13 1 eqtr4di ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( oppr𝑟 ) = 𝑂 )
15 12 14 oveq12d ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( 𝑟 RingHom ( oppr𝑟 ) ) = ( 𝑅 RingHom 𝑂 ) )
16 11 15 eleq12d ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( 𝑖 ∈ ( 𝑟 RingHom ( oppr𝑟 ) ) ↔ ∈ ( 𝑅 RingHom 𝑂 ) ) )
17 11 cnveqd ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → 𝑖 = )
18 11 17 eqeq12d ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( 𝑖 = 𝑖 = ) )
19 16 18 anbi12d ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( ( 𝑖 ∈ ( 𝑟 RingHom ( oppr𝑟 ) ) ∧ 𝑖 = 𝑖 ) ↔ ( ∈ ( 𝑅 RingHom 𝑂 ) ∧ = ) ) )
20 7 19 sbcied ( 𝑟 = 𝑅 → ( [ ( *rf𝑟 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑟 RingHom ( oppr𝑟 ) ) ∧ 𝑖 = 𝑖 ) ↔ ( ∈ ( 𝑅 RingHom 𝑂 ) ∧ = ) ) )
21 6 20 elab3 ( 𝑅 ∈ { 𝑟[ ( *rf𝑟 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑟 RingHom ( oppr𝑟 ) ) ∧ 𝑖 = 𝑖 ) } ↔ ( ∈ ( 𝑅 RingHom 𝑂 ) ∧ = ) )
22 4 21 bitri ( 𝑅 ∈ *-Ring ↔ ( ∈ ( 𝑅 RingHom 𝑂 ) ∧ = ) )