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 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
dvdsmulf1o.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dvdsmulf1o.3 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
dvdsmulf1o.x ⊢ 𝑋 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 }
dvdsmulf1o.y ⊢ 𝑌 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
dvdsmulf1o.z ⊢ 𝑍 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
Assertion dvdsmulf1o ( 𝜑 → ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto→ 𝑍 )

Proof

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