Metamath Proof Explorer

Theorem ostthlem2

Description: Lemma for ostth . Refine ostthlem1 so that it is sufficient to only show equality on the primes. (Contributed by Mario Carneiro, 9-Sep-2014) (Revised by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses qrng.q 
|- Q = ( CCfld |`s QQ )
qabsabv.a 
|- A = ( AbsVal ` Q )
ostthlem1.1 
|- ( ph -> F e. A )
ostthlem1.2 
|- ( ph -> G e. A )
ostthlem2.3 
|- ( ( ph /\ p e. Prime ) -> ( F ` p ) = ( G ` p ) )
Assertion ostthlem2 
|- ( ph -> F = G )

Proof

Step Hyp Ref Expression
1 qrng.q 
 |-  Q = ( CCfld |`s QQ )
2 qabsabv.a 
 |-  A = ( AbsVal ` Q )
3 ostthlem1.1 
 |-  ( ph -> F e. A )
4 ostthlem1.2 
 |-  ( ph -> G e. A )
5 ostthlem2.3 
 |-  ( ( ph /\ p e. Prime ) -> ( F ` p ) = ( G ` p ) )
6 eluz2nn 
 |-  ( n e. ( ZZ>= ` 2 ) -> n e. NN )
7 fveq2 
 |-  ( p = 1 -> ( F ` p ) = ( F ` 1 ) )
8 fveq2 
 |-  ( p = 1 -> ( G ` p ) = ( G ` 1 ) )
9 7 8 eqeq12d 
 |-  ( p = 1 -> ( ( F ` p ) = ( G ` p ) <-> ( F ` 1 ) = ( G ` 1 ) ) )
10 9 imbi2d 
 |-  ( p = 1 -> ( ( ph -> ( F ` p ) = ( G ` p ) ) <-> ( ph -> ( F ` 1 ) = ( G ` 1 ) ) ) )
11 fveq2 
 |-  ( p = y -> ( F ` p ) = ( F ` y ) )
12 fveq2 
 |-  ( p = y -> ( G ` p ) = ( G ` y ) )
13 11 12 eqeq12d 
 |-  ( p = y -> ( ( F ` p ) = ( G ` p ) <-> ( F ` y ) = ( G ` y ) ) )
14 13 imbi2d 
 |-  ( p = y -> ( ( ph -> ( F ` p ) = ( G ` p ) ) <-> ( ph -> ( F ` y ) = ( G ` y ) ) ) )
15 fveq2 
 |-  ( p = z -> ( F ` p ) = ( F ` z ) )
16 fveq2 
 |-  ( p = z -> ( G ` p ) = ( G ` z ) )
17 15 16 eqeq12d 
 |-  ( p = z -> ( ( F ` p ) = ( G ` p ) <-> ( F ` z ) = ( G ` z ) ) )
18 17 imbi2d 
 |-  ( p = z -> ( ( ph -> ( F ` p ) = ( G ` p ) ) <-> ( ph -> ( F ` z ) = ( G ` z ) ) ) )
19 fveq2 
 |-  ( p = ( y x. z ) -> ( F ` p ) = ( F ` ( y x. z ) ) )
20 fveq2 
 |-  ( p = ( y x. z ) -> ( G ` p ) = ( G ` ( y x. z ) ) )
21 19 20 eqeq12d 
 |-  ( p = ( y x. z ) -> ( ( F ` p ) = ( G ` p ) <-> ( F ` ( y x. z ) ) = ( G ` ( y x. z ) ) ) )
22 21 imbi2d 
 |-  ( p = ( y x. z ) -> ( ( ph -> ( F ` p ) = ( G ` p ) ) <-> ( ph -> ( F ` ( y x. z ) ) = ( G ` ( y x. z ) ) ) ) )
23 fveq2 
 |-  ( p = n -> ( F ` p ) = ( F ` n ) )
24 fveq2 
 |-  ( p = n -> ( G ` p ) = ( G ` n ) )
25 23 24 eqeq12d 
 |-  ( p = n -> ( ( F ` p ) = ( G ` p ) <-> ( F ` n ) = ( G ` n ) ) )
26 25 imbi2d 
 |-  ( p = n -> ( ( ph -> ( F ` p ) = ( G ` p ) ) <-> ( ph -> ( F ` n ) = ( G ` n ) ) ) )
27 ax-1ne0 
 |-  1 =/= 0
28 1 qrng1 
 |-  1 = ( 1r ` Q )
29 1 qrng0 
 |-  0 = ( 0g ` Q )
30 2 28 29 abv1z 
 |-  ( ( F e. A /\ 1 =/= 0 ) -> ( F ` 1 ) = 1 )
31 3 27 30 sylancl 
 |-  ( ph -> ( F ` 1 ) = 1 )
32 2 28 29 abv1z 
 |-  ( ( G e. A /\ 1 =/= 0 ) -> ( G ` 1 ) = 1 )
33 4 27 32 sylancl 
 |-  ( ph -> ( G ` 1 ) = 1 )
34 31 33 eqtr4d 
 |-  ( ph -> ( F ` 1 ) = ( G ` 1 ) )
35 5 expcom 
 |-  ( p e. Prime -> ( ph -> ( F ` p ) = ( G ` p ) ) )
36 jcab 
 |-  ( ( ph -> ( ( F ` y ) = ( G ` y ) /\ ( F ` z ) = ( G ` z ) ) ) <-> ( ( ph -> ( F ` y ) = ( G ` y ) ) /\ ( ph -> ( F ` z ) = ( G ` z ) ) ) )
37 oveq12 
 |-  ( ( ( F ` y ) = ( G ` y ) /\ ( F ` z ) = ( G ` z ) ) -> ( ( F ` y ) x. ( F ` z ) ) = ( ( G ` y ) x. ( G ` z ) ) )
38 3 adantr 
 |-  ( ( ph /\ ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) ) -> F e. A )
39 eluzelz 
 |-  ( y e. ( ZZ>= ` 2 ) -> y e. ZZ )
40 39 ad2antrl 
 |-  ( ( ph /\ ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) ) -> y e. ZZ )
