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

Metamath Proof Explorer

Theorem srng1

Description: The conjugate of the ring identity is the identity. (This is sometimes taken as an axiom, and indeed the proof here follows because we defined *r to be a ring homomorphism, which preserves 1; nevertheless, it is redundant, as can be seen from the proof of issrngd .) (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses srng1.i ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
srng1.t ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion srng1 ( 𝑅 ∈ *-Ring → ( ∗ ‘ 1 ) = 1 )

Proof

Step Hyp Ref Expression
1 srng1.i ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
2 srng1.t ⊢ 1 = ( 1r ‘ 𝑅 )
3 srngring ⊢ ( 𝑅 ∈ *-Ring → 𝑅 ∈ Ring )
4 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 4 2 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
6 eqid ⊢ ( *rf ‘ 𝑅 ) = ( *rf ‘ 𝑅 )
7 4 1 6 stafval ⊢ ( 1 ∈ ( Base ‘ 𝑅 ) → ( ( *rf ‘ 𝑅 ) ‘ 1 ) = ( ∗ ‘ 1 ) )
8 3 5 7 3syl ⊢ ( 𝑅 ∈ *-Ring → ( ( *rf ‘ 𝑅 ) ‘ 1 ) = ( ∗ ‘ 1 ) )
9 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
10 9 6 srngrhm ⊢ ( 𝑅 ∈ *-Ring → ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) )
11 9 2 oppr1 ⊢ 1 = ( 1r ‘ ( oppr ‘ 𝑅 ) )
12 2 11 rhm1 ⊢ ( ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) → ( ( *rf ‘ 𝑅 ) ‘ 1 ) = 1 )
13 10 12 syl ⊢ ( 𝑅 ∈ *-Ring → ( ( *rf ‘ 𝑅 ) ‘ 1 ) = 1 )
14 8 13 eqtr3d ⊢ ( 𝑅 ∈ *-Ring → ( ∗ ‘ 1 ) = 1 )