This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlocf1

Description: The embedding F of a ring R into its localization L . (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses rlocf1.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
rlocf1.2 ⊢ 1 = ( 1r ‘ 𝑅 )
rlocf1.3 ⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
rlocf1.4 ⊢ ∼ = ( 𝑅 ~RL 𝑆 )
rlocf1.5 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ ⟨ 𝑥 , 1 ⟩ ] ∼ )
rlocf1.6 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
rlocf1.7 ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
rlocf1.8 ⊢ ( 𝜑 → 𝑆 ⊆ ( RLReg ‘ 𝑅 ) )
Assertion rlocf1 ( 𝜑 → ( 𝐹 : 𝐵 –1-1→ ( ( 𝐵 × 𝑆 ) / ∼ ) ∧ 𝐹 ∈ ( 𝑅 RingHom 𝐿 ) ) )

Proof

Step Hyp Ref Expression
1 rlocf1.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rlocf1.2 ⊢ 1 = ( 1r ‘ 𝑅 )
3 rlocf1.3 ⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
4 rlocf1.4 ⊢ ∼ = ( 𝑅 ~RL 𝑆 )
5 rlocf1.5 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ ⟨ 𝑥 , 1 ⟩ ] ∼ )
6 rlocf1.6 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
7 rlocf1.7 ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
8 rlocf1.8 ⊢ ( 𝜑 → 𝑆 ⊆ ( RLReg ‘ 𝑅 ) )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
10 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
11 10 2 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
12 11 subm0cl ⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 1 ∈ 𝑆 )
13 7 12 syl ⊢ ( 𝜑 → 1 ∈ 𝑆 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 1 ∈ 𝑆 )
15 9 14 opelxpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ⟨ 𝑥 , 1 ⟩ ∈ ( 𝐵 × 𝑆 ) )
16 4 ovexi ⊢ ∼ ∈ V
17 16 ecelqsi ⊢ ( ⟨ 𝑥 , 1 ⟩ ∈ ( 𝐵 × 𝑆 ) → [ ⟨ 𝑥 , 1 ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
18 15 17 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ ⟨ 𝑥 , 1 ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
19 18 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 [ ⟨ 𝑥 , 1 ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
20 6 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
21 20 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Grp )
22 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑥 ∈ 𝐵 )
23 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑦 ∈ 𝐵 )
24 vex ⊢ 𝑥 ∈ V
25 2 fvexi ⊢ 1 ∈ V
26 24 25 op1st ⊢ ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) = 𝑥
27 26 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) = 𝑥 )
28 vex ⊢ 𝑦 ∈ V
29 28 25 op2nd ⊢ ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) = 1
30 29 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) = 1 )
31 27 30 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) = ( 𝑥 ( .r ‘ 𝑅 ) 1 ) )
32 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
33 6 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
34 33 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
35 1 32 2 34 22 ringridmd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 1 ) = 𝑥 )
36 31 35 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) = 𝑥 )
37 28 25 op1st ⊢ ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) = 𝑦
38 37 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) = 𝑦 )
39 24 25 op2nd ⊢ ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) = 1
40 39 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) = 1 )
41 38 40 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) = ( 𝑦 ( .r ‘ 𝑅 ) 1 ) )
42 1 32 2 34 23 ringridmd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 1 ) = 𝑦 )
43 41 42 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) = 𝑦 )
44 36 43 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) = ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) )
45 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑆 ⊆ ( RLReg ‘ 𝑅 ) )
46 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑡 ∈ 𝑆 )
47 45 46 sseldd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑡 ∈ ( RLReg ‘ 𝑅 ) )
48 27 22 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ∈ 𝐵 )
49 10 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
50 49 submss ⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 𝑆 ⊆ 𝐵 )
51 7 50 syl ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
52 51 13 sseldd ⊢ ( 𝜑 → 1 ∈ 𝐵 )
53 52 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 1 ∈ 𝐵 )
54 30 53 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ∈ 𝐵 )
55 1 32 34 48 54 ringcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ∈ 𝐵 )
56 38 23 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ∈ 𝐵 )
57 40 53 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ∈ 𝐵 )
58 1 32 34 56 57 ringcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ∈ 𝐵 )
59 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
60 1 59 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ∈ 𝐵 ∧ ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ∈ 𝐵 ) → ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ∈ 𝐵 )
61 21 55 58 60 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ∈ 𝐵 )
62 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) )
63 eqid ⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
64 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
65 63 1 32 64 rrgeq0i ⊢ ( ( 𝑡 ∈ ( RLReg ‘ 𝑅 ) ∧ ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ∈ 𝐵 ) → ( ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) → ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) = ( 0g ‘ 𝑅 ) ) )
66 65 imp ⊢ ( ( ( 𝑡 ∈ ( RLReg ‘ 𝑅 ) ∧ ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ∈ 𝐵 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) = ( 0g ‘ 𝑅 ) )
67 47 61 62 66 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) = ( 0g ‘ 𝑅 ) )
68 44 67 eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) )
69 1 64 59 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) ↔ 𝑥 = 𝑦 ) )
70 69 biimpa ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) ) → 𝑥 = 𝑦 )
71 21 22 23 68 70 syl31anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) ∧ 𝑡 ∈ 𝑆 ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑥 = 𝑦 )
72 51 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) → 𝑆 ⊆ 𝐵 )
73 eqid ⊢ ( 𝐵 × 𝑆 ) = ( 𝐵 × 𝑆 )
74 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑅 ∈ CRing )
75 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
76 1 64 2 32 59 73 4 74 75 erler ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ∼ Er ( 𝐵 × 𝑆 ) )
77 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 1 ⟩ ∈ ( 𝐵 × 𝑆 ) )
78 76 77 erth ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ⟨ 𝑥 , 1 ⟩ ∼ ⟨ 𝑦 , 1 ⟩ ↔ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) )
79 78 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) → ⟨ 𝑥 , 1 ⟩ ∼ ⟨ 𝑦 , 1 ⟩ )
80 1 4 72 64 32 59 79 erldi ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) → ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ 𝑥 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑦 , 1 ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ 𝑦 , 1 ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ 𝑥 , 1 ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) )
81 71 80 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ ) → 𝑥 = 𝑦 )
82 81 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ → 𝑥 = 𝑦 ) )
83 82 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ → 𝑥 = 𝑦 ) )
84 83 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ → 𝑥 = 𝑦 ) )
85 opeq1 ⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 1 ⟩ = ⟨ 𝑦 , 1 ⟩ )
86 85 eceq1d ⊢ ( 𝑥 = 𝑦 → [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ )
87 5 86 f1mpt ⊢ ( 𝐹 : 𝐵 –1-1→ ( ( 𝐵 × 𝑆 ) / ∼ ) ↔ ( ∀ 𝑥 ∈ 𝐵 [ ⟨ 𝑥 , 1 ⟩ ] ∼ ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑦 , 1 ⟩ ] ∼ → 𝑥 = 𝑦 ) ) )
88 19 84 87 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ ( ( 𝐵 × 𝑆 ) / ∼ ) )
89 eqid ⊢ ( 1r ‘ 𝐿 ) = ( 1r ‘ 𝐿 )
90 eqid ⊢ ( .r ‘ 𝐿 ) = ( .r ‘ 𝐿 )
91 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
92 1 32 91 3 4 6 7 rloccring ⊢ ( 𝜑 → 𝐿 ∈ CRing )
93 92 crngringd ⊢ ( 𝜑 → 𝐿 ∈ Ring )
94 opeq1 ⊢ ( 𝑥 = 1 → ⟨ 𝑥 , 1 ⟩ = ⟨ 1 , 1 ⟩ )
95 94 eceq1d ⊢ ( 𝑥 = 1 → [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 1 , 1 ⟩ ] ∼ )
96 eqid ⊢ [ ⟨ 1 , 1 ⟩ ] ∼ = [ ⟨ 1 , 1 ⟩ ] ∼
97 64 2 3 4 6 7 96 rloc1r ⊢ ( 𝜑 → [ ⟨ 1 , 1 ⟩ ] ∼ = ( 1r ‘ 𝐿 ) )
98 95 97 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → [ ⟨ 𝑥 , 1 ⟩ ] ∼ = ( 1r ‘ 𝐿 ) )
99 fvexd ⊢ ( 𝜑 → ( 1r ‘ 𝐿 ) ∈ V )
100 5 98 52 99 fvmptd2 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 1r ‘ 𝐿 ) )
101 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑅 ∈ Ring )
102 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → 1 ∈ 𝐵 )
103 1 32 2 101 102 ringlidmd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) 1 ) = 1 )
104 103 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → 1 = ( 1 ( .r ‘ 𝑅 ) 1 ) )
105 104 opeq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , 1 ⟩ = ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , ( 1 ( .r ‘ 𝑅 ) 1 ) ⟩ )
106 105 eceq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → [ ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ = [ ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , ( 1 ( .r ‘ 𝑅 ) 1 ) ⟩ ] ∼ )
107 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑅 ∈ CRing )
108 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
109 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
110 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
111 108 12 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → 1 ∈ 𝑆 )
112 1 32 91 3 4 107 108 109 110 111 111 90 rlocmulval ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( [ ⟨ 𝑎 , 1 ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑏 , 1 ⟩ ] ∼ ) = [ ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , ( 1 ( .r ‘ 𝑅 ) 1 ) ⟩ ] ∼ )
113 106 112 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → [ ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ = ( [ ⟨ 𝑎 , 1 ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑏 , 1 ⟩ ] ∼ ) )
114 opeq1 ⊢ ( 𝑥 = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) → ⟨ 𝑥 , 1 ⟩ = ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , 1 ⟩ )
115 114 eceq1d ⊢ ( 𝑥 = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) → [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ )
116 1 32 101 109 110 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
117 ecexg ⊢ ( ∼ ∈ V → [ ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ ∈ V )
118 16 117 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → [ ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ ∈ V )
119 5 115 116 118 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = [ ⟨ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ )
120 opeq1 ⊢ ( 𝑥 = 𝑎 → ⟨ 𝑥 , 1 ⟩ = ⟨ 𝑎 , 1 ⟩ )
121 120 eceq1d ⊢ ( 𝑥 = 𝑎 → [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑎 , 1 ⟩ ] ∼ )
122 ecexg ⊢ ( ∼ ∈ V → [ ⟨ 𝑎 , 1 ⟩ ] ∼ ∈ V )
123 16 122 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → [ ⟨ 𝑎 , 1 ⟩ ] ∼ ∈ V )
124 5 121 109 123 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) = [ ⟨ 𝑎 , 1 ⟩ ] ∼ )
125 opeq1 ⊢ ( 𝑥 = 𝑏 → ⟨ 𝑥 , 1 ⟩ = ⟨ 𝑏 , 1 ⟩ )
126 125 eceq1d ⊢ ( 𝑥 = 𝑏 → [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ 𝑏 , 1 ⟩ ] ∼ )
127 ecexg ⊢ ( ∼ ∈ V → [ ⟨ 𝑏 , 1 ⟩ ] ∼ ∈ V )
128 16 127 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → [ ⟨ 𝑏 , 1 ⟩ ] ∼ ∈ V )
129 5 126 110 128 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑏 ) = [ ⟨ 𝑏 , 1 ⟩ ] ∼ )
130 124 129 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝐿 ) ( 𝐹 ‘ 𝑏 ) ) = ( [ ⟨ 𝑎 , 1 ⟩ ] ∼ ( .r ‘ 𝐿 ) [ ⟨ 𝑏 , 1 ⟩ ] ∼ ) )
131 113 119 130 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝐿 ) ( 𝐹 ‘ 𝑏 ) ) )
132 131 anasss ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( .r ‘ 𝐿 ) ( 𝐹 ‘ 𝑏 ) ) )
133 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
134 eqid ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
135 18 5 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( ( 𝐵 × 𝑆 ) / ∼ ) )
136 1 64 32 59 73 3 4 6 51 rlocbas ⊢ ( 𝜑 → ( ( 𝐵 × 𝑆 ) / ∼ ) = ( Base ‘ 𝐿 ) )
137 136 feq3d ⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ ( ( 𝐵 × 𝑆 ) / ∼ ) ↔ 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐿 ) ) )
138 135 137 mpbid ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐿 ) )
139 1 32 2 101 109 ringridmd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( .r ‘ 𝑅 ) 1 ) = 𝑎 )
140 1 32 2 101 110 ringridmd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ( .r ‘ 𝑅 ) 1 ) = 𝑏 )
141 139 140 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 1 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 1 ) ) = ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) )
142 141 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 1 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 1 ) ) )
143 142 104 opeq12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ⟨ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) , 1 ⟩ = ⟨ ( ( 𝑎 ( .r ‘ 𝑅 ) 1 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 1 ) ) , ( 1 ( .r ‘ 𝑅 ) 1 ) ⟩ )
144 143 eceq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → [ ⟨ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ = [ ⟨ ( ( 𝑎 ( .r ‘ 𝑅 ) 1 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 1 ) ) , ( 1 ( .r ‘ 𝑅 ) 1 ) ⟩ ] ∼ )
145 1 32 91 3 4 107 108 109 110 111 111 134 rlocaddval ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( [ ⟨ 𝑎 , 1 ⟩ ] ∼ ( +g ‘ 𝐿 ) [ ⟨ 𝑏 , 1 ⟩ ] ∼ ) = [ ⟨ ( ( 𝑎 ( .r ‘ 𝑅 ) 1 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 1 ) ) , ( 1 ( .r ‘ 𝑅 ) 1 ) ⟩ ] ∼ )
146 144 145 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → [ ⟨ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ = ( [ ⟨ 𝑎 , 1 ⟩ ] ∼ ( +g ‘ 𝐿 ) [ ⟨ 𝑏 , 1 ⟩ ] ∼ ) )
147 opeq1 ⊢ ( 𝑥 = ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) → ⟨ 𝑥 , 1 ⟩ = ⟨ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) , 1 ⟩ )
148 147 eceq1d ⊢ ( 𝑥 = ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) → [ ⟨ 𝑥 , 1 ⟩ ] ∼ = [ ⟨ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ )
149 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → 𝑅 ∈ Grp )
150 1 91 149 109 110 grpcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
151 ecexg ⊢ ( ∼ ∈ V → [ ⟨ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ ∈ V )
152 16 151 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → [ ⟨ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ ∈ V )
153 5 148 150 152 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = [ ⟨ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) , 1 ⟩ ] ∼ )
154 124 129 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐿 ) ( 𝐹 ‘ 𝑏 ) ) = ( [ ⟨ 𝑎 , 1 ⟩ ] ∼ ( +g ‘ 𝐿 ) [ ⟨ 𝑏 , 1 ⟩ ] ∼ ) )
155 146 153 154 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐿 ) ( 𝐹 ‘ 𝑏 ) ) )
156 155 anasss ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝐿 ) ( 𝐹 ‘ 𝑏 ) ) )
157 1 2 89 32 90 33 93 100 132 133 91 134 138 156 isrhmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝐿 ) )
158 88 157 jca ⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1→ ( ( 𝐵 × 𝑆 ) / ∼ ) ∧ 𝐹 ∈ ( 𝑅 RingHom 𝐿 ) ) )