Metamath Proof Explorer


Theorem dvdsmulf1o

Description: If M and N are two coprime integers, multiplication forms a bijection from the set of pairs <. j , k >. where j || M and k || N , to the set of divisors of M x. N . (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Hypotheses dvdsmulf1o.1
|- ( ph -> M e. NN )
dvdsmulf1o.2
|- ( ph -> N e. NN )
dvdsmulf1o.3
|- ( ph -> ( M gcd N ) = 1 )
dvdsmulf1o.x
|- X = { x e. NN | x || M }
dvdsmulf1o.y
|- Y = { x e. NN | x || N }
dvdsmulf1o.z
|- Z = { x e. NN | x || ( M x. N ) }
Assertion dvdsmulf1o
|- ( ph -> ( x. |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z )

Proof

Step Hyp Ref Expression
1 dvdsmulf1o.1
 |-  ( ph -> M e. NN )
2 dvdsmulf1o.2
 |-  ( ph -> N e. NN )
3 dvdsmulf1o.3
 |-  ( ph -> ( M gcd N ) = 1 )
4 dvdsmulf1o.x
 |-  X = { x e. NN | x || M }
5 dvdsmulf1o.y
 |-  Y = { x e. NN | x || N }
6 dvdsmulf1o.z
 |-  Z = { x e. NN | x || ( M x. N ) }
7 ax-mulf
 |-  x. : ( CC X. CC ) --> CC
8 ffn
 |-  ( x. : ( CC X. CC ) --> CC -> x. Fn ( CC X. CC ) )
9 7 8 ax-mp
 |-  x. Fn ( CC X. CC )
10 4 ssrab3
 |-  X C_ NN
11 nnsscn
 |-  NN C_ CC
12 10 11 sstri
 |-  X C_ CC
13 5 ssrab3
 |-  Y C_ NN
14 13 11 sstri
 |-  Y C_ CC
15 xpss12
 |-  ( ( X C_ CC /\ Y C_ CC ) -> ( X X. Y ) C_ ( CC X. CC ) )
16 12 14 15 mp2an
 |-  ( X X. Y ) C_ ( CC X. CC )
17 fnssres
 |-  ( ( x. Fn ( CC X. CC ) /\ ( X X. Y ) C_ ( CC X. CC ) ) -> ( x. |` ( X X. Y ) ) Fn ( X X. Y ) )
18 9 16 17 mp2an
 |-  ( x. |` ( X X. Y ) ) Fn ( X X. Y )
19 18 a1i
 |-  ( ph -> ( x. |` ( X X. Y ) ) Fn ( X X. Y ) )
20 ovres
 |-  ( ( i e. X /\ j e. Y ) -> ( i ( x. |` ( X X. Y ) ) j ) = ( i x. j ) )
21 20 adantl
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i ( x. |` ( X X. Y ) ) j ) = ( i x. j ) )
22 breq1
 |-  ( x = i -> ( x || M <-> i || M ) )
23 22 4 elrab2
 |-  ( i e. X <-> ( i e. NN /\ i || M ) )
24 23 simplbi
 |-  ( i e. X -> i e. NN )
25 24 ad2antrl
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> i e. NN )
26 breq1
 |-  ( x = j -> ( x || N <-> j || N ) )
27 26 5 elrab2
 |-  ( j e. Y <-> ( j e. NN /\ j || N ) )
28 27 simplbi
 |-  ( j e. Y -> j e. NN )
29 28 ad2antll
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> j e. NN )
30 25 29 nnmulcld
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. j ) e. NN )
31 27 simprbi
 |-  ( j e. Y -> j || N )
32 31 ad2antll
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> j || N )
33 23 simprbi
 |-  ( i e. X -> i || M )
34 33 ad2antrl
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> i || M )
35 29 nnzd
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> j e. ZZ )
36 2 adantr
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> N e. NN )
37 36 nnzd
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> N e. ZZ )
38 25 nnzd
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> i e. ZZ )
39 dvdscmul
 |-  ( ( j e. ZZ /\ N e. ZZ /\ i e. ZZ ) -> ( j || N -> ( i x. j ) || ( i x. N ) ) )
40 35 37 38 39 syl3anc
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( j || N -> ( i x. j ) || ( i x. N ) ) )
41 1 adantr
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> M e. NN )
42 41 nnzd
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> M e. ZZ )
43 dvdsmulc
 |-  ( ( i e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( i || M -> ( i x. N ) || ( M x. N ) ) )
44 38 42 37 43 syl3anc
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i || M -> ( i x. N ) || ( M x. N ) ) )
45 30 nnzd
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. j ) e. ZZ )
46 38 37 zmulcld
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. N ) e. ZZ )
47 42 37 zmulcld
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( M x. N ) e. ZZ )
48 dvdstr
 |-  ( ( ( i x. j ) e. ZZ /\ ( i x. N ) e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( ( i x. j ) || ( i x. N ) /\ ( i x. N ) || ( M x. N ) ) -> ( i x. j ) || ( M x. N ) ) )
49 45 46 47 48 syl3anc
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( ( ( i x. j ) || ( i x. N ) /\ ( i x. N ) || ( M x. N ) ) -> ( i x. j ) || ( M x. N ) ) )
50 40 44 49 syl2and
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( ( j || N /\ i || M ) -> ( i x. j ) || ( M x. N ) ) )
51 32 34 50 mp2and
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. j ) || ( M x. N ) )
52 breq1
 |-  ( x = ( i x. j ) -> ( x || ( M x. N ) <-> ( i x. j ) || ( M x. N ) ) )
53 52 6 elrab2
 |-  ( ( i x. j ) e. Z <-> ( ( i x. j ) e. NN /\ ( i x. j ) || ( M x. N ) ) )
54 30 51 53 sylanbrc
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. j ) e. Z )
55 21 54 eqeltrd
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i ( x. |` ( X X. Y ) ) j ) e. Z )
56 55 ralrimivva
 |-  ( ph -> A. i e. X A. j e. Y ( i ( x. |` ( X X. Y ) ) j ) e. Z )
57 ffnov
 |-  ( ( x. |` ( X X. Y ) ) : ( X X. Y ) --> Z <-> ( ( x. |` ( X X. Y ) ) Fn ( X X. Y ) /\ A. i e. X A. j e. Y ( i ( x. |` ( X X. Y ) ) j ) e. Z ) )
