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

Metamath Proof Explorer

Theorem fidomndrnglem

Description: Lemma for fidomndrng . (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses fidomndrng.b 
|- B = ( Base ` R )
fidomndrng.z 
|- .0. = ( 0g ` R )
fidomndrng.o 
|- .1. = ( 1r ` R )
fidomndrng.d 
|- .|| = ( ||r ` R )
fidomndrng.t 
|- .x. = ( .r ` R )
fidomndrng.r 
|- ( ph -> R e. Domn )
fidomndrng.x 
|- ( ph -> B e. Fin )
fidomndrng.a 
|- ( ph -> A e. ( B \ { .0. } ) )
fidomndrng.f 
|- F = ( x e. B |-> ( x .x. A ) )
Assertion fidomndrnglem 
|- ( ph -> A .|| .1. )

Proof

Step Hyp Ref Expression
1 fidomndrng.b 
 |-  B = ( Base ` R )
2 fidomndrng.z 
 |-  .0. = ( 0g ` R )
3 fidomndrng.o 
 |-  .1. = ( 1r ` R )
4 fidomndrng.d 
 |-  .|| = ( ||r ` R )
5 fidomndrng.t 
 |-  .x. = ( .r ` R )
6 fidomndrng.r 
 |-  ( ph -> R e. Domn )
7 fidomndrng.x 
 |-  ( ph -> B e. Fin )
8 fidomndrng.a 
 |-  ( ph -> A e. ( B \ { .0. } ) )
9 fidomndrng.f 
 |-  F = ( x e. B |-> ( x .x. A ) )
10 8 eldifad 
 |-  ( ph -> A e. B )
11 eldifsni 
 |-  ( A e. ( B \ { .0. } ) -> A =/= .0. )
12 8 11 syl 
 |-  ( ph -> A =/= .0. )
13 12 ad2antrr 
 |-  ( ( ( ph /\ y e. B ) /\ ( F ` y ) = .0. ) -> A =/= .0. )
14 oveq1 
 |-  ( x = y -> ( x .x. A ) = ( y .x. A ) )
15 ovex 
 |-  ( y .x. A ) e. _V
16 14 9 15 fvmpt 
 |-  ( y e. B -> ( F ` y ) = ( y .x. A ) )
17 16 adantl 
 |-  ( ( ph /\ y e. B ) -> ( F ` y ) = ( y .x. A ) )
18 17 eqeq1d 
 |-  ( ( ph /\ y e. B ) -> ( ( F ` y ) = .0. <-> ( y .x. A ) = .0. ) )
19 6 adantr 
 |-  ( ( ph /\ y e. B ) -> R e. Domn )
20 simpr 
 |-  ( ( ph /\ y e. B ) -> y e. B )
21 10 adantr 
 |-  ( ( ph /\ y e. B ) -> A e. B )
22 1 5 2 domneq0 
 |-  ( ( R e. Domn /\ y e. B /\ A e. B ) -> ( ( y .x. A ) = .0. <-> ( y = .0. \/ A = .0. ) ) )
23 19 20 21 22 syl3anc 
 |-  ( ( ph /\ y e. B ) -> ( ( y .x. A ) = .0. <-> ( y = .0. \/ A = .0. ) ) )
24 18 23 bitrd 
 |-  ( ( ph /\ y e. B ) -> ( ( F ` y ) = .0. <-> ( y = .0. \/ A = .0. ) ) )
25 24 biimpa 
 |-  ( ( ( ph /\ y e. B ) /\ ( F ` y ) = .0. ) -> ( y = .0. \/ A = .0. ) )
26 25 ord 
 |-  ( ( ( ph /\ y e. B ) /\ ( F ` y ) = .0. ) -> ( -. y = .0. -> A = .0. ) )
27 26 necon1ad 
 |-  ( ( ( ph /\ y e. B ) /\ ( F ` y ) = .0. ) -> ( A =/= .0. -> y = .0. ) )
28 13 27 mpd 
 |-  ( ( ( ph /\ y e. B ) /\ ( F ` y ) = .0. ) -> y = .0. )
29 28 ex 
 |-  ( ( ph /\ y e. B ) -> ( ( F ` y ) = .0. -> y = .0. ) )
30 29 ralrimiva 
 |-  ( ph -> A. y e. B ( ( F ` y ) = .0. -> y = .0. ) )
31 domnring 
 |-  ( R e. Domn -> R e. Ring )
32 6 31 syl 
 |-  ( ph -> R e. Ring )
33 1 5 ringrghm 
 |-  ( ( R e. Ring /\ A e. B ) -> ( x e. B |-> ( x .x. A ) ) e. ( R GrpHom R ) )
34 32 10 33 syl2anc 
 |-  ( ph -> ( x e. B |-> ( x .x. A ) ) e. ( R GrpHom R ) )
35 9 34 eqeltrid 
 |-  ( ph -> F e. ( R GrpHom R ) )
36 1 1 2 2 ghmf1 
 |-  ( F e. ( R GrpHom R ) -> ( F : B -1-1-> B <-> A. y e. B ( ( F ` y ) = .0. -> y = .0. ) ) )
