Metamath Proof Explorer

Theorem fracfld

Description: The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypothesis fracfld.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
Assertion fracfld ( 𝜑 → ( Frac ‘ 𝑅 ) ∈ Field )

Proof

Step Hyp Ref Expression
1 fracfld.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
2 fracval ⊢ ( Frac ‘ 𝑅 ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) )
3 1 idomdomd ⊢ ( 𝜑 → 𝑅 ∈ Domn )
4 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
5 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7 5 6 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
8 3 4 7 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
9 fvex ⊢ ( 1r ‘ 𝑅 ) ∈ V
10 9 9 op1st ⊢ ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ( 1r ‘ 𝑅 )
11 10 a1i ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ( 1r ‘ 𝑅 ) )
12 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
13 12 9 op2nd ⊢ ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ( 1r ‘ 𝑅 )
14 13 a1i ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ( 1r ‘ 𝑅 ) )
15 11 14 oveq12d ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
16 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
18 1 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
20 16 5 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
21 19 20 syl ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
22 16 17 5 19 21 ringlidmd ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
23 15 22 eqtrd ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) = ( 1r ‘ 𝑅 ) )
24 12 9 op1st ⊢ ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ( 0g ‘ 𝑅 )
25 24 a1i ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ( 0g ‘ 𝑅 ) )
26 9 9 op2nd ⊢ ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ( 1r ‘ 𝑅 )
27 26 a1i ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) = ( 1r ‘ 𝑅 ) )
28 25 27 oveq12d ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
29 18 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
30 16 6 grpidcl ⊢ ( 𝑅 ∈ Grp → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
31 29 30 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
32 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
33 16 17 5 19 32 ringridmd ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
34 28 33 eqtrd ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) = ( 0g ‘ 𝑅 ) )
35 23 34 oveq12d ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( ( ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ) = ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
36 35 oveq2d ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ) ) = ( 𝑡 ( .r ‘ 𝑅 ) ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) ) )
37 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
38 eqid ⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
39 38 16 rrgss ⊢ ( RLReg ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 )
40 39 a1i ⊢ ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( RLReg ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
41 40 sselda ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → 𝑡 ∈ ( Base ‘ 𝑅 ) )
42 16 17 37 19 41 21 32 ringsubdi ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) ) = ( ( 𝑡 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ( -g ‘ 𝑅 ) ( 𝑡 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) ) )
43 16 17 5 19 41 ringridmd ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑡 )
44 16 17 6 19 41 ringrzd ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
45 43 44 oveq12d ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( ( 𝑡 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ( -g ‘ 𝑅 ) ( 𝑡 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) ) = ( 𝑡 ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
46 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → 𝑅 ∈ Grp )
47 16 6 37 grpsubid1 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑡 ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = 𝑡 )
48 46 41 47 syl2anc ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 𝑡 ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = 𝑡 )
49 45 48 eqtrd ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( ( 𝑡 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ( -g ‘ 𝑅 ) ( 𝑡 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) ) = 𝑡 )
50 36 42 49 3eqtrd ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ) ) = 𝑡 )
51 50 eqeq1d ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ( ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ↔ 𝑡 = ( 0g ‘ 𝑅 ) ) )
52 51 biimpa ⊢ ( ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑡 = ( 0g ‘ 𝑅 ) )
53 simpr ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → 𝑡 ∈ ( RLReg ‘ 𝑅 ) )
54 38 6 rrgnz ⊢ ( 𝑅 ∈ NzRing → ¬ ( 0g ‘ 𝑅 ) ∈ ( RLReg ‘ 𝑅 ) )
55 3 4 54 3syl ⊢ ( 𝜑 → ¬ ( 0g ‘ 𝑅 ) ∈ ( RLReg ‘ 𝑅 ) )
56 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → ¬ ( 0g ‘ 𝑅 ) ∈ ( RLReg ‘ 𝑅 ) )
57 nelne2 ⊢ ( ( 𝑡 ∈ ( RLReg ‘ 𝑅 ) ∧ ¬ ( 0g ‘ 𝑅 ) ∈ ( RLReg ‘ 𝑅 ) ) → 𝑡 ≠ ( 0g ‘ 𝑅 ) )
58 53 56 57 syl2anc ⊢ ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) → 𝑡 ≠ ( 0g ‘ 𝑅 ) )
59 58 adantr ⊢ ( ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → 𝑡 ≠ ( 0g ‘ 𝑅 ) )
60 52 59 pm2.21ddne ⊢ ( ( ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ) ∧ ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
61 eqid ⊢ ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) )
62 eqid ⊢ ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) = ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) )
63 1 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
64 16 38 6 isdomn6 ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) = ( RLReg ‘ 𝑅 ) ) )
65 3 64 sylib ⊢ ( 𝜑 → ( 𝑅 ∈ NzRing ∧ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) = ( RLReg ‘ 𝑅 ) ) )
66 65 simprd ⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) = ( RLReg ‘ 𝑅 ) )
67 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
68 16 6 67 isdomn3 ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ Ring ∧ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ) )
69 3 68 sylib ⊢ ( 𝜑 → ( 𝑅 ∈ Ring ∧ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ) )
70 69 simprd ⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
71 66 70 eqeltrrd ⊢ ( 𝜑 → ( RLReg ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
72 16 6 5 17 37 62 61 63 71 erler ⊢ ( 𝜑 → ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) Er ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) )
73 18 20 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
74 5 38 18 1rrg ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( RLReg ‘ 𝑅 ) )
75 73 74 opelxpd ⊢ ( 𝜑 → ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ∈ ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) )
76 72 75 erth ⊢ ( 𝜑 → ( ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ↔ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
77 76 biimpar ⊢ ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ )
78 16 61 40 6 17 37 77 erldi ⊢ ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ∃ 𝑡 ∈ ( RLReg ‘ 𝑅 ) ( 𝑡 ( .r ‘ 𝑅 ) ( ( ( 1st ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ( -g ‘ 𝑅 ) ( ( 1st ‘ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ( .r ‘ 𝑅 ) ( 2nd ‘ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ) ) ) ) = ( 0g ‘ 𝑅 ) )
79 60 78 r19.29a ⊢ ( ( 𝜑 ∧ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
80 8 79 mteqand ⊢ ( 𝜑 → [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ≠ [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) )
81 eqid ⊢ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) )
82 eqid ⊢ [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) )
83 6 5 81 61 63 71 82 rloc1r ⊢ ( 𝜑 → [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
84 eqid ⊢ [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) )
85 6 5 81 61 63 71 84 rloc0g ⊢ ( 𝜑 → [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
86 80 83 85 3netr3d ⊢ ( 𝜑 → ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ≠ ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
87 oveq2 ⊢ ( 𝑦 = [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
88 87 eqeq1d ⊢ ( 𝑦 = [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ↔ ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ) )
89 oveq1 ⊢ ( 𝑦 = [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) )
90 89 eqeq1d ⊢ ( 𝑦 = [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) → ( ( 𝑦 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ↔ ( [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ) )
91 88 90 anbi12d ⊢ ( 𝑦 = [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) → ( ( ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑦 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ) ↔ ( ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∧ ( [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ) ) )
92 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑏 ∈ ( RLReg ‘ 𝑅 ) )
93 39 92 sselid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
94 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
95 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) )
96 72 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) Er ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) )
97 18 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
98 97 20 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
99 16 17 6 97 98 ringlzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
100 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → 𝑎 = ( 0g ‘ 𝑅 ) )
101 100 oveq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
102 93 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
103 16 17 6 97 102 ringlzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) )
104 99 101 103 3eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑏 ) )
105 63 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ CRing )
106 94 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
107 31 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
108 92 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → 𝑏 ∈ ( RLReg ‘ 𝑅 ) )
109 74 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( RLReg ‘ 𝑅 ) )
110 16 17 61 105 106 107 108 109 fracerl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ↔ ( 𝑎 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑏 ) ) )
111 104 110 mpbird ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ⟨ 𝑎 , 𝑏 ⟩ ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ )
112 96 111 erthi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) )
113 85 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → [ ⟨ ( 0g ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
114 95 112 113 3eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → 𝑥 = ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
115 eldifsni ⊢ ( 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) → 𝑥 ≠ ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
116 115 ad5antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → 𝑥 ≠ ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
117 116 neneqd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ 𝑎 = ( 0g ‘ 𝑅 ) ) → ¬ 𝑥 = ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
118 114 117 pm2.65da ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ¬ 𝑎 = ( 0g ‘ 𝑅 ) )
119 118 neqned ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑎 ≠ ( 0g ‘ 𝑅 ) )
120 94 119 eldifsnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑎 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
121 66 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) = ( RLReg ‘ 𝑅 ) )
122 120 121 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑎 ∈ ( RLReg ‘ 𝑅 ) )
123 93 122 opelxpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ⟨ 𝑏 , 𝑎 ⟩ ∈ ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) )
124 ovex ⊢ ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ∈ V
125 124 ecelqsi ⊢ ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) → [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ∈ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
126 123 125 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ∈ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
127 39 a1i ⊢ ( 𝜑 → ( RLReg ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
128 16 6 17 37 62 81 61 1 127 rlocbas ⊢ ( 𝜑 → ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
129 128 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
130 126 129 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ∈ ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
131 eqid ⊢ ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) )
132 eqid ⊢ ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) = ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) )
133 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
134 16 17 133 81 61 63 71 rloccring ⊢ ( 𝜑 → ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ∈ CRing )
135 134 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ∈ CRing )
136 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) )
137 136 eldifad ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑥 ∈ ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
138 131 132 135 137 130 crngcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) )
139 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) )
140 139 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
141 63 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑅 ∈ CRing )
142 71 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( RLReg ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
143 16 17 133 81 61 141 142 93 94 122 92 132 rlocmulval ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = [ ⟨ ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) )
144 72 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) Er ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) )
145 16 17 141 93 94 crngcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) )
146 18 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
147 16 17 146 93 94 ringcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
148 16 17 5 146 147 ringridmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) )
149 16 17 146 94 93 ringcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
150 16 17 5 146 149 ringlidmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) )
151 145 148 150 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) )
152 73 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
153 94 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
154 31 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
155 92 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → 𝑏 ∈ ( RLReg ‘ 𝑅 ) )
156 66 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) = ( RLReg ‘ 𝑅 ) )
157 155 156 eleqtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → 𝑏 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
158 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) → 𝑅 ∈ IDomn )
159 158 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ IDomn )
160 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) )
161 146 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
162 93 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
163 16 17 6 161 162 ringlzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) )
164 160 163 eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑏 ) )
165 16 6 17 153 154 157 159 164 idomrcan ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → 𝑎 = ( 0g ‘ 𝑅 ) )
166 118 165 mtand ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ¬ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) )
167 166 neqned ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ≠ ( 0g ‘ 𝑅 ) )
168 149 167 eldifsnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
169 168 121 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ ( RLReg ‘ 𝑅 ) )
170 74 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 1r ‘ 𝑅 ) ∈ ( RLReg ‘ 𝑅 ) )
171 16 17 61 141 147 152 169 170 fracerl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( ⟨ ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ⟩ ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ↔ ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) ) )
172 151 171 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ⟨ ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ⟩ ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ )
173 144 172 erthi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → [ ⟨ ( 𝑏 ( .r ‘ 𝑅 ) 𝑎 ) , ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) )
174 143 173 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) )
175 83 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → [ ⟨ ( 1r ‘ 𝑅 ) , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
176 140 174 175 3eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
177 138 176 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) )
178 177 176 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∧ ( [ ⟨ 𝑏 , 𝑎 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ) )
179 91 130 178 rspcedvdw ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 ∈ ( RLReg ‘ 𝑅 ) ) ∧ 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ∃ 𝑦 ∈ ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ( ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑦 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ) )
180 128 difeq1d ⊢ ( 𝜑 → ( ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) = ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) )
181 180 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ↔ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) )
182 181 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) → 𝑥 ∈ ( ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) )
183 182 eldifad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) → 𝑥 ∈ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
184 183 elrlocbasi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) → ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) ∃ 𝑏 ∈ ( RLReg ‘ 𝑅 ) 𝑥 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) )
185 179 184 r19.29vva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ) → ∃ 𝑦 ∈ ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ( ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑦 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ) )
186 185 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ∃ 𝑦 ∈ ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ( ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑦 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ) )
187 eqid ⊢ ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) = ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) )
188 eqid ⊢ ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) )
189 eqid ⊢ ( Unit ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) = ( Unit ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) )
190 134 crngringd ⊢ ( 𝜑 → ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ∈ Ring )
191 131 187 188 132 189 190 isdrng4 ⊢ ( 𝜑 → ( ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ∈ DivRing ↔ ( ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ≠ ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∧ ∀ 𝑥 ∈ ( ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∖ { ( 0g ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) } ) ∃ 𝑦 ∈ ( Base ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ( ( 𝑥 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑦 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑦 ( .r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) 𝑥 ) = ( 1r ‘ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ) ) ) ) )
192 86 186 191 mpbir2and ⊢ ( 𝜑 → ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ∈ DivRing )
193 isfld ⊢ ( ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ∈ Field ↔ ( ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ∈ DivRing ∧ ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ∈ CRing ) )
194 192 134 193 sylanbrc ⊢ ( 𝜑 → ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ∈ Field )
195 2 194 eqeltrid ⊢ ( 𝜑 → ( Frac ‘ 𝑅 ) ∈ Field )