58 19 56 57 sylanbrc
 |-  ( ph -> ( x. |` ( X X. Y ) ) : ( X X. Y ) --> Z )
59 25 adantr
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i e. NN )
60 59 nnnn0d
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i e. NN0 )
61 simprll
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m e. X )
62 breq1
 |-  ( x = m -> ( x || M <-> m || M ) )
63 62 4 elrab2
 |-  ( m e. X <-> ( m e. NN /\ m || M ) )
64 63 simplbi
 |-  ( m e. X -> m e. NN )
65 61 64 syl
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m e. NN )
66 65 nnnn0d
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m e. NN0 )
67 59 nnzd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i e. ZZ )
68 29 adantr
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> j e. NN )
69 68 nnzd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> j e. ZZ )
70 dvdsmul1
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> i || ( i x. j ) )
71 67 69 70 syl2anc
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i || ( i x. j ) )
72 simprr
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i x. j ) = ( m x. n ) )
73 12 61 sselid
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m e. CC )
74 simprlr
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> n e. Y )
75 breq1
 |-  ( x = n -> ( x || N <-> n || N ) )
76 75 5 elrab2
 |-  ( n e. Y <-> ( n e. NN /\ n || N ) )
77 76 simplbi
 |-  ( n e. Y -> n e. NN )
78 74 77 syl
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> n e. NN )
79 78 nncnd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> n e. CC )
80 73 79 mulcomd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( m x. n ) = ( n x. m ) )
81 72 80 eqtrd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i x. j ) = ( n x. m ) )
82 71 81 breqtrd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i || ( n x. m ) )
83 78 nnzd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> n e. ZZ )
84 37 adantr
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> N e. ZZ )
85 67 84 gcdcomd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i gcd N ) = ( N gcd i ) )
86 42 adantr
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> M e. ZZ )
87 2 nnzd
 |-  ( ph -> N e. ZZ )
88 1 nnzd
 |-  ( ph -> M e. ZZ )
89 87 88 gcdcomd
 |-  ( ph -> ( N gcd M ) = ( M gcd N ) )
90 89 3 eqtrd
 |-  ( ph -> ( N gcd M ) = 1 )
91 90 ad2antrr
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( N gcd M ) = 1 )
92 34 adantr
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i || M )
93 rpdvds
 |-  ( ( ( N e. ZZ /\ i e. ZZ /\ M e. ZZ ) /\ ( ( N gcd M ) = 1 /\ i || M ) ) -> ( N gcd i ) = 1 )
94 84 67 86 91 92 93 syl32anc
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( N gcd i ) = 1 )
95 85 94 eqtrd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i gcd N ) = 1 )
96 76 simprbi
 |-  ( n e. Y -> n || N )
97 74 96 syl
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> n || N )
98 rpdvds
 |-  ( ( ( i e. ZZ /\ n e. ZZ /\ N e. ZZ ) /\ ( ( i gcd N ) = 1 /\ n || N ) ) -> ( i gcd n ) = 1 )
99 67 83 84 95 97 98 syl32anc
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i gcd n ) = 1 )
100 65 nnzd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m e. ZZ )
101 coprmdvds
 |-  ( ( i e. ZZ /\ n e. ZZ /\ m e. ZZ ) -> ( ( i || ( n x. m ) /\ ( i gcd n ) = 1 ) -> i || m ) )
102 67 83 100 101 syl3anc
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( ( i || ( n x. m ) /\ ( i gcd n ) = 1 ) -> i || m ) )
103 82 99 102 mp2and
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i || m )
104 dvdsmul1
 |-  ( ( m e. ZZ /\ n e. ZZ ) -> m || ( m x. n ) )
105 100 83 104 syl2anc
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m || ( m x. n ) )
106 59 nncnd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i e. CC )
107 68 nncnd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> j e. CC )
108 106 107 mulcomd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i x. j ) = ( j x. i ) )
109 72 108 eqtr3d
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( m x. n ) = ( j x. i ) )
110 105 109 breqtrd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m || ( j x. i ) )
111 100 84 gcdcomd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( m gcd N ) = ( N gcd m ) )
112 63 simprbi
 |-  ( m e. X -> m || M )
113 61 112 syl
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m || M )
114 rpdvds
 |-  ( ( ( N e. ZZ /\ m e. ZZ /\ M e. ZZ ) /\ ( ( N gcd M ) = 1 /\ m || M ) ) -> ( N gcd m ) = 1 )
115 84 100 86 91 113 114 syl32anc
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( N gcd m ) = 1 )
116 111 115 eqtrd
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( m gcd N ) = 1 )
117 32 adantr
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> j || N )
118 rpdvds
 |-  ( ( ( m e. ZZ /\ j e. ZZ /\ N e. ZZ ) /\ ( ( m gcd N ) = 1 /\ j || N ) ) -> ( m gcd j ) = 1 )
119 100 69 84 116 117 118 syl32anc
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( m gcd j ) = 1 )
120 coprmdvds
 |-  ( ( m e. ZZ /\ j e. ZZ /\ i e. ZZ ) -> ( ( m || ( j x. i ) /\ ( m gcd j ) = 1 ) -> m || i ) )
121 100 69 67 120 syl3anc
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( ( m || ( j x. i ) /\ ( m gcd j ) = 1 ) -> m || i ) )
122 110 119 121 mp2and
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m || i )
123 dvdseq
 |-  ( ( ( i e. NN0 /\ m e. NN0 ) /\ ( i || m /\ m || i ) ) -> i = m )
124 60 66 103 122 123 syl22anc
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i = m )
125 59 nnne0d
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i =/= 0 )
126 124 oveq1d
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i x. n ) = ( m x. n ) )
127 72 126 eqtr4d
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i x. j ) = ( i x. n ) )
128 107 79 106 125 127 mulcanad
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> j = n )
129 124 128 opeq12d
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> <. i , j >. = <. m , n >. )
130 129 expr
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( m e. X /\ n e. Y ) ) -> ( ( i x. j ) = ( m x. n ) -> <. i , j >. = <. m , n >. ) )
131 130 ralrimivva
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> A. m e. X A. n e. Y ( ( i x. j ) = ( m x. n ) -> <. i , j >. = <. m , n >. ) )
132 131 ralrimivva
 |-  ( ph -> A. i e. X A. j e. Y A. m e. X A. n e. Y ( ( i x. j ) = ( m x. n ) -> <. i , j >. = <. m , n >. ) )
133 fvres
 |-  ( u e. ( X X. Y ) -> ( ( x. |` ( X X. Y ) ) ` u ) = ( x. ` u ) )