37 35 36 syl 
 |-  ( ph -> ( F : B -1-1-> B <-> A. y e. B ( ( F ` y ) = .0. -> y = .0. ) ) )
38 30 37 mpbird 
 |-  ( ph -> F : B -1-1-> B )
39 enreffi 
 |-  ( B e. Fin -> B ~~ B )
40 7 39 syl 
 |-  ( ph -> B ~~ B )
41 f1finf1o 
 |-  ( ( B ~~ B /\ B e. Fin ) -> ( F : B -1-1-> B <-> F : B -1-1-onto-> B ) )
42 40 7 41 syl2anc 
 |-  ( ph -> ( F : B -1-1-> B <-> F : B -1-1-onto-> B ) )
43 38 42 mpbid 
 |-  ( ph -> F : B -1-1-onto-> B )
44 f1ocnv 
 |-  ( F : B -1-1-onto-> B -> `' F : B -1-1-onto-> B )
45 f1of 
 |-  ( `' F : B -1-1-onto-> B -> `' F : B --> B )
46 43 44 45 3syl 
 |-  ( ph -> `' F : B --> B )
47 1 3 ringidcl 
 |-  ( R e. Ring -> .1. e. B )
48 32 47 syl 
 |-  ( ph -> .1. e. B )
49 46 48 ffvelcdmd 
 |-  ( ph -> ( `' F ` .1. ) e. B )
50 1 4 5 dvdsrmul 
 |-  ( ( A e. B /\ ( `' F ` .1. ) e. B ) -> A .|| ( ( `' F ` .1. ) .x. A ) )
51 10 49 50 syl2anc 
 |-  ( ph -> A .|| ( ( `' F ` .1. ) .x. A ) )
52 oveq1 
 |-  ( y = ( `' F ` .1. ) -> ( y .x. A ) = ( ( `' F ` .1. ) .x. A ) )
53 14 cbvmptv 
 |-  ( x e. B |-> ( x .x. A ) ) = ( y e. B |-> ( y .x. A ) )
54 9 53 eqtri 
 |-  F = ( y e. B |-> ( y .x. A ) )
55 ovex 
 |-  ( ( `' F ` .1. ) .x. A ) e. _V
56 52 54 55 fvmpt 
 |-  ( ( `' F ` .1. ) e. B -> ( F ` ( `' F ` .1. ) ) = ( ( `' F ` .1. ) .x. A ) )
57 49 56 syl 
 |-  ( ph -> ( F ` ( `' F ` .1. ) ) = ( ( `' F ` .1. ) .x. A ) )
58 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> B /\ .1. e. B ) -> ( F ` ( `' F ` .1. ) ) = .1. )
59 43 48 58 syl2anc 
 |-  ( ph -> ( F ` ( `' F ` .1. ) ) = .1. )
60 57 59 eqtr3d 
 |-  ( ph -> ( ( `' F ` .1. ) .x. A ) = .1. )
61 51 60 breqtrd 
 |-  ( ph -> A .|| .1. )