This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem srngf1o

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

Ref Expression
Hypotheses srngcnv.i ⊢ ∗ = ( *rf ‘ 𝑅 )
srngf1o.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion srngf1o ( 𝑅 ∈ *-Ring → ∗ : 𝐵 –1-1-onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 srngcnv.i ⊢ ∗ = ( *rf ‘ 𝑅 )
2 srngf1o.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
4 3 1 srngrhm ⊢ ( 𝑅 ∈ *-Ring → ∗ ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) )
5 eqid ⊢ ( Base ‘ ( oppr ‘ 𝑅 ) ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
6 2 5 rhmf ⊢ ( ∗ ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) → ∗ : 𝐵 ⟶ ( Base ‘ ( oppr ‘ 𝑅 ) ) )
7 ffn ⊢ ( ∗ : 𝐵 ⟶ ( Base ‘ ( oppr ‘ 𝑅 ) ) → ∗ Fn 𝐵 )
8 4 6 7 3syl ⊢ ( 𝑅 ∈ *-Ring → ∗ Fn 𝐵 )
9 1 srngcnv ⊢ ( 𝑅 ∈ *-Ring → ∗ = ◡ ∗ )
10 9 fneq1d ⊢ ( 𝑅 ∈ *-Ring → ( ∗ Fn 𝐵 ↔ ◡ ∗ Fn 𝐵 ) )
11 8 10 mpbid ⊢ ( 𝑅 ∈ *-Ring → ◡ ∗ Fn 𝐵 )
12 dff1o4 ⊢ ( ∗ : 𝐵 –1-1-onto→ 𝐵 ↔ ( ∗ Fn 𝐵 ∧ ◡ ∗ Fn 𝐵 ) )
13 8 11 12 sylanbrc ⊢ ( 𝑅 ∈ *-Ring → ∗ : 𝐵 –1-1-onto→ 𝐵 )