134 fvres
 |-  ( v e. ( X X. Y ) -> ( ( x. |` ( X X. Y ) ) ` v ) = ( x. ` v ) )
135 133 134 eqeqan12d
 |-  ( ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) -> ( ( ( x. |` ( X X. Y ) ) ` u ) = ( ( x. |` ( X X. Y ) ) ` v ) <-> ( x. ` u ) = ( x. ` v ) ) )
136 135 imbi1d
 |-  ( ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) -> ( ( ( ( x. |` ( X X. Y ) ) ` u ) = ( ( x. |` ( X X. Y ) ) ` v ) -> u = v ) <-> ( ( x. ` u ) = ( x. ` v ) -> u = v ) ) )
137 136 ralbidva
 |-  ( u e. ( X X. Y ) -> ( A. v e. ( X X. Y ) ( ( ( x. |` ( X X. Y ) ) ` u ) = ( ( x. |` ( X X. Y ) ) ` v ) -> u = v ) <-> A. v e. ( X X. Y ) ( ( x. ` u ) = ( x. ` v ) -> u = v ) ) )
138 137 ralbiia
 |-  ( A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( ( x. |` ( X X. Y ) ) ` u ) = ( ( x. |` ( X X. Y ) ) ` v ) -> u = v ) <-> A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( x. ` u ) = ( x. ` v ) -> u = v ) )
139 fveq2
 |-  ( v = <. m , n >. -> ( x. ` v ) = ( x. ` <. m , n >. ) )
140 df-ov
 |-  ( m x. n ) = ( x. ` <. m , n >. )
