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	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	rngidpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	rngidpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
Assertion	rngidpropd	⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		rngidpropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		rngidpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		rngidpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
4		eqid	⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
5		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6	4 5	mgpbas	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
7	1 6	eqtrdi	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
8		eqid	⊢ ( mulGrp ‘ 𝐿 ) = ( mulGrp ‘ 𝐿 )
9		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
10	8 9	mgpbas	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ ( mulGrp ‘ 𝐿 ) )
11	2 10	eqtrdi	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐿 ) ) )
12		eqid	⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
13	4 12	mgpplusg	⊢ ( .r ‘ 𝐾 ) = ( +g ‘ ( mulGrp ‘ 𝐾 ) )
14	13	oveqi	⊢ ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 )
15		eqid	⊢ ( .r ‘ 𝐿 ) = ( .r ‘ 𝐿 )
16	8 15	mgpplusg	⊢ ( .r ‘ 𝐿 ) = ( +g ‘ ( mulGrp ‘ 𝐿 ) )
17	16	oveqi	⊢ ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐿 ) ) 𝑦 )
18	3 14 17	3eqtr3g	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐿 ) ) 𝑦 ) )
19	7 11 18	grpidpropd	⊢ ( 𝜑 → ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) = ( 0g ‘ ( mulGrp ‘ 𝐿 ) ) )
20		eqid	⊢ ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐾 )
21	4 20	ringidval	⊢ ( 1r ‘ 𝐾 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) )
22		eqid	⊢ ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐿 )
23	8 22	ringidval	⊢ ( 1r ‘ 𝐿 ) = ( 0g ‘ ( mulGrp ‘ 𝐿 ) )
24	19 21 23	3eqtr4g	⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐿 ) )