Theorem rngoideu 33934

Description: The unit element of a ring is unique. (Contributed by NM, 4-Apr-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ringi.1	⊢ 𝐺 = (1st ‘𝑅)
ringi.2	⊢ 𝐻 = (2nd ‘𝑅)
ringi.3	⊢ 𝑋 = ran 𝐺

Assertion

Ref	Expression
rngoideu	⊢ (𝑅 ∈ RingOps → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))

Distinct variable groups:   𝑥,𝑢,𝐺   𝑢,𝐻,𝑥   𝑢,𝑋,𝑥   𝑢,𝑅,𝑥

Proof of Theorem rngoideu

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ringi.1	. . . . 5 ⊢ 𝐺 = (1st ‘𝑅)
2		ringi.2	. . . . 5 ⊢ 𝐻 = (2nd ‘𝑅)
3		ringi.3	. . . . 5 ⊢ 𝑋 = ran 𝐺
4	1, 2, 3	rngoi 33930	. . . 4 ⊢ (𝑅 ∈ RingOps → ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑢𝐻𝑥)𝐻𝑦) = (𝑢𝐻(𝑥𝐻𝑦)) ∧ (𝑢𝐻(𝑥𝐺𝑦)) = ((𝑢𝐻𝑥)𝐺(𝑢𝐻𝑦)) ∧ ((𝑢𝐺𝑥)𝐻𝑦) = ((𝑢𝐻𝑦)𝐺(𝑥𝐻𝑦))) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))))
5	4	simprrd 814	. . 3 ⊢ (𝑅 ∈ RingOps → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))
6		simpl 474	. . . . . . . 8 ⊢ (((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) → (𝑢𝐻𝑥) = 𝑥)
7	6	ralimi 3054	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) → ∀𝑥 ∈ 𝑋 (𝑢𝐻𝑥) = 𝑥)
8		oveq2 6773	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑢𝐻𝑥) = (𝑢𝐻𝑦))
9		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
10	8, 9	eqeq12d 2739	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑢𝐻𝑥) = 𝑥 ↔ (𝑢𝐻𝑦) = 𝑦))
11	10	rspcv 3409	. . . . . . 7 ⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑢𝐻𝑥) = 𝑥 → (𝑢𝐻𝑦) = 𝑦))
12	7, 11	syl5 34	. . . . . 6 ⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) → (𝑢𝐻𝑦) = 𝑦))
13		simpr 479	. . . . . . . 8 ⊢ (((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥) → (𝑥𝐻𝑦) = 𝑥)
14	13	ralimi 3054	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥) → ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑦) = 𝑥)
15		oveq1 6772	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (𝑥𝐻𝑦) = (𝑢𝐻𝑦))
16		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → 𝑥 = 𝑢)
17	15, 16	eqeq12d 2739	. . . . . . . 8 ⊢ (𝑥 = 𝑢 → ((𝑥𝐻𝑦) = 𝑥 ↔ (𝑢𝐻𝑦) = 𝑢))
18	17	rspcv 3409	. . . . . . 7 ⊢ (𝑢 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑦) = 𝑥 → (𝑢𝐻𝑦) = 𝑢))
19	14, 18	syl5 34	. . . . . 6 ⊢ (𝑢 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥) → (𝑢𝐻𝑦) = 𝑢))
20	12, 19	im2anan9r 917	. . . . 5 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → ((𝑢𝐻𝑦) = 𝑦 ∧ (𝑢𝐻𝑦) = 𝑢)))
21		eqtr2 2744	. . . . . 6 ⊢ (((𝑢𝐻𝑦) = 𝑦 ∧ (𝑢𝐻𝑦) = 𝑢) → 𝑦 = 𝑢)
22	21	eqcomd 2730	. . . . 5 ⊢ (((𝑢𝐻𝑦) = 𝑦 ∧ (𝑢𝐻𝑦) = 𝑢) → 𝑢 = 𝑦)
23	20, 22	syl6 35	. . . 4 ⊢ ((𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦))
24	23	rgen2a 3079	. . 3 ⊢ ∀𝑢 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦)
25	5, 24	jctir 562	. 2 ⊢ (𝑅 ∈ RingOps → (∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑢 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦)))
26		oveq1 6772	. . . . . 6 ⊢ (𝑢 = 𝑦 → (𝑢𝐻𝑥) = (𝑦𝐻𝑥))
27	26	eqeq1d 2726	. . . . 5 ⊢ (𝑢 = 𝑦 → ((𝑢𝐻𝑥) = 𝑥 ↔ (𝑦𝐻𝑥) = 𝑥))
28		oveq2 6773	. . . . . 6 ⊢ (𝑢 = 𝑦 → (𝑥𝐻𝑢) = (𝑥𝐻𝑦))
29	28	eqeq1d 2726	. . . . 5 ⊢ (𝑢 = 𝑦 → ((𝑥𝐻𝑢) = 𝑥 ↔ (𝑥𝐻𝑦) = 𝑥))
30	27, 29	anbi12d 749	. . . 4 ⊢ (𝑢 = 𝑦 → (((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)))
31	30	ralbidv 3088	. . 3 ⊢ (𝑢 = 𝑦 → (∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)))
32	31	reu4 3506	. 2 ⊢ (∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ (∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑢 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦)))
33	25, 32	sylibr 224	1 ⊢ (𝑅 ∈ RingOps → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥))

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1596   ∈ wcel 2103  ∀wral 3014  ∃wrex 3015  ∃!wreu 3016   × cxp 5216  ran crn 5219  ⟶wf 5997  ‘cfv 6001  (class class class)co 6765  1^st c1st 7283  2^nd c2nd 7284  AbelOpcablo 27628  RingOpscrngo 33925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-fv 6009  df-ov 6768  df-1st 7285  df-2nd 7286  df-rngo 33926

This theorem is referenced by: (None)