Theorem recrng

Description: The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019)

	Ref	Expression
Assertion	recrng	⊢ ℝfld ∈ *-Ring

Proof

Step	Hyp	Ref	Expression
1		rebase	⊢ ℝ = ( Base ‘ ℝfld )
2		refldcj	⊢ ∗ = ( *𝑟 ‘ ℝfld )
3		refld	⊢ ℝfld ∈ Field
4		isfld	⊢ ( ℝfld ∈ Field ↔ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) )
5	3 4	mpbi	⊢ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing )
6	5	simpri	⊢ ℝfld ∈ CRing
7	6	a1i	⊢ ( ⊤ → ℝfld ∈ CRing )
8		cjre	⊢ ( 𝑥 ∈ ℝ → ( ∗ ‘ 𝑥 ) = 𝑥 )
9	8	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( ∗ ‘ 𝑥 ) = 𝑥 )
10	1 2 7 9	idsrngd	⊢ ( ⊤ → ℝfld ∈ *-Ring )
11	10	mptru	⊢ ℝfld ∈ *-Ring