rngidpropd

Description: The ring unity depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014)

	Ref	Expression
Hypotheses	rngidpropd.1	$⊢ φ \to B = {Base}_{K}$
	rngidpropd.2	$⊢ φ \to B = {Base}_{L}$
	rngidpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
Assertion	rngidpropd	$⊢ φ \to 1_{K} = 1_{L}$

Step	Hyp	Ref	Expression
1		rngidpropd.1	$⊢ φ \to B = {Base}_{K}$
2		rngidpropd.2	$⊢ φ \to B = {Base}_{L}$
3		rngidpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
4		eqid	$⊢ {mulGrp}_{K} = {mulGrp}_{K}$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6	4 5	mgpbas	$⊢ {Base}_{K} = {Base}_{{mulGrp}_{K}}$
7	1 6	eqtrdi	$⊢ φ \to B = {Base}_{{mulGrp}_{K}}$
8		eqid	$⊢ {mulGrp}_{L} = {mulGrp}_{L}$
9		eqid	$⊢ {Base}_{L} = {Base}_{L}$
10	8 9	mgpbas	$⊢ {Base}_{L} = {Base}_{{mulGrp}_{L}}$
11	2 10	eqtrdi	$⊢ φ \to B = {Base}_{{mulGrp}_{L}}$
12		eqid	$⊢ \cdot_{K} = \cdot_{K}$
13	4 12	mgpplusg	$⊢ \cdot_{K} = +_{{mulGrp}_{K}}$
14	13	oveqi	$⊢ x \cdot_{K} y = x +_{{mulGrp}_{K}} y$
15		eqid	$⊢ \cdot_{L} = \cdot_{L}$
16	8 15	mgpplusg	$⊢ \cdot_{L} = +_{{mulGrp}_{L}}$
17	16	oveqi	$⊢ x \cdot_{L} y = x +_{{mulGrp}_{L}} y$
18	3 14 17	3eqtr3g	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{{mulGrp}_{K}} y = x +_{{mulGrp}_{L}} y$
19	7 11 18	grpidpropd	$⊢ φ \to 0_{{mulGrp}_{K}} = 0_{{mulGrp}_{L}}$
20		eqid	$⊢ 1_{K} = 1_{K}$
21	4 20	ringidval	$⊢ 1_{K} = 0_{{mulGrp}_{K}}$
22		eqid	$⊢ 1_{L} = 1_{L}$
23	8 22	ringidval	$⊢ 1_{L} = 0_{{mulGrp}_{L}}$
24	19 21 23	3eqtr4g	$⊢ φ \to 1_{K} = 1_{L}$

Metamath Proof Explorer