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	$⊢ φ \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	unitpropd	$⊢ φ \to Unit (K) = Unit (L)$

Proof

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	1 2 3	rngidpropd	$⊢ φ \to 1_{K} = 1_{L}$
5	4	breq2d	$⊢ φ \to (z ∥_{r} (K) 1_{K} \leftrightarrow z ∥_{r} (K) 1_{L})$
6	4	breq2d	$⊢ φ \to (z ∥_{r} ({opp}_{r} (K)) 1_{K} \leftrightarrow z ∥_{r} ({opp}_{r} (K)) 1_{L})$
7	5 6	anbi12d	$⊢ φ \to ((z ∥_{r} (K) 1_{K} \land z ∥_{r} ({opp}_{r} (K)) 1_{K}) \leftrightarrow (z ∥_{r} (K) 1_{L} \land z ∥_{r} ({opp}_{r} (K)) 1_{L}))$
8	1 2 3	dvdsrpropd	$⊢ φ \to ∥_{r} (K) = ∥_{r} (L)$
9	8	breqd	$⊢ φ \to (z ∥_{r} (K) 1_{L} \leftrightarrow z ∥_{r} (L) 1_{L})$
10		eqid	$⊢ {opp}_{r} (K) = {opp}_{r} (K)$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	10 11	opprbas	$⊢ {Base}_{K} = {Base}_{{opp}_{r} (K)}$
13	1 12	syl6eq	$⊢ φ \to B = {Base}_{{opp}_{r} (K)}$
14		eqid	$⊢ {opp}_{r} (L) = {opp}_{r} (L)$
15		eqid	$⊢ {Base}_{L} = {Base}_{L}$
16	14 15	opprbas	$⊢ {Base}_{L} = {Base}_{{opp}_{r} (L)}$
17	2 16	syl6eq	$⊢ φ \to B = {Base}_{{opp}_{r} (L)}$
18	3	ancom2s	$⊢ (φ \land (y \in B \land x \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
19		eqid	$⊢ \cdot_{K} = \cdot_{K}$
20		eqid	$⊢ \cdot_{{opp}_{r} (K)} = \cdot_{{opp}_{r} (K)}$
21	11 19 10 20	opprmul	$⊢ y \cdot_{{opp}_{r} (K)} x = x \cdot_{K} y$
22		eqid	$⊢ \cdot_{L} = \cdot_{L}$
23		eqid	$⊢ \cdot_{{opp}_{r} (L)} = \cdot_{{opp}_{r} (L)}$
24	15 22 14 23	opprmul	$⊢ y \cdot_{{opp}_{r} (L)} x = x \cdot_{L} y$
25	18 21 24	3eqtr4g	$⊢ (φ \land (y \in B \land x \in B)) \to y \cdot_{{opp}_{r} (K)} x = y \cdot_{{opp}_{r} (L)} x$
26	13 17 25	dvdsrpropd	$⊢ φ \to ∥_{r} ({opp}_{r} (K)) = ∥_{r} ({opp}_{r} (L))$
27	26	breqd	$⊢ φ \to (z ∥_{r} ({opp}_{r} (K)) 1_{L} \leftrightarrow z ∥_{r} ({opp}_{r} (L)) 1_{L})$
28	9 27	anbi12d	$⊢ φ \to ((z ∥_{r} (K) 1_{L} \land z ∥_{r} ({opp}_{r} (K)) 1_{L}) \leftrightarrow (z ∥_{r} (L) 1_{L} \land z ∥_{r} ({opp}_{r} (L)) 1_{L}))$
29	7 28	bitrd	$⊢ φ \to ((z ∥_{r} (K) 1_{K} \land z ∥_{r} ({opp}_{r} (K)) 1_{K}) \leftrightarrow (z ∥_{r} (L) 1_{L} \land z ∥_{r} ({opp}_{r} (L)) 1_{L}))$
30		eqid	$⊢ Unit (K) = Unit (K)$
31		eqid	$⊢ 1_{K} = 1_{K}$
32		eqid	$⊢ ∥_{r} (K) = ∥_{r} (K)$
33		eqid	$⊢ ∥_{r} ({opp}_{r} (K)) = ∥_{r} ({opp}_{r} (K))$
34	30 31 32 10 33	isunit	$⊢ z \in Unit (K) \leftrightarrow (z ∥_{r} (K) 1_{K} \land z ∥_{r} ({opp}_{r} (K)) 1_{K})$
35		eqid	$⊢ Unit (L) = Unit (L)$
36		eqid	$⊢ 1_{L} = 1_{L}$
37		eqid	$⊢ ∥_{r} (L) = ∥_{r} (L)$
38		eqid	$⊢ ∥_{r} ({opp}_{r} (L)) = ∥_{r} ({opp}_{r} (L))$
39	35 36 37 14 38	isunit	$⊢ z \in Unit (L) \leftrightarrow (z ∥_{r} (L) 1_{L} \land z ∥_{r} ({opp}_{r} (L)) 1_{L})$
40	29 34 39	3bitr4g	$⊢ φ \to (z \in Unit (K) \leftrightarrow z \in Unit (L))$
41	40	eqrdv	$⊢ φ \to Unit (K) = Unit (L)$

Metamath Proof Explorer

Theorem unitpropd

Proof