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 elexd ( ∈ ( 𝑅 RingHom 𝑂 ) → 𝑅 ∈ V )
7 6 adantr ( ( ∈ ( 𝑅 RingHom 𝑂 ) ∧ = ) → 𝑅 ∈ V )
8 fvexd ( 𝑟 = 𝑅 → ( *rf𝑟 ) ∈ V )
9 id ( 𝑖 = ( *rf𝑟 ) → 𝑖 = ( *rf𝑟 ) )
10 fveq2 ( 𝑟 = 𝑅 → ( *rf𝑟 ) = ( *rf𝑅 ) )
11 10 2 eqtr4di ( 𝑟 = 𝑅 → ( *rf𝑟 ) = )
12 9 11 sylan9eqr ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → 𝑖 = )
13 simpl ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → 𝑟 = 𝑅 )
14 13 fveq2d ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( oppr𝑟 ) = ( oppr𝑅 ) )
15 14 1 eqtr4di ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( oppr𝑟 ) = 𝑂 )
16 13 15 oveq12d ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( 𝑟 RingHom ( oppr𝑟 ) ) = ( 𝑅 RingHom 𝑂 ) )
17 12 16 eleq12d ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( 𝑖 ∈ ( 𝑟 RingHom ( oppr𝑟 ) ) ↔ ∈ ( 𝑅 RingHom 𝑂 ) ) )
18 12 cnveqd ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → 𝑖 = )
19 12 18 eqeq12d ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( 𝑖 = 𝑖 = ) )
20 17 19 anbi12d ( ( 𝑟 = 𝑅𝑖 = ( *rf𝑟 ) ) → ( ( 𝑖 ∈ ( 𝑟 RingHom ( oppr𝑟 ) ) ∧ 𝑖 = 𝑖 ) ↔ ( ∈ ( 𝑅 RingHom 𝑂 ) ∧ = ) ) )
21 8 20 sbcied ( 𝑟 = 𝑅 → ( [ ( *rf𝑟 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑟 RingHom ( oppr𝑟 ) ) ∧ 𝑖 = 𝑖 ) ↔ ( ∈ ( 𝑅 RingHom 𝑂 ) ∧ = ) ) )
22 7 21 elab3 ( 𝑅 ∈ { 𝑟[ ( *rf𝑟 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑟 RingHom ( oppr𝑟 ) ) ∧ 𝑖 = 𝑖 ) } ↔ ( ∈ ( 𝑅 RingHom 𝑂 ) ∧ = ) )
23 4 22 bitri ( 𝑅 ∈ *-Ring ↔ ( ∈ ( 𝑅 RingHom 𝑂 ) ∧ = ) )