Metamath Proof Explorer

Theorem phimullem

Description: Lemma for phimul . (Contributed by Mario Carneiro, 24-Feb-2014)

Ref Expression
Hypotheses crth.1 
|- S = ( 0 ..^ ( M x. N ) )
crth.2 
|- T = ( ( 0 ..^ M ) X. ( 0 ..^ N ) )
crth.3 
|- F = ( x e. S |-> <. ( x mod M ) , ( x mod N ) >. )
crth.4 
|- ( ph -> ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) )
phimul.4 
|- U = { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 }
phimul.5 
|- V = { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 }
phimul.6 
|- W = { y e. S | ( y gcd ( M x. N ) ) = 1 }
Assertion phimullem 
|- ( ph -> ( phi ` ( M x. N ) ) = ( ( phi ` M ) x. ( phi ` N ) ) )

Proof

Step Hyp Ref Expression
1 crth.1 
 |-  S = ( 0 ..^ ( M x. N ) )
2 crth.2 
 |-  T = ( ( 0 ..^ M ) X. ( 0 ..^ N ) )
3 crth.3 
 |-  F = ( x e. S |-> <. ( x mod M ) , ( x mod N ) >. )
4 crth.4 
 |-  ( ph -> ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) )
5 phimul.4 
 |-  U = { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 }
6 phimul.5 
 |-  V = { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 }
7 phimul.6 
 |-  W = { y e. S | ( y gcd ( M x. N ) ) = 1 }
8 fzofi 
 |-  ( 0 ..^ M ) e. Fin
9 ssrab2 
 |-  { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 } C_ ( 0 ..^ M )
10 ssfi 
 |-  ( ( ( 0 ..^ M ) e. Fin /\ { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 } C_ ( 0 ..^ M ) ) -> { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 } e. Fin )
11 8 9 10 mp2an 
 |-  { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 } e. Fin
12 5 11 eqeltri 
 |-  U e. Fin
13 fzofi 
 |-  ( 0 ..^ N ) e. Fin
14 ssrab2 
 |-  { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 } C_ ( 0 ..^ N )
15 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 } C_ ( 0 ..^ N ) ) -> { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 } e. Fin )
16 13 14 15 mp2an 
 |-  { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 } e. Fin
17 6 16 eqeltri 
 |-  V e. Fin
18 hashxp 
 |-  ( ( U e. Fin /\ V e. Fin ) -> ( # ` ( U X. V ) ) = ( ( # ` U ) x. ( # ` V ) ) )
19 12 17 18 mp2an 
 |-  ( # ` ( U X. V ) ) = ( ( # ` U ) x. ( # ` V ) )
20 oveq1 
 |-  ( y = w -> ( y gcd ( M x. N ) ) = ( w gcd ( M x. N ) ) )
21 20 eqeq1d 
 |-  ( y = w -> ( ( y gcd ( M x. N ) ) = 1 <-> ( w gcd ( M x. N ) ) = 1 ) )
22 21 7 elrab2 
 |-  ( w e. W <-> ( w e. S /\ ( w gcd ( M x. N ) ) = 1 ) )
23 22 simplbi 
 |-  ( w e. W -> w e. S )
24 oveq1 
 |-  ( x = w -> ( x mod M ) = ( w mod M ) )
25 oveq1 
 |-  ( x = w -> ( x mod N ) = ( w mod N ) )
26 24 25 opeq12d 
 |-  ( x = w -> <. ( x mod M ) , ( x mod N ) >. = <. ( w mod M ) , ( w mod N ) >. )
27 opex 
 |-  <. ( w mod M ) , ( w mod N ) >. e. _V
28 26 3 27 fvmpt 
 |-  ( w e. S -> ( F ` w ) = <. ( w mod M ) , ( w mod N ) >. )
29 23 28 syl 
 |-  ( w e. W -> ( F ` w ) = <. ( w mod M ) , ( w mod N ) >. )
30 29 adantl 
 |-  ( ( ph /\ w e. W ) -> ( F ` w ) = <. ( w mod M ) , ( w mod N ) >. )
31 23 1 eleqtrdi 
 |-  ( w e. W -> w e. ( 0 ..^ ( M x. N ) ) )
32 31 adantl 
 |-  ( ( ph /\ w e. W ) -> w e. ( 0 ..^ ( M x. N ) ) )
33 elfzoelz 
 |-  ( w e. ( 0 ..^ ( M x. N ) ) -> w e. ZZ )
34 32 33 syl 
 |-  ( ( ph /\ w e. W ) -> w e. ZZ )
35 4 simp1d 
 |-  ( ph -> M e. NN )
36 35 adantr 
 |-  ( ( ph /\ w e. W ) -> M e. NN )
37 zmodfzo 
 |-  ( ( w e. ZZ /\ M e. NN ) -> ( w mod M ) e. ( 0 ..^ M ) )
38 34 36 37 syl2anc 
 |-  ( ( ph /\ w e. W ) -> ( w mod M ) e. ( 0 ..^ M ) )
39 modgcd 
 |-  ( ( w e. ZZ /\ M e. NN ) -> ( ( w mod M ) gcd M ) = ( w gcd M ) )
40 34 36 39 syl2anc 
 |-  ( ( ph /\ w e. W ) -> ( ( w mod M ) gcd M ) = ( w gcd M ) )
41 36 nnzd 
 |-  ( ( ph /\ w e. W ) -> M e. ZZ )
42 gcddvds 
 |-  ( ( w e. ZZ /\ M e. ZZ ) -> ( ( w gcd M ) || w /\ ( w gcd M ) || M ) )
43 34 41 42 syl2anc 
 |-  ( ( ph /\ w e. W ) -> ( ( w gcd M ) || w /\ ( w gcd M ) || M ) )
44 43 simpld 
 |-  ( ( ph /\ w e. W ) -> ( w gcd M ) || w )
45 nnne0 
 |-  ( M e. NN -> M =/= 0 )
46 simpr 
 |-  ( ( w = 0 /\ M = 0 ) -> M = 0 )
47 46 necon3ai 
 |-  ( M =/= 0 -> -. ( w = 0 /\ M = 0 ) )
48 36 45 47 3syl 
 |-  ( ( ph /\ w e. W ) -> -. ( w = 0 /\ M = 0 ) )
49 gcdn0cl 
 |-  ( ( ( w e. ZZ /\ M e. ZZ ) /\ -. ( w = 0 /\ M = 0 ) ) -> ( w gcd M ) e. NN )
50 34 41 48 49 syl21anc 
 |-  ( ( ph /\ w e. W ) -> ( w gcd M ) e. NN )
51 50 nnzd 
 |-  ( ( ph /\ w e. W ) -> ( w gcd M ) e. ZZ )
52 4 simp2d 
 |-  ( ph -> N e. NN )
53 52 adantr 
 |-  ( ( ph /\ w e. W ) -> N e. NN )
54 53 nnzd 
 |-  ( ( ph /\ w e. W ) -> N e. ZZ )
55 43 simprd 
 |-  ( ( ph /\ w e. W ) -> ( w gcd M ) || M )
56 51 41 54 55 dvdsmultr1d 
 |-  ( ( ph /\ w e. W ) -> ( w gcd M ) || ( M x. N ) )
57 36 53 nnmulcld 
 |-  ( ( ph /\ w e. W ) -> ( M x. N ) e. NN )
58 57 nnzd 
 |-  ( ( ph /\ w e. W ) -> ( M x. N ) e. ZZ )
59 nnne0 
 |-  ( ( M x. N ) e. NN -> ( M x. N ) =/= 0 )
60 simpr 
 |-  ( ( w = 0 /\ ( M x. N ) = 0 ) -> ( M x. N ) = 0 )
61 60 necon3ai 
 |-  ( ( M x. N ) =/= 0 -> -. ( w = 0 /\ ( M x. N ) = 0 ) )
62 57 59 61 3syl 
 |-  ( ( ph /\ w e. W ) -> -. ( w = 0 /\ ( M x. N ) = 0 ) )
63 dvdslegcd 
 |-  ( ( ( ( w gcd M ) e. ZZ /\ w e. ZZ /\ ( M x. N ) e. ZZ ) /\ -. ( w = 0 /\ ( M x. N ) = 0 ) ) -> ( ( ( w gcd M ) || w /\ ( w gcd M ) || ( M x. N ) ) -> ( w gcd M ) <_ ( w gcd ( M x. N ) ) ) )
64 51 34 58 62 63 syl31anc 
 |-  ( ( ph /\ w e. W ) -> ( ( ( w gcd M ) || w /\ ( w gcd M ) || ( M x. N ) ) -> ( w gcd M ) <_ ( w gcd ( M x. N ) ) ) )
65 44 56 64 mp2and 
 |-  ( ( ph /\ w e. W ) -> ( w gcd M ) <_ ( w gcd ( M x. N ) ) )
66 22 simprbi 
 |-  ( w e. W -> ( w gcd ( M x. N ) ) = 1 )
67 66 adantl 
 |-  ( ( ph /\ w e. W ) -> ( w gcd ( M x. N ) ) = 1 )
68 65 67 breqtrd 
 |-  ( ( ph /\ w e. W ) -> ( w gcd M ) <_ 1 )
69 nnle1eq1 
 |-  ( ( w gcd M ) e. NN -> ( ( w gcd M ) <_ 1 <-> ( w gcd M ) = 1 ) )
70 50 69 syl 
 |-  ( ( ph /\ w e. W ) -> ( ( w gcd M ) <_ 1 <-> ( w gcd M ) = 1 ) )
71 68 70 mpbid 
 |-  ( ( ph /\ w e. W ) -> ( w gcd M ) = 1 )
72 40 71 eqtrd 
 |-  ( ( ph /\ w e. W ) -> ( ( w mod M ) gcd M ) = 1 )
73 oveq1 
 |-  ( y = ( w mod M ) -> ( y gcd M ) = ( ( w mod M ) gcd M ) )
74 73 eqeq1d 
 |-  ( y = ( w mod M ) -> ( ( y gcd M ) = 1 <-> ( ( w mod M ) gcd M ) = 1 ) )
75 74 5 elrab2 
 |-  ( ( w mod M ) e. U <-> ( ( w mod M ) e. ( 0 ..^ M ) /\ ( ( w mod M ) gcd M ) = 1 ) )
76 38 72 75 sylanbrc 
 |-  ( ( ph /\ w e. W ) -> ( w mod M ) e. U )
77 zmodfzo 
 |-  ( ( w e. ZZ /\ N e. NN ) -> ( w mod N ) e. ( 0 ..^ N ) )
78 34 53 77 syl2anc 
 |-  ( ( ph /\ w e. W ) -> ( w mod N ) e. ( 0 ..^ N ) )
79 modgcd 
 |-  ( ( w e. ZZ /\ N e. NN ) -> ( ( w mod N ) gcd N ) = ( w gcd N ) )
80 34 53 79 syl2anc 
 |-  ( ( ph /\ w e. W ) -> ( ( w mod N ) gcd N ) = ( w gcd N ) )
81 gcddvds 
 |-  ( ( w e. ZZ /\ N e. ZZ ) -> ( ( w gcd N ) || w /\ ( w gcd N ) || N ) )
82 34 54 81 syl2anc 
 |-  ( ( ph /\ w e. W ) -> ( ( w gcd N ) || w /\ ( w gcd N ) || N ) )
83 82 simpld 
 |-  ( ( ph /\ w e. W ) -> ( w gcd N ) || w )
84 nnne0 
 |-  ( N e. NN -> N =/= 0 )
85 simpr 
 |-  ( ( w = 0 /\ N = 0 ) -> N = 0 )
86 85 necon3ai 
 |-  ( N =/= 0 -> -. ( w = 0 /\ N = 0 ) )
87 53 84 86 3syl 
 |-  ( ( ph /\ w e. W ) -> -. ( w = 0 /\ N = 0 ) )
88 gcdn0cl 
 |-  ( ( ( w e. ZZ /\ N e. ZZ ) /\ -. ( w = 0 /\ N = 0 ) ) -> ( w gcd N ) e. NN )
89 34 54 87 88 syl21anc 
 |-  ( ( ph /\ w e. W ) -> ( w gcd N ) e. NN )
90 89 nnzd 
 |-  ( ( ph /\ w e. W ) -> ( w gcd N ) e. ZZ )
91 82 simprd 
 |-  ( ( ph /\ w e. W ) -> ( w gcd N ) || N )
92 dvdsmul2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N || ( M x. N ) )
93 41 54 92 syl2anc 
 |-  ( ( ph /\ w e. W ) -> N || ( M x. N ) )
94 90 54 58 91 93 dvdstrd 
 |-  ( ( ph /\ w e. W ) -> ( w gcd N ) || ( M x. N ) )
95 dvdslegcd 
 |-  ( ( ( ( w gcd N ) e. ZZ /\ w e. ZZ /\ ( M x. N ) e. ZZ ) /\ -. ( w = 0 /\ ( M x. N ) = 0 ) ) -> ( ( ( w gcd N ) || w /\ ( w gcd N ) || ( M x. N ) ) -> ( w gcd N ) <_ ( w gcd ( M x. N ) ) ) )
96 90 34 58 62 95 syl31anc 
 |-  ( ( ph /\ w e. W ) -> ( ( ( w gcd N ) || w /\ ( w gcd N ) || ( M x. N ) ) -> ( w gcd N ) <_ ( w gcd ( M x. N ) ) ) )
97 83 94 96 mp2and 
 |-  ( ( ph /\ w e. W ) -> ( w gcd N ) <_ ( w gcd ( M x. N ) ) )
98 97 67 breqtrd 
 |-  ( ( ph /\ w e. W ) -> ( w gcd N ) <_ 1 )
99 nnle1eq1 
 |-  ( ( w gcd N ) e. NN -> ( ( w gcd N ) <_ 1 <-> ( w gcd N ) = 1 ) )
100 89 99 syl 
 |-  ( ( ph /\ w e. W ) -> ( ( w gcd N ) <_ 1 <-> ( w gcd N ) = 1 ) )
101 98 100 mpbid 
 |-  ( ( ph /\ w e. W ) -> ( w gcd N ) = 1 )
102 80 101 eqtrd 
 |-  ( ( ph /\ w e. W ) -> ( ( w mod N ) gcd N ) = 1 )
103 oveq1 
 |-  ( y = ( w mod N ) -> ( y gcd N ) = ( ( w mod N ) gcd N ) )
104 103 eqeq1d 
 |-  ( y = ( w mod N ) -> ( ( y gcd N ) = 1 <-> ( ( w mod N ) gcd N ) = 1 ) )
105 104 6 elrab2 
 |-  ( ( w mod N ) e. V <-> ( ( w mod N ) e. ( 0 ..^ N ) /\ ( ( w mod N ) gcd N ) = 1 ) )
106 78 102 105 sylanbrc 
 |-  ( ( ph /\ w e. W ) -> ( w mod N ) e. V )
107 76 106 opelxpd 
 |-  ( ( ph /\ w e. W ) -> <. ( w mod M ) , ( w mod N ) >. e. ( U X. V ) )
108 30 107 eqeltrd 
 |-  ( ( ph /\ w e. W ) -> ( F ` w ) e. ( U X. V ) )
109 108 ralrimiva 
 |-  ( ph -> A. w e. W ( F ` w ) e. ( U X. V ) )
110 1 2 3 4 crth 
 |-  ( ph -> F : S -1-1-onto-> T )
111 f1ofn 
 |-  ( F : S -1-1-onto-> T -> F Fn S )
112 fnfun 
 |-  ( F Fn S -> Fun F )
113 110 111 112 3syl 
 |-  ( ph -> Fun F )
114 7 ssrab3 
 |-  W C_ S
115 fndm 
 |-  ( F Fn S -> dom F = S )
116 110 111 115 3syl 
 |-  ( ph -> dom F = S )
117 114 116 sseqtrrid 
 |-  ( ph -> W C_ dom F )
118 funimass4 
 |-  ( ( Fun F /\ W C_ dom F ) -> ( ( F " W ) C_ ( U X. V ) <-> A. w e. W ( F ` w ) e. ( U X. V ) ) )
119 113 117 118 syl2anc 
 |-  ( ph -> ( ( F " W ) C_ ( U X. V ) <-> A. w e. W ( F ` w ) e. ( U X. V ) ) )
120 109 119 mpbird 
 |-  ( ph -> ( F " W ) C_ ( U X. V ) )
121 5 ssrab3 
 |-  U C_ ( 0 ..^ M )
122 6 ssrab3 
 |-  V C_ ( 0 ..^ N )
123 xpss12 
 |-  ( ( U C_ ( 0 ..^ M ) /\ V C_ ( 0 ..^ N ) ) -> ( U X. V ) C_ ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) )
124 121 122 123 mp2an 
 |-  ( U X. V ) C_ ( ( 0 ..^ M ) X. ( 0 ..^ N ) )
125 124 2 sseqtrri 
 |-  ( U X. V ) C_ T
126 125 sseli 
 |-  ( z e. ( U X. V ) -> z e. T )
127 f1ocnvfv2 
 |-  ( ( F : S -1-1-onto-> T /\ z e. T ) -> ( F ` ( `' F ` z ) ) = z )
128 110 126 127 syl2an 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( F ` ( `' F ` z ) ) = z )
129 f1ocnv 
 |-  ( F : S -1-1-onto-> T -> `' F : T -1-1-onto-> S )
130 f1of 
 |-  ( `' F : T -1-1-onto-> S -> `' F : T --> S )
131 110 129 130 3syl 
 |-  ( ph -> `' F : T --> S )
132 ffvelrn 
 |-  ( ( `' F : T --> S /\ z e. T ) -> ( `' F ` z ) e. S )
133 131 126 132 syl2an 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( `' F ` z ) e. S )
134 133 1 eleqtrdi 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( `' F ` z ) e. ( 0 ..^ ( M x. N ) ) )
135 elfzoelz 
 |-  ( ( `' F ` z ) e. ( 0 ..^ ( M x. N ) ) -> ( `' F ` z ) e. ZZ )
136 134 135 syl 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( `' F ` z ) e. ZZ )
137 35 adantr 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> M e. NN )
138 modgcd 
 |-  ( ( ( `' F ` z ) e. ZZ /\ M e. NN ) -> ( ( ( `' F ` z ) mod M ) gcd M ) = ( ( `' F ` z ) gcd M ) )
139 136 137 138 syl2anc 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( ( `' F ` z ) mod M ) gcd M ) = ( ( `' F ` z ) gcd M ) )
140 oveq1 
 |-  ( w = ( `' F ` z ) -> ( w mod M ) = ( ( `' F ` z ) mod M ) )
141 oveq1 
 |-  ( w = ( `' F ` z ) -> ( w mod N ) = ( ( `' F ` z ) mod N ) )
142 140 141 opeq12d 
 |-  ( w = ( `' F ` z ) -> <. ( w mod M ) , ( w mod N ) >. = <. ( ( `' F ` z ) mod M ) , ( ( `' F ` z ) mod N ) >. )
143 26 cbvmptv 
 |-  ( x e. S |-> <. ( x mod M ) , ( x mod N ) >. ) = ( w e. S |-> <. ( w mod M ) , ( w mod N ) >. )
144 3 143 eqtri 
 |-  F = ( w e. S |-> <. ( w mod M ) , ( w mod N ) >. )
145 opex 
 |-  <. ( ( `' F ` z ) mod M ) , ( ( `' F ` z ) mod N ) >. e. _V
146 142 144 145 fvmpt 
 |-  ( ( `' F ` z ) e. S -> ( F ` ( `' F ` z ) ) = <. ( ( `' F ` z ) mod M ) , ( ( `' F ` z ) mod N ) >. )
147 133 146 syl 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( F ` ( `' F ` z ) ) = <. ( ( `' F ` z ) mod M ) , ( ( `' F ` z ) mod N ) >. )
148 128 147 eqtr3d 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> z = <. ( ( `' F ` z ) mod M ) , ( ( `' F ` z ) mod N ) >. )
149 simpr 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> z e. ( U X. V ) )
150 148 149 eqeltrrd 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> <. ( ( `' F ` z ) mod M ) , ( ( `' F ` z ) mod N ) >. e. ( U X. V ) )
151 opelxp 
 |-  ( <. ( ( `' F ` z ) mod M ) , ( ( `' F ` z ) mod N ) >. e. ( U X. V ) <-> ( ( ( `' F ` z ) mod M ) e. U /\ ( ( `' F ` z ) mod N ) e. V ) )
152 150 151 sylib 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( ( `' F ` z ) mod M ) e. U /\ ( ( `' F ` z ) mod N ) e. V ) )
153 152 simpld 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( `' F ` z ) mod M ) e. U )
154 oveq1 
 |-  ( y = ( ( `' F ` z ) mod M ) -> ( y gcd M ) = ( ( ( `' F ` z ) mod M ) gcd M ) )
155 154 eqeq1d 
 |-  ( y = ( ( `' F ` z ) mod M ) -> ( ( y gcd M ) = 1 <-> ( ( ( `' F ` z ) mod M ) gcd M ) = 1 ) )
156 155 5 elrab2 
 |-  ( ( ( `' F ` z ) mod M ) e. U <-> ( ( ( `' F ` z ) mod M ) e. ( 0 ..^ M ) /\ ( ( ( `' F ` z ) mod M ) gcd M ) = 1 ) )
157 153 156 sylib 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( ( `' F ` z ) mod M ) e. ( 0 ..^ M ) /\ ( ( ( `' F ` z ) mod M ) gcd M ) = 1 ) )
158 157 simprd 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( ( `' F ` z ) mod M ) gcd M ) = 1 )
159 139 158 eqtr3d 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( `' F ` z ) gcd M ) = 1 )
160 52 adantr 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> N e. NN )
161 modgcd 
 |-  ( ( ( `' F ` z ) e. ZZ /\ N e. NN ) -> ( ( ( `' F ` z ) mod N ) gcd N ) = ( ( `' F ` z ) gcd N ) )