41 zq 
 |-  ( y e. ZZ -> y e. QQ )
42 40 41 syl 
 |-  ( ( ph /\ ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) ) -> y e. QQ )
43 eluzelz 
 |-  ( z e. ( ZZ>= ` 2 ) -> z e. ZZ )
44 43 ad2antll 
 |-  ( ( ph /\ ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) ) -> z e. ZZ )
45 zq 
 |-  ( z e. ZZ -> z e. QQ )
46 44 45 syl 
 |-  ( ( ph /\ ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) ) -> z e. QQ )
47 1 qrngbas 
 |-  QQ = ( Base ` Q )
48 qex 
 |-  QQ e. _V
49 cnfldmul 
 |-  x. = ( .r ` CCfld )
50 1 49 ressmulr 
 |-  ( QQ e. _V -> x. = ( .r ` Q ) )
51 48 50 ax-mp 
 |-  x. = ( .r ` Q )
52 2 47 51 abvmul 
 |-  ( ( F e. A /\ y e. QQ /\ z e. QQ ) -> ( F ` ( y x. z ) ) = ( ( F ` y ) x. ( F ` z ) ) )
53 38 42 46 52 syl3anc 
 |-  ( ( ph /\ ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) ) -> ( F ` ( y x. z ) ) = ( ( F ` y ) x. ( F ` z ) ) )
54 4 adantr 
 |-  ( ( ph /\ ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) ) -> G e. A )
55 2 47 51 abvmul 
 |-  ( ( G e. A /\ y e. QQ /\ z e. QQ ) -> ( G ` ( y x. z ) ) = ( ( G ` y ) x. ( G ` z ) ) )
56 54 42 46 55 syl3anc 
 |-  ( ( ph /\ ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) ) -> ( G ` ( y x. z ) ) = ( ( G ` y ) x. ( G ` z ) ) )
57 53 56 eqeq12d 
 |-  ( ( ph /\ ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) ) -> ( ( F ` ( y x. z ) ) = ( G ` ( y x. z ) ) <-> ( ( F ` y ) x. ( F ` z ) ) = ( ( G ` y ) x. ( G ` z ) ) ) )
58 37 57 imbitrrid 
 |-  ( ( ph /\ ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) ) -> ( ( ( F ` y ) = ( G ` y ) /\ ( F ` z ) = ( G ` z ) ) -> ( F ` ( y x. z ) ) = ( G ` ( y x. z ) ) ) )
59 58 expcom 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ph -> ( ( ( F ` y ) = ( G ` y ) /\ ( F ` z ) = ( G ` z ) ) -> ( F ` ( y x. z ) ) = ( G ` ( y x. z ) ) ) ) )
60 59 a2d 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ph -> ( ( F ` y ) = ( G ` y ) /\ ( F ` z ) = ( G ` z ) ) ) -> ( ph -> ( F ` ( y x. z ) ) = ( G ` ( y x. z ) ) ) ) )
61 36 60 biimtrrid 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ( ph -> ( F ` y ) = ( G ` y ) ) /\ ( ph -> ( F ` z ) = ( G ` z ) ) ) -> ( ph -> ( F ` ( y x. z ) ) = ( G ` ( y x. z ) ) ) ) )
62 10 14 18 22 26 34 35 61 prmind 
 |-  ( n e. NN -> ( ph -> ( F ` n ) = ( G ` n ) ) )
63 62 impcom 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = ( G ` n ) )
64 6 63 sylan2 
 |-  ( ( ph /\ n e. ( ZZ>= ` 2 ) ) -> ( F ` n ) = ( G ` n ) )
65 1 2 3 4 64 ostthlem1 
 |-  ( ph -> F = G )