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

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 bitrid 
 |-  ( 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 )