Theorem 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	$$⊢\phi \to B={\mathrm{Base}}_K$$
	rngidpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	rngidpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
Assertion	rngidpropd	$$⊢\phi \to 1_K=1_L$$

Proof

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