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	|- ( ph -> B = ( Base ` K ) )
	rngidpropd.2	|- ( ph -> B = ( Base ` L ) )
	rngidpropd.3	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion	rngidpropd	|- ( ph -> ( 1r ` K ) = ( 1r ` L ) )

Proof

Step	Hyp	Ref	Expression
1		rngidpropd.1	|- ( ph -> B = ( Base ` K ) )
2		rngidpropd.2	|- ( ph -> B = ( Base ` L ) )
3		rngidpropd.3	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` 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	|- ( ph -> 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	|- ( ph -> B = ( Base ` ( mulGrp ` L ) ) )
12		eqid	|- ( .r ` K ) = ( .r ` K )
13	4 12	mgpplusg	|- ( .r ` K ) = ( +g ` ( mulGrp ` K ) )
14	13	oveqi	|- ( x ( .r ` K ) y ) = ( x ( +g ` ( mulGrp ` K ) ) y )
15		eqid	|- ( .r ` L ) = ( .r ` L )
16	8 15	mgpplusg	|- ( .r ` L ) = ( +g ` ( mulGrp ` L ) )
17	16	oveqi	|- ( x ( .r ` L ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y )
18	3 14 17	3eqtr3g	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` ( mulGrp ` K ) ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y ) )
19	7 11 18	grpidpropd	|- ( ph -> ( 0g ` ( mulGrp ` K ) ) = ( 0g ` ( mulGrp ` L ) ) )
20		eqid	|- ( 1r ` K ) = ( 1r ` K )
21	4 20	ringidval	|- ( 1r ` K ) = ( 0g ` ( mulGrp ` K ) )
22		eqid	|- ( 1r ` L ) = ( 1r ` L )
23	8 22	ringidval	|- ( 1r ` L ) = ( 0g ` ( mulGrp ` L ) )
24	19 21 23	3eqtr4g	|- ( ph -> ( 1r ` K ) = ( 1r ` L ) )