Theorem unitpropd

Description: The set of units 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	unitpropd	⊢ ( 𝜑 → ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		rngidpropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		rngidpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		rngidpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
4	1 2 3	rngidpropd	⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐿 ) )
5	4	breq2d	⊢ ( 𝜑 → ( 𝑧 ( ∥r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ↔ 𝑧 ( ∥r ‘ 𝐾 ) ( 1r ‘ 𝐿 ) ) )
6	4	breq2d	⊢ ( 𝜑 → ( 𝑧 ( ∥r ‘ ( oppr ‘ 𝐾 ) ) ( 1r ‘ 𝐾 ) ↔ 𝑧 ( ∥r ‘ ( oppr ‘ 𝐾 ) ) ( 1r ‘ 𝐿 ) ) )
7	5 6	anbi12d	⊢ ( 𝜑 → ( ( 𝑧 ( ∥r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ∧ 𝑧 ( ∥r ‘ ( oppr ‘ 𝐾 ) ) ( 1r ‘ 𝐾 ) ) ↔ ( 𝑧 ( ∥r ‘ 𝐾 ) ( 1r ‘ 𝐿 ) ∧ 𝑧 ( ∥r ‘ ( oppr ‘ 𝐾 ) ) ( 1r ‘ 𝐿 ) ) ) )
8	1 2 3	dvdsrpropd	⊢ ( 𝜑 → ( ∥r ‘ 𝐾 ) = ( ∥r ‘ 𝐿 ) )
9	8	breqd	⊢ ( 𝜑 → ( 𝑧 ( ∥r ‘ 𝐾 ) ( 1r ‘ 𝐿 ) ↔ 𝑧 ( ∥r ‘ 𝐿 ) ( 1r ‘ 𝐿 ) ) )
10		eqid	⊢ ( oppr ‘ 𝐾 ) = ( oppr ‘ 𝐾 )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12	10 11	opprbas	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( oppr ‘ 𝐾 ) )
13	1 12	eqtrdi	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( oppr ‘ 𝐾 ) ) )
14		eqid	⊢ ( oppr ‘ 𝐿 ) = ( oppr ‘ 𝐿 )
15		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
16	14 15	opprbas	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ ( oppr ‘ 𝐿 ) )
17	2 16	eqtrdi	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( oppr ‘ 𝐿 ) ) )
18	3	ancom2s	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
19		eqid	⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
20		eqid	⊢ ( .r ‘ ( oppr ‘ 𝐾 ) ) = ( .r ‘ ( oppr ‘ 𝐾 ) )
21	11 19 10 20	opprmul	⊢ ( 𝑦 ( .r ‘ ( oppr ‘ 𝐾 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 )
22		eqid	⊢ ( .r ‘ 𝐿 ) = ( .r ‘ 𝐿 )
23		eqid	⊢ ( .r ‘ ( oppr ‘ 𝐿 ) ) = ( .r ‘ ( oppr ‘ 𝐿 ) )
24	15 22 14 23	opprmul	⊢ ( 𝑦 ( .r ‘ ( oppr ‘ 𝐿 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 )
25	18 21 24	3eqtr4g	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝐾 ) ) 𝑥 ) = ( 𝑦 ( .r ‘ ( oppr ‘ 𝐿 ) ) 𝑥 ) )
26	13 17 25	dvdsrpropd	⊢ ( 𝜑 → ( ∥r ‘ ( oppr ‘ 𝐾 ) ) = ( ∥r ‘ ( oppr ‘ 𝐿 ) ) )
27	26	breqd	⊢ ( 𝜑 → ( 𝑧 ( ∥r ‘ ( oppr ‘ 𝐾 ) ) ( 1r ‘ 𝐿 ) ↔ 𝑧 ( ∥r ‘ ( oppr ‘ 𝐿 ) ) ( 1r ‘ 𝐿 ) ) )
28	9 27	anbi12d	⊢ ( 𝜑 → ( ( 𝑧 ( ∥r ‘ 𝐾 ) ( 1r ‘ 𝐿 ) ∧ 𝑧 ( ∥r ‘ ( oppr ‘ 𝐾 ) ) ( 1r ‘ 𝐿 ) ) ↔ ( 𝑧 ( ∥r ‘ 𝐿 ) ( 1r ‘ 𝐿 ) ∧ 𝑧 ( ∥r ‘ ( oppr ‘ 𝐿 ) ) ( 1r ‘ 𝐿 ) ) ) )
29	7 28	bitrd	⊢ ( 𝜑 → ( ( 𝑧 ( ∥r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ∧ 𝑧 ( ∥r ‘ ( oppr ‘ 𝐾 ) ) ( 1r ‘ 𝐾 ) ) ↔ ( 𝑧 ( ∥r ‘ 𝐿 ) ( 1r ‘ 𝐿 ) ∧ 𝑧 ( ∥r ‘ ( oppr ‘ 𝐿 ) ) ( 1r ‘ 𝐿 ) ) ) )
30		eqid	⊢ ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐾 )
31		eqid	⊢ ( 1r ‘ 𝐾 ) = ( 1r ‘ 𝐾 )
32		eqid	⊢ ( ∥r ‘ 𝐾 ) = ( ∥r ‘ 𝐾 )
33		eqid	⊢ ( ∥r ‘ ( oppr ‘ 𝐾 ) ) = ( ∥r ‘ ( oppr ‘ 𝐾 ) )
34	30 31 32 10 33	isunit	⊢ ( 𝑧 ∈ ( Unit ‘ 𝐾 ) ↔ ( 𝑧 ( ∥r ‘ 𝐾 ) ( 1r ‘ 𝐾 ) ∧ 𝑧 ( ∥r ‘ ( oppr ‘ 𝐾 ) ) ( 1r ‘ 𝐾 ) ) )
35		eqid	⊢ ( Unit ‘ 𝐿 ) = ( Unit ‘ 𝐿 )
36		eqid	⊢ ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐿 )
37		eqid	⊢ ( ∥r ‘ 𝐿 ) = ( ∥r ‘ 𝐿 )
38		eqid	⊢ ( ∥r ‘ ( oppr ‘ 𝐿 ) ) = ( ∥r ‘ ( oppr ‘ 𝐿 ) )
39	35 36 37 14 38	isunit	⊢ ( 𝑧 ∈ ( Unit ‘ 𝐿 ) ↔ ( 𝑧 ( ∥r ‘ 𝐿 ) ( 1r ‘ 𝐿 ) ∧ 𝑧 ( ∥r ‘ ( oppr ‘ 𝐿 ) ) ( 1r ‘ 𝐿 ) ) )
40	29 34 39	3bitr4g	⊢ ( 𝜑 → ( 𝑧 ∈ ( Unit ‘ 𝐾 ) ↔ 𝑧 ∈ ( Unit ‘ 𝐿 ) ) )
41	40	eqrdv	⊢ ( 𝜑 → ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐿 ) )