Metamath Proof Explorer

Theorem urpropd

Description: Sufficient condition for ring unities to be equal. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses urpropd.b ⊢ B = Base S
urpropd.s ⊢ φ → S ∈ V
urpropd.t ⊢ φ → T ∈ W
urpropd.1 ⊢ φ → B = Base T
urpropd.2 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ S y = x ⋅ T y
Assertion urpropd ⊢ φ → 1 S = 1 T

Proof

Step Hyp Ref Expression
1 urpropd.b ⊢ B = Base S
2 urpropd.s ⊢ φ → S ∈ V
3 urpropd.t ⊢ φ → T ∈ W
4 urpropd.1 ⊢ φ → B = Base T
5 urpropd.2 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ S y = x ⋅ T y
6 4 adantr ⊢ φ ∧ e ∈ B → B = Base T
7 5 anasss ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ S y = x ⋅ T y
8 7 ralrimivva ⊢ φ → ∀ x ∈ B ∀ y ∈ B x ⋅ S y = x ⋅ T y
9 8 ad2antrr ⊢ φ ∧ e ∈ B ∧ p ∈ B → ∀ x ∈ B ∀ y ∈ B x ⋅ S y = x ⋅ T y
10 oveq1 ⊢ x = e → x ⋅ S y = e ⋅ S y
11 oveq1 ⊢ x = e → x ⋅ T y = e ⋅ T y
12 10 11 eqeq12d ⊢ x = e → x ⋅ S y = x ⋅ T y ↔ e ⋅ S y = e ⋅ T y
13 oveq2 ⊢ y = p → e ⋅ S y = e ⋅ S p
14 oveq2 ⊢ y = p → e ⋅ T y = e ⋅ T p
15 13 14 eqeq12d ⊢ y = p → e ⋅ S y = e ⋅ T y ↔ e ⋅ S p = e ⋅ T p
16 simplr ⊢ φ ∧ e ∈ B ∧ p ∈ B → e ∈ B
17 eqidd ⊢ φ ∧ e ∈ B ∧ p ∈ B ∧ x = e → B = B
18 simpr ⊢ φ ∧ e ∈ B ∧ p ∈ B → p ∈ B
19 12 15 16 17 18 rspc2vd ⊢ φ ∧ e ∈ B ∧ p ∈ B → ∀ x ∈ B ∀ y ∈ B x ⋅ S y = x ⋅ T y → e ⋅ S p = e ⋅ T p
20 9 19 mpd ⊢ φ ∧ e ∈ B ∧ p ∈ B → e ⋅ S p = e ⋅ T p
21 20 eqeq1d ⊢ φ ∧ e ∈ B ∧ p ∈ B → e ⋅ S p = p ↔ e ⋅ T p = p
22 oveq1 ⊢ x = p → x ⋅ S y = p ⋅ S y
23 oveq1 ⊢ x = p → x ⋅ T y = p ⋅ T y
24 22 23 eqeq12d ⊢ x = p → x ⋅ S y = x ⋅ T y ↔ p ⋅ S y = p ⋅ T y
25 oveq2 ⊢ y = e → p ⋅ S y = p ⋅ S e
26 oveq2 ⊢ y = e → p ⋅ T y = p ⋅ T e
27 25 26 eqeq12d ⊢ y = e → p ⋅ S y = p ⋅ T y ↔ p ⋅ S e = p ⋅ T e
28 eqidd ⊢ φ ∧ e ∈ B ∧ p ∈ B ∧ x = p → B = B
29 24 27 18 28 16 rspc2vd ⊢ φ ∧ e ∈ B ∧ p ∈ B → ∀ x ∈ B ∀ y ∈ B x ⋅ S y = x ⋅ T y → p ⋅ S e = p ⋅ T e
30 9 29 mpd ⊢ φ ∧ e ∈ B ∧ p ∈ B → p ⋅ S e = p ⋅ T e
31 30 eqeq1d ⊢ φ ∧ e ∈ B ∧ p ∈ B → p ⋅ S e = p ↔ p ⋅ T e = p
32 21 31 anbi12d ⊢ φ ∧ e ∈ B ∧ p ∈ B → e ⋅ S p = p ∧ p ⋅ S e = p ↔ e ⋅ T p = p ∧ p ⋅ T e = p
33 6 32 raleqbidva ⊢ φ ∧ e ∈ B → ∀ p ∈ B e ⋅ S p = p ∧ p ⋅ S e = p ↔ ∀ p ∈ Base T e ⋅ T p = p ∧ p ⋅ T e = p
34 33 pm5.32da ⊢ φ → e ∈ B ∧ ∀ p ∈ B e ⋅ S p = p ∧ p ⋅ S e = p ↔ e ∈ B ∧ ∀ p ∈ Base T e ⋅ T p = p ∧ p ⋅ T e = p
35 4 eleq2d ⊢ φ → e ∈ B ↔ e ∈ Base T
36 35 anbi1d ⊢ φ → e ∈ B ∧ ∀ p ∈ Base T e ⋅ T p = p ∧ p ⋅ T e = p ↔ e ∈ Base T ∧ ∀ p ∈ Base T e ⋅ T p = p ∧ p ⋅ T e = p
37 34 36 bitrd ⊢ φ → e ∈ B ∧ ∀ p ∈ B e ⋅ S p = p ∧ p ⋅ S e = p ↔ e ∈ Base T ∧ ∀ p ∈ Base T e ⋅ T p = p ∧ p ⋅ T e = p
38 37 iotabidv ⊢ φ → ι e | e ∈ B ∧ ∀ p ∈ B e ⋅ S p = p ∧ p ⋅ S e = p = ι e | e ∈ Base T ∧ ∀ p ∈ Base T e ⋅ T p = p ∧ p ⋅ T e = p
39 eqid ⊢ mulGrp S = mulGrp S
40 39 1 mgpbas ⊢ B = Base mulGrp S
41 eqid ⊢ ⋅ S = ⋅ S
42 39 41 mgpplusg ⊢ ⋅ S = + mulGrp S
43 eqid ⊢ 0 mulGrp S = 0 mulGrp S
44 40 42 43 grpidval ⊢ 0 mulGrp S = ι e | e ∈ B ∧ ∀ p ∈ B e ⋅ S p = p ∧ p ⋅ S e = p
45 eqid ⊢ mulGrp T = mulGrp T
46 eqid ⊢ Base T = Base T
47 45 46 mgpbas ⊢ Base T = Base mulGrp T
48 eqid ⊢ ⋅ T = ⋅ T
49 45 48 mgpplusg ⊢ ⋅ T = + mulGrp T
50 eqid ⊢ 0 mulGrp T = 0 mulGrp T
51 47 49 50 grpidval ⊢ 0 mulGrp T = ι e | e ∈ Base T ∧ ∀ p ∈ Base T e ⋅ T p = p ∧ p ⋅ T e = p
52 38 44 51 3eqtr4g ⊢ φ → 0 mulGrp S = 0 mulGrp T
53 eqid ⊢ 1 S = 1 S
54 39 53 ringidval ⊢ 1 S = 0 mulGrp S
55 eqid ⊢ 1 T = 1 T
56 45 55 ringidval ⊢ 1 T = 0 mulGrp T
57 52 54 56 3eqtr4g ⊢ φ → 1 S = 1 T