162 136 160 161 syl2anc 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( ( `' F ` z ) mod N ) gcd N ) = ( ( `' F ` z ) gcd N ) )
163 152 simprd 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( `' F ` z ) mod N ) e. V )
164 oveq1 
 |-  ( y = ( ( `' F ` z ) mod N ) -> ( y gcd N ) = ( ( ( `' F ` z ) mod N ) gcd N ) )
165 164 eqeq1d 
 |-  ( y = ( ( `' F ` z ) mod N ) -> ( ( y gcd N ) = 1 <-> ( ( ( `' F ` z ) mod N ) gcd N ) = 1 ) )
166 165 6 elrab2 
 |-  ( ( ( `' F ` z ) mod N ) e. V <-> ( ( ( `' F ` z ) mod N ) e. ( 0 ..^ N ) /\ ( ( ( `' F ` z ) mod N ) gcd N ) = 1 ) )
167 163 166 sylib 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( ( `' F ` z ) mod N ) e. ( 0 ..^ N ) /\ ( ( ( `' F ` z ) mod N ) gcd N ) = 1 ) )
168 167 simprd 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( ( `' F ` z ) mod N ) gcd N ) = 1 )
169 162 168 eqtr3d 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( `' F ` z ) gcd N ) = 1 )
170 35 nnzd 
 |-  ( ph -> M e. ZZ )
