mpodvdsmulf1o

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 . Version of dvdsmulf1o using maps-to notation, which does not require ax-mulf . (Contributed by GG, 18-Apr-2025)

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

Proof

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

Metamath Proof Explorer

Theorem mpodvdsmulf1o

Proof