Metamath Proof Explorer

Theorem fracerl

Description: Rewrite the ring localization equivalence relation in the case of a field of fractions. (Contributed by Thierry Arnoux, 5-May-2025)

Ref Expression
Hypotheses fracerl.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
fracerl.2 ⊢ · = ( .r ‘ 𝑅 )
fracerl.3 ⊢ ∼ = ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) )
fracerl.4 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
fracerl.5 ⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
fracerl.6 ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
fracerl.7 ⊢ ( 𝜑 → 𝐹 ∈ ( RLReg ‘ 𝑅 ) )
fracerl.8 ⊢ ( 𝜑 → 𝐻 ∈ ( RLReg ‘ 𝑅 ) )
Assertion fracerl ( 𝜑 → ( ⟨ 𝐸 , 𝐹 ⟩ ∼ ⟨ 𝐺 , 𝐻 ⟩ ↔ ( 𝐸 · 𝐻 ) = ( 𝐺 · 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 fracerl.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 fracerl.2 ⊢ · = ( .r ‘ 𝑅 )
3 fracerl.3 ⊢ ∼ = ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) )
4 fracerl.4 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
5 fracerl.5 ⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
6 fracerl.6 ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
7 fracerl.7 ⊢ ( 𝜑 → 𝐹 ∈ ( RLReg ‘ 𝑅 ) )
8 fracerl.8 ⊢ ( 𝜑 → 𝐻 ∈ ( RLReg ‘ 𝑅 ) )
9 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
10 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
11 eqid ⊢ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) = ( 𝐵 × ( RLReg ‘ 𝑅 ) )
12 eqid ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ) ∧ ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( ( 1st ‘ 𝑎 ) · ( 2nd ‘ 𝑏 ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ 𝑏 ) · ( 2nd ‘ 𝑎 ) ) ) ) = ( 0g ‘ 𝑅 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ) ∧ ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( ( 1st ‘ 𝑎 ) · ( 2nd ‘ 𝑏 ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ 𝑏 ) · ( 2nd ‘ 𝑎 ) ) ) ) = ( 0g ‘ 𝑅 ) ) }
13 eqid ⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
14 13 1 rrgss ⊢ ( RLReg ‘ 𝑅 ) ⊆ 𝐵
15 14 a1i ⊢ ( 𝜑 → ( RLReg ‘ 𝑅 ) ⊆ 𝐵 )
16 1 9 2 10 11 12 15 erlval ⊢ ( 𝜑 → ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ) ∧ ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( ( 1st ‘ 𝑎 ) · ( 2nd ‘ 𝑏 ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ 𝑏 ) · ( 2nd ‘ 𝑎 ) ) ) ) = ( 0g ‘ 𝑅 ) ) } )
17 3 16 eqtrid ⊢ ( 𝜑 → ∼ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ) ∧ ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( ( 1st ‘ 𝑎 ) · ( 2nd ‘ 𝑏 ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ 𝑏 ) · ( 2nd ‘ 𝑎 ) ) ) ) = ( 0g ‘ 𝑅 ) ) } )
18 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ )
19 18 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 1st ‘ 𝑎 ) = ( 1st ‘ ⟨ 𝐸 , 𝐹 ⟩ ) )
20 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → 𝐹 ∈ ( RLReg ‘ 𝑅 ) )
21 op1stg ⊢ ( ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ ( RLReg ‘ 𝑅 ) ) → ( 1st ‘ ⟨ 𝐸 , 𝐹 ⟩ ) = 𝐸 )
22 5 20 21 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 1st ‘ ⟨ 𝐸 , 𝐹 ⟩ ) = 𝐸 )
23 19 22 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 1st ‘ 𝑎 ) = 𝐸 )
24 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ )
25 24 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 2nd ‘ 𝑏 ) = ( 2nd ‘ ⟨ 𝐺 , 𝐻 ⟩ ) )
26 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → 𝐻 ∈ ( RLReg ‘ 𝑅 ) )
27 op2ndg ⊢ ( ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ ( RLReg ‘ 𝑅 ) ) → ( 2nd ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = 𝐻 )
28 6 26 27 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 2nd ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = 𝐻 )
29 25 28 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 2nd ‘ 𝑏 ) = 𝐻 )
30 23 29 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ( 1st ‘ 𝑎 ) · ( 2nd ‘ 𝑏 ) ) = ( 𝐸 · 𝐻 ) )
31 24 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 1st ‘ 𝑏 ) = ( 1st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) )
32 op1stg ⊢ ( ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ ( RLReg ‘ 𝑅 ) ) → ( 1st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = 𝐺 )
33 6 26 32 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 1st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = 𝐺 )
34 31 33 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 1st ‘ 𝑏 ) = 𝐺 )
35 18 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 2nd ‘ 𝑎 ) = ( 2nd ‘ ⟨ 𝐸 , 𝐹 ⟩ ) )
36 op2ndg ⊢ ( ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ ( RLReg ‘ 𝑅 ) ) → ( 2nd ‘ ⟨ 𝐸 , 𝐹 ⟩ ) = 𝐹 )
37 5 20 36 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 2nd ‘ ⟨ 𝐸 , 𝐹 ⟩ ) = 𝐹 )
38 35 37 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 2nd ‘ 𝑎 ) = 𝐹 )
39 34 38 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ( 1st ‘ 𝑏 ) · ( 2nd ‘ 𝑎 ) ) = ( 𝐺 · 𝐹 ) )
40 30 39 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ( ( 1st ‘ 𝑎 ) · ( 2nd ‘ 𝑏 ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ 𝑏 ) · ( 2nd ‘ 𝑎 ) ) ) = ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) )
41 40 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( 𝑡 · ( ( ( 1st ‘ 𝑎 ) · ( 2nd ‘ 𝑏 ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ 𝑏 ) · ( 2nd ‘ 𝑎 ) ) ) ) = ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) )
42 41 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ( 𝑡 · ( ( ( 1st ‘ 𝑎 ) · ( 2nd ‘ 𝑏 ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ 𝑏 ) · ( 2nd ‘ 𝑎 ) ) ) ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) )
43 42 rexbidv ⊢ ( ( 𝜑 ∧ ( 𝑎 = ⟨ 𝐸 , 𝐹 ⟩ ∧ 𝑏 = ⟨ 𝐺 , 𝐻 ⟩ ) ) → ( ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( ( 1st ‘ 𝑎 ) · ( 2nd ‘ 𝑏 ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ 𝑏 ) · ( 2nd ‘ 𝑎 ) ) ) ) = ( 0g ‘ 𝑅 ) ↔ ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) )
44 17 43 brab2d ⊢ ( 𝜑 → ( ⟨ 𝐸 , 𝐹 ⟩ ∼ ⟨ 𝐺 , 𝐻 ⟩ ↔ ( ( ⟨ 𝐸 , 𝐹 ⟩ ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ∧ ⟨ 𝐺 , 𝐻 ⟩ ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ) ∧ ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) ) )
45 5 7 opelxpd ⊢ ( 𝜑 → ⟨ 𝐸 , 𝐹 ⟩ ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) )
46 6 8 opelxpd ⊢ ( 𝜑 → ⟨ 𝐺 , 𝐻 ⟩ ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) )
47 45 46 jca ⊢ ( 𝜑 → ( ⟨ 𝐸 , 𝐹 ⟩ ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ∧ ⟨ 𝐺 , 𝐻 ⟩ ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ) )
48 47 biantrurd ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( ⟨ 𝐸 , 𝐹 ⟩ ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ∧ ⟨ 𝐺 , 𝐻 ⟩ ∈ ( 𝐵 × ( RLReg ‘ 𝑅 ) ) ) ∧ ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) ) )
49 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑡 ∈ ( RLReg ‘ 𝑅 ) )
50 4 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
51 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Grp )
52 4 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
54 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝐸 ∈ 𝐵 )
55 14 8 sselid ⊢ ( 𝜑 → 𝐻 ∈ 𝐵 )
56 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝐻 ∈ 𝐵 )
57 1 2 53 54 56 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝐸 · 𝐻 ) ∈ 𝐵 )
58 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝐺 ∈ 𝐵 )
59 14 7 sselid ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
60 59 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝐹 ∈ 𝐵 )
61 1 2 53 58 60 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝐺 · 𝐹 ) ∈ 𝐵 )
62 1 10 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐸 · 𝐻 ) ∈ 𝐵 ∧ ( 𝐺 · 𝐹 ) ∈ 𝐵 ) → ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ∈ 𝐵 )
63 51 57 61 62 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ∈ 𝐵 )
64 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) )
65 13 1 2 9 rrgeq0i ⊢ ( ( 𝑡 ∈ ( RLReg ‘ 𝑅 ) ∧ ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ∈ 𝐵 ) → ( ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) → ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ) )
66 65 imp ⊢ ( ( ( 𝑡 ∈ ( RLReg ‘ 𝑅 ) ∧ ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ∈ 𝐵 ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) )
67 49 63 64 66 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) )
68 67 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) )
69 oveq1 ⊢ ( 𝑡 = ( 1r ‘ 𝑅 ) → ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( ( 1r ‘ 𝑅 ) · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) )
70 69 eqeq1d ⊢ ( 𝑡 = ( 1r ‘ 𝑅 ) → ( ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( 1r ‘ 𝑅 ) · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ) )
71 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
72 71 13 52 1rrg ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( RLReg ‘ 𝑅 ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( RLReg ‘ 𝑅 ) )
74 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) )
75 74 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( ( 1r ‘ 𝑅 ) · ( 0g ‘ 𝑅 ) ) )
76 1 71 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
77 52 76 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
78 1 2 9 52 77 ringrzd ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
79 78 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
80 75 79 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) )
81 70 73 80 rspcedvdw ⊢ ( ( 𝜑 ∧ ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) )
82 68 81 impbida ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 · ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ) )
83 44 48 82 3bitr2d ⊢ ( 𝜑 → ( ⟨ 𝐸 , 𝐹 ⟩ ∼ ⟨ 𝐺 , 𝐻 ⟩ ↔ ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ) )
84 1 2 52 5 55 ringcld ⊢ ( 𝜑 → ( 𝐸 · 𝐻 ) ∈ 𝐵 )
85 1 2 52 6 59 ringcld ⊢ ( 𝜑 → ( 𝐺 · 𝐹 ) ∈ 𝐵 )
86 1 9 10 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐸 · 𝐻 ) ∈ 𝐵 ∧ ( 𝐺 · 𝐹 ) ∈ 𝐵 ) → ( ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ↔ ( 𝐸 · 𝐻 ) = ( 𝐺 · 𝐹 ) ) )
87 50 84 85 86 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐸 · 𝐻 ) ( -g ‘ 𝑅 ) ( 𝐺 · 𝐹 ) ) = ( 0g ‘ 𝑅 ) ↔ ( 𝐸 · 𝐻 ) = ( 𝐺 · 𝐹 ) ) )
88 83 87 bitrd ⊢ ( 𝜑 → ( ⟨ 𝐸 , 𝐹 ⟩ ∼ ⟨ 𝐺 , 𝐻 ⟩ ↔ ( 𝐸 · 𝐻 ) = ( 𝐺 · 𝐹 ) ) )