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 ⊢ ∗ ˙ = ∗ 𝑟𝑓 ⁡ R
srngf1o.b ⊢ B = Base R
Assertion srngf1o ⊢ R ∈ *-Ring → ∗ ˙ : B ⟶ 1-1 onto B

Proof

Step Hyp Ref Expression
1 srngcnv.i ⊢ ∗ ˙ = ∗ 𝑟𝑓 ⁡ R
2 srngf1o.b ⊢ B = Base R
3 eqid ⊢ opp r ⁡ R = opp r ⁡ R
4 3 1 srngrhm ⊢ R ∈ *-Ring → ∗ ˙ ∈ R RingHom opp r ⁡ R
5 eqid ⊢ Base opp r ⁡ R = Base opp r ⁡ R
6 2 5 rhmf ⊢ ∗ ˙ ∈ R RingHom opp r ⁡ R → ∗ ˙ : B ⟶ Base opp r ⁡ R
7 ffn ⊢ ∗ ˙ : B ⟶ Base opp r ⁡ R → ∗ ˙ Fn B
8 4 6 7 3syl ⊢ R ∈ *-Ring → ∗ ˙ Fn B
9 1 srngcnv ⊢ R ∈ *-Ring → ∗ ˙ = ∗ ˙ -1
10 9 fneq1d ⊢ R ∈ *-Ring → ∗ ˙ Fn B ↔ ∗ ˙ -1 Fn B
11 8 10 mpbid ⊢ R ∈ *-Ring → ∗ ˙ -1 Fn B
12 dff1o4 ⊢ ∗ ˙ : B ⟶ 1-1 onto B ↔ ∗ ˙ Fn B ∧ ∗ ˙ -1 Fn B
13 8 11 12 sylanbrc ⊢ R ∈ *-Ring → ∗ ˙ : B ⟶ 1-1 onto B