141 139 140 eqtr4di
 |-  ( v = <. m , n >. -> ( x. ` v ) = ( m x. n ) )
142 141 eqeq2d
 |-  ( v = <. m , n >. -> ( ( x. ` u ) = ( x. ` v ) <-> ( x. ` u ) = ( m x. n ) ) )
143 eqeq2
 |-  ( v = <. m , n >. -> ( u = v <-> u = <. m , n >. ) )
144 142 143 imbi12d
 |-  ( v = <. m , n >. -> ( ( ( x. ` u ) = ( x. ` v ) -> u = v ) <-> ( ( x. ` u ) = ( m x. n ) -> u = <. m , n >. ) ) )
145 144 ralxp
 |-  ( A. v e. ( X X. Y ) ( ( x. ` u ) = ( x. ` v ) -> u = v ) <-> A. m e. X A. n e. Y ( ( x. ` u ) = ( m x. n ) -> u = <. m , n >. ) )
146 fveq2
 |-  ( u = <. i , j >. -> ( x. ` u ) = ( x. ` <. i , j >. ) )
147 df-ov
 |-  ( i x. j ) = ( x. ` <. i , j >. )
148 146 147 eqtr4di
 |-  ( u = <. i , j >. -> ( x. ` u ) = ( i x. j ) )
149 148 eqeq1d
 |-  ( u = <. i , j >. -> ( ( x. ` u ) = ( m x. n ) <-> ( i x. j ) = ( m x. n ) ) )
150 eqeq1
 |-  ( u = <. i , j >. -> ( u = <. m , n >. <-> <. i , j >. = <. m , n >. ) )
151 149 150 imbi12d
 |-  ( u = <. i , j >. -> ( ( ( x. ` u ) = ( m x. n ) -> u = <. m , n >. ) <-> ( ( i x. j ) = ( m x. n ) -> <. i , j >. = <. m , n >. ) ) )
152 151 2ralbidv
 |-  ( u = <. i , j >. -> ( A. m e. X A. n e. Y ( ( x. ` u ) = ( m x. n ) -> u = <. m , n >. ) <-> A. m e. X A. n e. Y ( ( i x. j ) = ( m x. n ) -> <. i , j >. = <. m , n >. ) ) )
153 145 152 syl5bb
 |-  ( u = <. i , j >. -> ( A. v e. ( X X. Y ) ( ( x. ` u ) = ( x. ` v ) -> u = v ) <-> A. m e. X A. n e. Y ( ( i x. j ) = ( m x. n ) -> <. i , j >. = <. m , n >. ) ) )
154 153 ralxp
 |-  ( A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( x. ` u ) = ( x. ` v ) -> u = v ) <-> A. i e. X A. j e. Y A. m e. X A. n e. Y ( ( i x. j ) = ( m x. n ) -> <. i , j >. = <. m , n >. ) )
155 138 154 bitri
 |-  ( A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( ( x. |` ( X X. Y ) ) ` u ) = ( ( x. |` ( X X. Y ) ) ` v ) -> u = v ) <-> A. i e. X A. j e. Y A. m e. X A. n e. Y ( ( i x. j ) = ( m x. n ) -> <. i , j >. = <. m , n >. ) )
156 132 155 sylibr
 |-  ( ph -> A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( ( x. |` ( X X. Y ) ) ` u ) = ( ( x. |` ( X X. Y ) ) ` v ) -> u = v ) )
157 dff13
 |-  ( ( x. |` ( X X. Y ) ) : ( X X. Y ) -1-1-> Z <-> ( ( x. |` ( X X. Y ) ) : ( X X. Y ) --> Z /\ A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( ( x. |` ( X X. Y ) ) ` u ) = ( ( x. |` ( X X. Y ) ) ` v ) -> u = v ) ) )
158 58 156 157 sylanbrc
 |-  ( ph -> ( x. |` ( X X. Y ) ) : ( X X. Y ) -1-1-> Z )
