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	$⊢ \underset{˙}{} = _{R}$
	srng1.t	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	srng1	$⊢ R \in -Ring \to \underset{˙}{} (\underset{˙}{1}) = \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		srng1.i	$⊢ \underset{˙}{} = _{R}$
2		srng1.t	$⊢ \underset{˙}{1} = 1_{R}$
3		srngring	$⊢ R \in *-Ring \to R \in Ring$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	4 2	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
6		eqid	$⊢ _{𝑟𝑓} (R) = _{𝑟𝑓} (R)$
7	4 1 6	stafval	$⊢ \underset{˙}{1} \in {Base}_{R} \to _{𝑟𝑓} (R) (\underset{˙}{1}) = \underset{˙}{} (\underset{˙}{1})$
8	3 5 7	3syl	$⊢ R \in -Ring \to _{𝑟𝑓} (R) (\underset{˙}{1}) = \underset{˙}{*} (\underset{˙}{1})$
9		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
10	9 6	srngrhm	$⊢ R \in -Ring \to _{𝑟𝑓} (R) \in (R RingHom {opp}_{r} (R))$
11	9 2	oppr1	$⊢ \underset{˙}{1} = 1_{{opp}_{r} (R)}$
12	2 11	rhm1	$⊢ _{𝑟𝑓} (R) \in (R RingHom {opp}_{r} (R)) \to _{𝑟𝑓} (R) (\underset{˙}{1}) = \underset{˙}{1}$
13	10 12	syl	$⊢ R \in -Ring \to _{𝑟𝑓} (R) (\underset{˙}{1}) = \underset{˙}{1}$
14	8 13	eqtr3d	$⊢ R \in -Ring \to \underset{˙}{} (\underset{˙}{1}) = \underset{˙}{1}$

Metamath Proof Explorer

Theorem srng1

Proof