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→ 𝐵 )