159 breq1
 |-  ( x = w -> ( x || ( M x. N ) <-> w || ( M x. N ) ) )
160 159 6 elrab2
 |-  ( w e. Z <-> ( w e. NN /\ w || ( M x. N ) ) )
161 160 simplbi
 |-  ( w e. Z -> w e. NN )
162 161 adantl
 |-  ( ( ph /\ w e. Z ) -> w e. NN )
163 162 nnzd
 |-  ( ( ph /\ w e. Z ) -> w e. ZZ )
164 1 adantr
 |-  ( ( ph /\ w e. Z ) -> M e. NN )
165 164 nnzd
 |-  ( ( ph /\ w e. Z ) -> M e. ZZ )
166 164 nnne0d
 |-  ( ( ph /\ w e. Z ) -> M =/= 0 )
167 simpr
 |-  ( ( w = 0 /\ M = 0 ) -> M = 0 )
168 167 necon3ai
 |-  ( M =/= 0 -> -. ( w = 0 /\ M = 0 ) )
169 166 168 syl
 |-  ( ( ph /\ w e. Z ) -> -. ( w = 0 /\ M = 0 ) )
170 gcdn0cl
 |-  ( ( ( w e. ZZ /\ M e. ZZ ) /\ -. ( w = 0 /\ M = 0 ) ) -> ( w gcd M ) e. NN )
171 163 165 169 170 syl21anc
 |-  ( ( ph /\ w e. Z ) -> ( w gcd M ) e. NN )
172 gcddvds
 |-  ( ( w e. ZZ /\ M e. ZZ ) -> ( ( w gcd M ) || w /\ ( w gcd M ) || M ) )
173 163 165 172 syl2anc
 |-  ( ( ph /\ w e. Z ) -> ( ( w gcd M ) || w /\ ( w gcd M ) || M ) )
174 173 simprd
 |-  ( ( ph /\ w e. Z ) -> ( w gcd M ) || M )
175 breq1
 |-  ( x = ( w gcd M ) -> ( x || M <-> ( w gcd M ) || M ) )
176 175 4 elrab2
 |-  ( ( w gcd M ) e. X <-> ( ( w gcd M ) e. NN /\ ( w gcd M ) || M ) )
177 171 174 176 sylanbrc
 |-  ( ( ph /\ w e. Z ) -> ( w gcd M ) e. X )
178 2 adantr
 |-  ( ( ph /\ w e. Z ) -> N e. NN )
179 178 nnzd
 |-  ( ( ph /\ w e. Z ) -> N e. ZZ )
180 178 nnne0d
 |-  ( ( ph /\ w e. Z ) -> N =/= 0 )
181 simpr
 |-  ( ( w = 0 /\ N = 0 ) -> N = 0 )
182 181 necon3ai
 |-  ( N =/= 0 -> -. ( w = 0 /\ N = 0 ) )
183 180 182 syl
 |-  ( ( ph /\ w e. Z ) -> -. ( w = 0 /\ N = 0 ) )
184 gcdn0cl
 |-  ( ( ( w e. ZZ /\ N e. ZZ ) /\ -. ( w = 0 /\ N = 0 ) ) -> ( w gcd N ) e. NN )
185 163 179 183 184 syl21anc
 |-  ( ( ph /\ w e. Z ) -> ( w gcd N ) e. NN )
186 gcddvds
 |-  ( ( w e. ZZ /\ N e. ZZ ) -> ( ( w gcd N ) || w /\ ( w gcd N ) || N ) )
