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 ⊢ 𝐵 = ( Base ‘ 𝑆 )
urpropd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
urpropd.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑊 )
urpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑇 ) )
urpropd.2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) )
Assertion urpropd ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 urpropd.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 urpropd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3 urpropd.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑊 )
4 urpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑇 ) )
5 urpropd.2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) )
6 4 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝑇 ) )
7 5 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) )
8 7 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) )
9 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) )
10 oveq1 ⊢ ( 𝑥 = 𝑒 → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑒 ( .r ‘ 𝑆 ) 𝑦 ) )
11 oveq1 ⊢ ( 𝑥 = 𝑒 → ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) = ( 𝑒 ( .r ‘ 𝑇 ) 𝑦 ) )
12 10 11 eqeq12d ⊢ ( 𝑥 = 𝑒 → ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) ↔ ( 𝑒 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑒 ( .r ‘ 𝑇 ) 𝑦 ) ) )
13 oveq2 ⊢ ( 𝑦 = 𝑝 → ( 𝑒 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) )
14 oveq2 ⊢ ( 𝑦 = 𝑝 → ( 𝑒 ( .r ‘ 𝑇 ) 𝑦 ) = ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) )
15 13 14 eqeq12d ⊢ ( 𝑦 = 𝑝 → ( ( 𝑒 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑒 ( .r ‘ 𝑇 ) 𝑦 ) ↔ ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) = ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) ) )
16 simplr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑒 ∈ 𝐵 )
17 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑥 = 𝑒 ) → 𝐵 = 𝐵 )
18 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
19 12 15 16 17 18 rspc2vd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) → ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) = ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) ) )
20 9 19 mpd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) = ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) )
21 20 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) = 𝑝 ↔ ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) = 𝑝 ) )
22 oveq1 ⊢ ( 𝑥 = 𝑝 → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑝 ( .r ‘ 𝑆 ) 𝑦 ) )
23 oveq1 ⊢ ( 𝑥 = 𝑝 → ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) = ( 𝑝 ( .r ‘ 𝑇 ) 𝑦 ) )
24 22 23 eqeq12d ⊢ ( 𝑥 = 𝑝 → ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) ↔ ( 𝑝 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑝 ( .r ‘ 𝑇 ) 𝑦 ) ) )
25 oveq2 ⊢ ( 𝑦 = 𝑒 → ( 𝑝 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) )
26 oveq2 ⊢ ( 𝑦 = 𝑒 → ( 𝑝 ( .r ‘ 𝑇 ) 𝑦 ) = ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) )
27 25 26 eqeq12d ⊢ ( 𝑦 = 𝑒 → ( ( 𝑝 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑝 ( .r ‘ 𝑇 ) 𝑦 ) ↔ ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) = ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) ) )
28 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ 𝑥 = 𝑝 ) → 𝐵 = 𝐵 )
29 24 27 18 28 16 rspc2vd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑇 ) 𝑦 ) → ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) = ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) ) )
30 9 29 mpd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) = ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) )
31 30 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) = 𝑝 ↔ ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) = 𝑝 ) )
32 21 31 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) = 𝑝 ) ↔ ( ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) = 𝑝 ) ) )
33 6 32 raleqbidva ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐵 ( ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) = 𝑝 ) ↔ ∀ 𝑝 ∈ ( Base ‘ 𝑇 ) ( ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) = 𝑝 ) ) )
34 33 pm5.32da ⊢ ( 𝜑 → ( ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑝 ∈ 𝐵 ( ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) = 𝑝 ) ) ↔ ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑝 ∈ ( Base ‘ 𝑇 ) ( ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) = 𝑝 ) ) ) )
35 4 eleq2d ⊢ ( 𝜑 → ( 𝑒 ∈ 𝐵 ↔ 𝑒 ∈ ( Base ‘ 𝑇 ) ) )
36 35 anbi1d ⊢ ( 𝜑 → ( ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑝 ∈ ( Base ‘ 𝑇 ) ( ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) = 𝑝 ) ) ↔ ( 𝑒 ∈ ( Base ‘ 𝑇 ) ∧ ∀ 𝑝 ∈ ( Base ‘ 𝑇 ) ( ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) = 𝑝 ) ) ) )
37 34 36 bitrd ⊢ ( 𝜑 → ( ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑝 ∈ 𝐵 ( ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) = 𝑝 ) ) ↔ ( 𝑒 ∈ ( Base ‘ 𝑇 ) ∧ ∀ 𝑝 ∈ ( Base ‘ 𝑇 ) ( ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) = 𝑝 ) ) ) )
38 37 iotabidv ⊢ ( 𝜑 → ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑝 ∈ 𝐵 ( ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) = 𝑝 ) ) ) = ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑇 ) ∧ ∀ 𝑝 ∈ ( Base ‘ 𝑇 ) ( ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) = 𝑝 ) ) ) )
39 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
40 39 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
41 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
42 39 41 mgpplusg ⊢ ( .r ‘ 𝑆 ) = ( +g ‘ ( mulGrp ‘ 𝑆 ) )
43 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑆 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑆 ) )
44 40 42 43 grpidval ⊢ ( 0g ‘ ( mulGrp ‘ 𝑆 ) ) = ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑝 ∈ 𝐵 ( ( 𝑒 ( .r ‘ 𝑆 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑒 ) = 𝑝 ) ) )
45 eqid ⊢ ( mulGrp ‘ 𝑇 ) = ( mulGrp ‘ 𝑇 )
46 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
47 45 46 mgpbas ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ ( mulGrp ‘ 𝑇 ) )
48 eqid ⊢ ( .r ‘ 𝑇 ) = ( .r ‘ 𝑇 )
49 45 48 mgpplusg ⊢ ( .r ‘ 𝑇 ) = ( +g ‘ ( mulGrp ‘ 𝑇 ) )
50 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑇 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑇 ) )
51 47 49 50 grpidval ⊢ ( 0g ‘ ( mulGrp ‘ 𝑇 ) ) = ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑇 ) ∧ ∀ 𝑝 ∈ ( Base ‘ 𝑇 ) ( ( 𝑒 ( .r ‘ 𝑇 ) 𝑝 ) = 𝑝 ∧ ( 𝑝 ( .r ‘ 𝑇 ) 𝑒 ) = 𝑝 ) ) )
52 38 44 51 3eqtr4g ⊢ ( 𝜑 → ( 0g ‘ ( mulGrp ‘ 𝑆 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑇 ) ) )
53 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
54 39 53 ringidval ⊢ ( 1r ‘ 𝑆 ) = ( 0g ‘ ( mulGrp ‘ 𝑆 ) )
55 eqid ⊢ ( 1r ‘ 𝑇 ) = ( 1r ‘ 𝑇 )
56 45 55 ringidval ⊢ ( 1r ‘ 𝑇 ) = ( 0g ‘ ( mulGrp ‘ 𝑇 ) )
57 52 54 56 3eqtr4g ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑇 ) )