Metamath Proof Explorer


Theorem srngcl

Description: The involution function in a star ring is closed in the ring. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses srngcl.i = ( *𝑟𝑅 )
srngcl.b 𝐵 = ( Base ‘ 𝑅 )
Assertion srngcl ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵 ) → ( 𝑋 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 srngcl.i = ( *𝑟𝑅 )
2 srngcl.b 𝐵 = ( Base ‘ 𝑅 )
3 eqid ( *rf𝑅 ) = ( *rf𝑅 )
4 2 1 3 stafval ( 𝑋𝐵 → ( ( *rf𝑅 ) ‘ 𝑋 ) = ( 𝑋 ) )
5 4 adantl ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵 ) → ( ( *rf𝑅 ) ‘ 𝑋 ) = ( 𝑋 ) )
6 3 2 srngf1o ( 𝑅 ∈ *-Ring → ( *rf𝑅 ) : 𝐵1-1-onto𝐵 )
7 f1of ( ( *rf𝑅 ) : 𝐵1-1-onto𝐵 → ( *rf𝑅 ) : 𝐵𝐵 )
8 6 7 syl ( 𝑅 ∈ *-Ring → ( *rf𝑅 ) : 𝐵𝐵 )
9 8 ffvelrnda ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵 ) → ( ( *rf𝑅 ) ‘ 𝑋 ) ∈ 𝐵 )
10 5 9 eqeltrrd ( ( 𝑅 ∈ *-Ring ∧ 𝑋𝐵 ) → ( 𝑋 ) ∈ 𝐵 )