187 163 179 186 syl2anc
 |-  ( ( ph /\ w e. Z ) -> ( ( w gcd N ) || w /\ ( w gcd N ) || N ) )
188 187 simprd
 |-  ( ( ph /\ w e. Z ) -> ( w gcd N ) || N )
189 breq1
 |-  ( x = ( w gcd N ) -> ( x || N <-> ( w gcd N ) || N ) )
190 189 5 elrab2
 |-  ( ( w gcd N ) e. Y <-> ( ( w gcd N ) e. NN /\ ( w gcd N ) || N ) )
191 185 188 190 sylanbrc
 |-  ( ( ph /\ w e. Z ) -> ( w gcd N ) e. Y )
192 177 191 opelxpd
 |-  ( ( ph /\ w e. Z ) -> <. ( w gcd M ) , ( w gcd N ) >. e. ( X X. Y ) )
193 192 fvresd
 |-  ( ( ph /\ w e. Z ) -> ( ( x. |` ( X X. Y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) = ( x. ` <. ( w gcd M ) , ( w gcd N ) >. ) )
194 3 adantr
 |-  ( ( ph /\ w e. Z ) -> ( M gcd N ) = 1 )
195 rpmulgcd2
 |-  ( ( ( w e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( w gcd ( M x. N ) ) = ( ( w gcd M ) x. ( w gcd N ) ) )
196 163 165 179 194 195 syl31anc
 |-  ( ( ph /\ w e. Z ) -> ( w gcd ( M x. N ) ) = ( ( w gcd M ) x. ( w gcd N ) ) )
197 df-ov
 |-  ( ( w gcd M ) x. ( w gcd N ) ) = ( x. ` <. ( w gcd M ) , ( w gcd N ) >. )
198 196 197 eqtrdi
 |-  ( ( ph /\ w e. Z ) -> ( w gcd ( M x. N ) ) = ( x. ` <. ( w gcd M ) , ( w gcd N ) >. ) )
199 160 simprbi
 |-  ( w e. Z -> w || ( M x. N ) )
200 199 adantl
 |-  ( ( ph /\ w e. Z ) -> w || ( M x. N ) )
201 1 2 nnmulcld
 |-  ( ph -> ( M x. N ) e. NN )
202 gcdeq
 |-  ( ( w e. NN /\ ( M x. N ) e. NN ) -> ( ( w gcd ( M x. N ) ) = w <-> w || ( M x. N ) ) )
203 161 201 202 syl2anr
 |-  ( ( ph /\ w e. Z ) -> ( ( w gcd ( M x. N ) ) = w <-> w || ( M x. N ) ) )
204 200 203 mpbird
 |-  ( ( ph /\ w e. Z ) -> ( w gcd ( M x. N ) ) = w )
205 193 198 204 3eqtr2rd
 |-  ( ( ph /\ w e. Z ) -> w = ( ( x. |` ( X X. Y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) )
206 fveq2
 |-  ( u = <. ( w gcd M ) , ( w gcd N ) >. -> ( ( x. |` ( X X. Y ) ) ` u ) = ( ( x. |` ( X X. Y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) )
207 206 rspceeqv
 |-  ( ( <. ( w gcd M ) , ( w gcd N ) >. e. ( X X. Y ) /\ w = ( ( x. |` ( X X. Y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) ) -> E. u e. ( X X. Y ) w = ( ( x. |` ( X X. Y ) ) ` u ) )
208 192 205 207 syl2anc
 |-  ( ( ph /\ w e. Z ) -> E. u e. ( X X. Y ) w = ( ( x. |` ( X X. Y ) ) ` u ) )
209 208 ralrimiva
 |-  ( ph -> A. w e. Z E. u e. ( X X. Y ) w = ( ( x. |` ( X X. Y ) ) ` u ) )
210 dffo3
 |-  ( ( x. |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z <-> ( ( x. |` ( X X. Y ) ) : ( X X. Y ) --> Z /\ A. w e. Z E. u e. ( X X. Y ) w = ( ( x. |` ( X X. Y ) ) ` u ) ) )
211 58 209 210 sylanbrc
 |-  ( ph -> ( x. |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z )
212 df-f1o
 |-  ( ( x. |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z <-> ( ( x. |` ( X X. Y ) ) : ( X X. Y ) -1-1-> Z /\ ( x. |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z ) )
213 158 211 212 sylanbrc
 |-  ( ph -> ( x. |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z )