171 170 adantr 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> M e. ZZ )
172 52 nnzd 
 |-  ( ph -> N e. ZZ )
173 172 adantr 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> N e. ZZ )
174 rpmul 
 |-  ( ( ( `' F ` z ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( ( `' F ` z ) gcd M ) = 1 /\ ( ( `' F ` z ) gcd N ) = 1 ) -> ( ( `' F ` z ) gcd ( M x. N ) ) = 1 ) )
175 136 171 173 174 syl3anc 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( ( ( `' F ` z ) gcd M ) = 1 /\ ( ( `' F ` z ) gcd N ) = 1 ) -> ( ( `' F ` z ) gcd ( M x. N ) ) = 1 ) )
176 159 169 175 mp2and 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( ( `' F ` z ) gcd ( M x. N ) ) = 1 )
177 oveq1 
 |-  ( y = ( `' F ` z ) -> ( y gcd ( M x. N ) ) = ( ( `' F ` z ) gcd ( M x. N ) ) )
178 177 eqeq1d 
 |-  ( y = ( `' F ` z ) -> ( ( y gcd ( M x. N ) ) = 1 <-> ( ( `' F ` z ) gcd ( M x. N ) ) = 1 ) )
179 178 7 elrab2 
 |-  ( ( `' F ` z ) e. W <-> ( ( `' F ` z ) e. S /\ ( ( `' F ` z ) gcd ( M x. N ) ) = 1 ) )
