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 
|- ( ph -> R e. IDomn )
Assertion fracfld 
|- ( ph -> ( Frac ` R ) e. Field )

Proof

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