Description: The involution function in a star ring is its own inverse function. (Contributed by Mario Carneiro, 6-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | srngcnv.i | ⊢ ∗ = ( *_{rf} ‘ 𝑅 ) | |
Assertion | srngcnv | ⊢ ( 𝑅 ∈ *-Ring → ∗ = ^{◡} ∗ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | srngcnv.i | ⊢ ∗ = ( *_{rf} ‘ 𝑅 ) | |
2 | eqid | ⊢ ( opp_{r} ‘ 𝑅 ) = ( opp_{r} ‘ 𝑅 ) | |
3 | 2 1 | issrng | ⊢ ( 𝑅 ∈ *-Ring ↔ ( ∗ ∈ ( 𝑅 RingHom ( opp_{r} ‘ 𝑅 ) ) ∧ ∗ = ^{◡} ∗ ) ) |
4 | 3 | simprbi | ⊢ ( 𝑅 ∈ *-Ring → ∗ = ^{◡} ∗ ) |