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