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=BaseS
urpropd.s ⊢φ→S∈V
urpropd.t ⊢φ→T∈W
urpropd.1 ⊢φ→B=BaseT
urpropd.2 ⊢φ∧x∈B∧y∈B→x⋅Sy=x⋅Ty
Assertion urpropd ⊢φ→1S=1T

Proof

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