180 133 176 179 sylanbrc 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( `' F ` z ) e. W )
181 funfvima2 
 |-  ( ( Fun F /\ W C_ dom F ) -> ( ( `' F ` z ) e. W -> ( F ` ( `' F ` z ) ) e. ( F " W ) ) )
182 113 117 181 syl2anc 
 |-  ( ph -> ( ( `' F ` z ) e. W -> ( F ` ( `' F ` z ) ) e. ( F " W ) ) )
183 182 imp 
 |-  ( ( ph /\ ( `' F ` z ) e. W ) -> ( F ` ( `' F ` z ) ) e. ( F " W ) )
184 180 183 syldan 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> ( F ` ( `' F ` z ) ) e. ( F " W ) )
185 128 184 eqeltrrd 
 |-  ( ( ph /\ z e. ( U X. V ) ) -> z e. ( F " W ) )
186 120 185 eqelssd 
 |-  ( ph -> ( F " W ) = ( U X. V ) )
187 f1of1 
 |-  ( F : S -1-1-onto-> T -> F : S -1-1-> T )
188 110 187 syl 
 |-  ( ph -> F : S -1-1-> T )
189 fzofi 
 |-  ( 0 ..^ ( M x. N ) ) e. Fin
190 1 189 eqeltri 
 |-  S e. Fin
191 ssfi 
 |-  ( ( S e. Fin /\ W C_ S ) -> W e. Fin )
192 190 114 191 mp2an 
 |-  W e. Fin
193 192 elexi 
 |-  W e. _V
194 193 f1imaen 
 |-  ( ( F : S -1-1-> T /\ W C_ S ) -> ( F " W ) ~~ W )
195 188 114 194 sylancl 
 |-  ( ph -> ( F " W ) ~~ W )
196 186 195 eqbrtrrd 
 |-  ( ph -> ( U X. V ) ~~ W )
197 xpfi 
 |-  ( ( U e. Fin /\ V e. Fin ) -> ( U X. V ) e. Fin )
198 12 17 197 mp2an 
 |-  ( U X. V ) e. Fin
199 hashen 
 |-  ( ( ( U X. V ) e. Fin /\ W e. Fin ) -> ( ( # ` ( U X. V ) ) = ( # ` W ) <-> ( U X. V ) ~~ W ) )
200 198 192 199 mp2an 
 |-  ( ( # ` ( U X. V ) ) = ( # ` W ) <-> ( U X. V ) ~~ W )
201 196 200 sylibr 
 |-  ( ph -> ( # ` ( U X. V ) ) = ( # ` W ) )
202 19 201 syl5reqr 
 |-  ( ph -> ( # ` W ) = ( ( # ` U ) x. ( # ` V ) ) )
203 35 52 nnmulcld 
 |-  ( ph -> ( M x. N ) e. NN )
204 dfphi2 
 |-  ( ( M x. N ) e. NN -> ( phi ` ( M x. N ) ) = ( # ` { y e. ( 0 ..^ ( M x. N ) ) | ( y gcd ( M x. N ) ) = 1 } ) )
205 1 rabeqi 
 |-  { y e. S | ( y gcd ( M x. N ) ) = 1 } = { y e. ( 0 ..^ ( M x. N ) ) | ( y gcd ( M x. N ) ) = 1 }
206 7 205 eqtri 
 |-  W = { y e. ( 0 ..^ ( M x. N ) ) | ( y gcd ( M x. N ) ) = 1 }
207 206 fveq2i 
 |-  ( # ` W ) = ( # ` { y e. ( 0 ..^ ( M x. N ) ) | ( y gcd ( M x. N ) ) = 1 } )
208 204 207 eqtr4di 
 |-  ( ( M x. N ) e. NN -> ( phi ` ( M x. N ) ) = ( # ` W ) )
209 203 208 syl 
 |-  ( ph -> ( phi ` ( M x. N ) ) = ( # ` W ) )
210 dfphi2 
 |-  ( M e. NN -> ( phi ` M ) = ( # ` { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 } ) )
211 5 fveq2i 
 |-  ( # ` U ) = ( # ` { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 } )
212 210 211 eqtr4di 
 |-  ( M e. NN -> ( phi ` M ) = ( # ` U ) )
213 35 212 syl 
 |-  ( ph -> ( phi ` M ) = ( # ` U ) )
214 dfphi2 
 |-  ( N e. NN -> ( phi ` N ) = ( # ` { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 } ) )
215 6 fveq2i 
 |-  ( # ` V ) = ( # ` { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 } )
216 214 215 eqtr4di 
 |-  ( N e. NN -> ( phi ` N ) = ( # ` V ) )
217 52 216 syl 
 |-  ( ph -> ( phi ` N ) = ( # ` V ) )
218 213 217 oveq12d 
 |-  ( ph -> ( ( phi ` M ) x. ( phi ` N ) ) = ( ( # ` U ) x. ( # ` V ) ) )
219 202 209 218 3eqtr4d 
 |-  ( ph -> ( phi ` ( M x. N ) ) = ( ( phi ` M ) x. ( phi ` N ) ) )