Theorem ringurd

Description: Deduce the unity element of a ring from its properties. (Contributed by Thierry Arnoux, 6-Sep-2016)

	Ref	Expression
Hypotheses	ringurd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
	ringurd.p	⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
	ringurd.z	⊢ ( 𝜑 → 1 ∈ 𝐵 )
	ringurd.i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
	ringurd.j	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · 1 ) = 𝑥 )
Assertion	ringurd	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ringurd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
2		ringurd.p	⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
3		ringurd.z	⊢ ( 𝜑 → 1 ∈ 𝐵 )
4		ringurd.i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
5		ringurd.j	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · 1 ) = 𝑥 )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
9	6 7 8	dfur2	⊢ ( 1r ‘ 𝑅 ) = ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) )
10	3 1	eleqtrd	⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝑅 ) )
11	4 5	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) )
12	11	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) )
13	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → · = ( .r ‘ 𝑅 ) )
14	13	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) = ( 1 ( .r ‘ 𝑅 ) 𝑥 ) )
15	14	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
16	13	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · 1 ) = ( 𝑥 ( .r ‘ 𝑅 ) 1 ) )
17	16	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 · 1 ) = 𝑥 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 ) )
18	15 17	anbi12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) ↔ ( ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 ) ) )
19	1 18	raleqbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 ) ) )
20	12 19	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 ) )
21	1	eleq2d	⊢ ( 𝜑 → ( 𝑒 ∈ 𝐵 ↔ 𝑒 ∈ ( Base ‘ 𝑅 ) ) )
22	13	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑒 · 𝑥 ) = ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) )
23	22	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑒 · 𝑥 ) = 𝑥 ↔ ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
24	13	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · 𝑒 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) )
25	24	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 · 𝑒 ) = 𝑥 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) )
26	23 25	anbi12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ↔ ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) )
27	1 26	raleqbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) )
28	21 27	anbi12d	⊢ ( 𝜑 → ( ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ↔ ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) ) )
29	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → 𝑒 ∈ 𝐵 )
32		simpr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑥 = 𝑒 ) → 𝑥 = 𝑒 )
33	32	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑥 = 𝑒 ) → ( 1 · 𝑥 ) = ( 1 · 𝑒 ) )
34	33 32	eqeq12d	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑥 = 𝑒 ) → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( 1 · 𝑒 ) = 𝑒 ) )
35	31 34	rspcdv	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 1 · 𝑥 ) = 𝑥 → ( 1 · 𝑒 ) = 𝑒 ) )
36	30 35	mpd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( 1 · 𝑒 ) = 𝑒 )
37	36	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) → ( 1 · 𝑒 ) = 𝑒 )
38	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) → 1 ∈ 𝐵 )
39		simprr	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) )
40		oveq2	⊢ ( 𝑥 = 1 → ( 𝑒 · 𝑥 ) = ( 𝑒 · 1 ) )
41		id	⊢ ( 𝑥 = 1 → 𝑥 = 1 )
42	40 41	eqeq12d	⊢ ( 𝑥 = 1 → ( ( 𝑒 · 𝑥 ) = 𝑥 ↔ ( 𝑒 · 1 ) = 1 ) )
43		oveq1	⊢ ( 𝑥 = 1 → ( 𝑥 · 𝑒 ) = ( 1 · 𝑒 ) )
44	43 41	eqeq12d	⊢ ( 𝑥 = 1 → ( ( 𝑥 · 𝑒 ) = 𝑥 ↔ ( 1 · 𝑒 ) = 1 ) )
45	42 44	anbi12d	⊢ ( 𝑥 = 1 → ( ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ↔ ( ( 𝑒 · 1 ) = 1 ∧ ( 1 · 𝑒 ) = 1 ) ) )
46	45	rspcva	⊢ ( ( 1 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) → ( ( 𝑒 · 1 ) = 1 ∧ ( 1 · 𝑒 ) = 1 ) )
47	46	simprd	⊢ ( ( 1 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) → ( 1 · 𝑒 ) = 1 )
48	38 39 47	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) → ( 1 · 𝑒 ) = 1 )
49	37 48	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) → 𝑒 = 1 )
50	49	ex	⊢ ( 𝜑 → ( ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) → 𝑒 = 1 ) )
51	28 50	sylbird	⊢ ( 𝜑 → ( ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) → 𝑒 = 1 ) )
52	51	alrimiv	⊢ ( 𝜑 → ∀ 𝑒 ( ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) → 𝑒 = 1 ) )
53		eleq1	⊢ ( 𝑒 = 1 → ( 𝑒 ∈ ( Base ‘ 𝑅 ) ↔ 1 ∈ ( Base ‘ 𝑅 ) ) )
54		oveq1	⊢ ( 𝑒 = 1 → ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1 ( .r ‘ 𝑅 ) 𝑥 ) )
55	54	eqeq1d	⊢ ( 𝑒 = 1 → ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ↔ ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
56	55	ovanraleqv	⊢ ( 𝑒 = 1 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 ) ) )
57	53 56	anbi12d	⊢ ( 𝑒 = 1 → ( ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) ↔ ( 1 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 ) ) ) )
58	57	eqeu	⊢ ( ( 1 ∈ ( Base ‘ 𝑅 ) ∧ ( 1 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 ) ) ∧ ∀ 𝑒 ( ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) → 𝑒 = 1 ) ) → ∃! 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) )
59	10 10 20 52 58	syl121anc	⊢ ( 𝜑 → ∃! 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) )
60	57	iota2	⊢ ( ( 1 ∈ 𝐵 ∧ ∃! 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) ) → ( ( 1 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 ) ) ↔ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) ) = 1 ) )
61	3 59 60	syl2anc	⊢ ( 𝜑 → ( ( 1 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 1 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 ) ) ↔ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) ) = 1 ) )
62	10 20 61	mpbi2and	⊢ ( 𝜑 → ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑒 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑒 ) = 𝑥 ) ) ) = 1 )
63	9 62	eqtr2id	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑅 ) )