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

Metamath Proof Explorer

Theorem rlocf1

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

Ref Expression
Hypotheses rlocf1.1 
|- B = ( Base ` R )
rlocf1.2 
|- .1. = ( 1r ` R )
rlocf1.3 
|- L = ( R RLocal S )
rlocf1.4 
|- .~ = ( R ~RL S )
rlocf1.5 
|- F = ( x e. B |-> [ <. x , .1. >. ] .~ )
rlocf1.6 
|- ( ph -> R e. CRing )
rlocf1.7 
|- ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
rlocf1.8 
|- ( ph -> S C_ ( RLReg ` R ) )
Assertion rlocf1 
|- ( ph -> ( F : B -1-1-> ( ( B X. S ) /. .~ ) /\ F e. ( R RingHom L ) ) )

Proof

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