reprpmtf1o

Description: Transposing 0 and X maps representations with a condition on the first index to transpositions with the same condition on the index X . (Contributed by Thierry Arnoux, 27-Dec-2021)

	Ref	Expression
Hypotheses	reprpmtf1o.s	$⊢ φ \to S \in ℕ$
	reprpmtf1o.m	$⊢ φ \to M \in ℤ$
	reprpmtf1o.a	$⊢ φ \to A \subseteq ℕ$
	reprpmtf1o.x	$⊢ φ \to X \in (0 ..^S)$
	reprpmtf1o.o	$⊢ O = \{c \in (A repr (S) M) \| \neg c (0) \in B\}$
	reprpmtf1o.p	$⊢ P = \{c \in (A repr (S) M) \| \neg c (X) \in B\}$
	reprpmtf1o.t	$⊢ T = if (X = 0, {I ↾}_{(0 ..^S)}, pmTrsp ((0 ..^S)) (\{X, 0\}))$
	reprpmtf1o.f	$⊢ F = (c \in P ⟼ c \circ T)$
Assertion	reprpmtf1o	$⊢ φ \to F : P \underset{1-1 onto}{⟶} O$

Proof

Step	Hyp	Ref	Expression
1		reprpmtf1o.s	$⊢ φ \to S \in ℕ$
2		reprpmtf1o.m	$⊢ φ \to M \in ℤ$
3		reprpmtf1o.a	$⊢ φ \to A \subseteq ℕ$
4		reprpmtf1o.x	$⊢ φ \to X \in (0 ..^S)$
5		reprpmtf1o.o	$⊢ O = \{c \in (A repr (S) M) \| \neg c (0) \in B\}$
6		reprpmtf1o.p	$⊢ P = \{c \in (A repr (S) M) \| \neg c (X) \in B\}$
7		reprpmtf1o.t	$⊢ T = if (X = 0, {I ↾}_{(0 ..^S)}, pmTrsp ((0 ..^S)) (\{X, 0\}))$
8		reprpmtf1o.f	$⊢ F = (c \in P ⟼ c \circ T)$
9		eqid	$⊢ A^{(0 ..^S)} = A^{(0 ..^S)}$
10		eqid	$⊢ (c \in (A^{(0 ..^S)}) ⟼ c \circ T) = (c \in (A^{(0 ..^S)}) ⟼ c \circ T)$
11		ovexd	$⊢ φ \to (0 ..^S) \in V$
12		nnex	$⊢ ℕ \in V$
13	12	a1i	$⊢ φ \to ℕ \in V$
14	13 3	ssexd	$⊢ φ \to A \in V$
15		lbfzo0	$⊢ 0 \in (0 ..^S) \leftrightarrow S \in ℕ$
16	1 15	sylibr	$⊢ φ \to 0 \in (0 ..^S)$
17	11 4 16 7	pmtridf1o	$⊢ φ \to T : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S)$
18	9 9 10 11 11 14 17	fmptco1f1o	$⊢ φ \to (c \in (A^{(0 ..^S)}) ⟼ c \circ T) : A^{(0 ..^S)} \underset{1-1 onto}{⟶} A^{(0 ..^S)}$
19		f1of1	$⊢ (c \in (A^{(0 ..^S)}) ⟼ c \circ T) : A^{(0 ..^S)} \underset{1-1 onto}{⟶} A^{(0 ..^S)} \to (c \in (A^{(0 ..^S)}) ⟼ c \circ T) : A^{(0 ..^S)} \underset{1-1}{⟶} A^{(0 ..^S)}$
20	18 19	syl	$⊢ φ \to (c \in (A^{(0 ..^S)}) ⟼ c \circ T) : A^{(0 ..^S)} \underset{1-1}{⟶} A^{(0 ..^S)}$
21		ssrab2	$⊢ \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\} \subseteq A^{(0 ..^S)}$
22	6	ssrab3	$⊢ P \subseteq A repr (S) M$
23	22	a1i	$⊢ φ \to P \subseteq A repr (S) M$
24	1	nnnn0d	$⊢ φ \to S \in ℕ_{0}$
25	3 2 24	reprval	$⊢ φ \to A repr (S) M = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
26	23 25	sseqtrd	$⊢ φ \to P \subseteq \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
27	26	sselda	$⊢ (φ \land c \in P) \to c \in \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
28	21 27	sselid	$⊢ (φ \land c \in P) \to c \in (A^{(0 ..^S)})$
29	28	ex	$⊢ φ \to (c \in P \to c \in (A^{(0 ..^S)}))$
30	29	ssrdv	$⊢ φ \to P \subseteq A^{(0 ..^S)}$
31		f1ores	$⊢ ((c \in (A^{(0 ..^S)}) ⟼ c \circ T) : A^{(0 ..^S)} \underset{1-1}{⟶} A^{(0 ..^S)} \land P \subseteq A^{(0 ..^S)}) \to ({(c \in (A^{(0 ..^S)}) ⟼ c \circ T) ↾}_{P}) : P \underset{1-1 onto}{⟶} (c \in (A^{(0 ..^S)}) ⟼ c \circ T) [P]$
32	20 30 31	syl2anc	$⊢ φ \to ({(c \in (A^{(0 ..^S)}) ⟼ c \circ T) ↾}_{P}) : P \underset{1-1 onto}{⟶} (c \in (A^{(0 ..^S)}) ⟼ c \circ T) [P]$
33		resmpt	$⊢ P \subseteq A^{(0 ..^S)} \to {(c \in (A^{(0 ..^S)}) ⟼ c \circ T) ↾}_{P} = (c \in P ⟼ c \circ T)$
34	30 33	syl	$⊢ φ \to {(c \in (A^{(0 ..^S)}) ⟼ c \circ T) ↾}_{P} = (c \in P ⟼ c \circ T)$
35	34 8	eqtr4di	$⊢ φ \to {(c \in (A^{(0 ..^S)}) ⟼ c \circ T) ↾}_{P} = F$
36		eqidd	$⊢ φ \to P = P$
37		vex	$⊢ d \in V$
38	37	a1i	$⊢ φ \to d \in V$
39	10 38 30	elimampt	$⊢ φ \to (d \in (c \in (A^{(0 ..^S)}) ⟼ c \circ T) [P] \leftrightarrow \exists c \in P d = c \circ T)$
40		simpr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to d = c \circ T$
41		f1of	$⊢ (c \in (A^{(0 ..^S)}) ⟼ c \circ T) : A^{(0 ..^S)} \underset{1-1 onto}{⟶} A^{(0 ..^S)} \to (c \in (A^{(0 ..^S)}) ⟼ c \circ T) : A^{(0 ..^S)} ⟶ A^{(0 ..^S)}$
42	18 41	syl	$⊢ φ \to (c \in (A^{(0 ..^S)}) ⟼ c \circ T) : A^{(0 ..^S)} ⟶ A^{(0 ..^S)}$
43	42	ad2antrr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to (c \in (A^{(0 ..^S)}) ⟼ c \circ T) : A^{(0 ..^S)} ⟶ A^{(0 ..^S)}$
44	10	fmpt	$⊢ \forall c \in (A^{(0 ..^S)}) c \circ T \in (A^{(0 ..^S)}) \leftrightarrow (c \in (A^{(0 ..^S)}) ⟼ c \circ T) : A^{(0 ..^S)} ⟶ A^{(0 ..^S)}$
45	43 44	sylibr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to \forall c \in (A^{(0 ..^S)}) c \circ T \in (A^{(0 ..^S)})$
46	28	adantr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to c \in (A^{(0 ..^S)})$
47		rspa	$⊢ (\forall c \in (A^{(0 ..^S)}) c \circ T \in (A^{(0 ..^S)}) \land c \in (A^{(0 ..^S)})) \to c \circ T \in (A^{(0 ..^S)})$
48	45 46 47	syl2anc	$⊢ ((φ \land c \in P) \land d = c \circ T) \to c \circ T \in (A^{(0 ..^S)})$
49	40 48	eqeltrd	$⊢ ((φ \land c \in P) \land d = c \circ T) \to d \in (A^{(0 ..^S)})$
50	40	adantr	$⊢ (((φ \land c \in P) \land d = c \circ T) \land a \in (0 ..^S)) \to d = c \circ T$
51	50	fveq1d	$⊢ (((φ \land c \in P) \land d = c \circ T) \land a \in (0 ..^S)) \to d (a) = (c \circ T) (a)$
52		f1ofun	$⊢ T : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S) \to Fun T$
53	17 52	syl	$⊢ φ \to Fun T$
54	53	ad2antrr	$⊢ ((φ \land c \in P) \land a \in (0 ..^S)) \to Fun T$
55		simpr	$⊢ ((φ \land c \in P) \land a \in (0 ..^S)) \to a \in (0 ..^S)$
56		f1odm	$⊢ T : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S) \to dom T = (0 ..^S)$
57	17 56	syl	$⊢ φ \to dom T = (0 ..^S)$
58	57	ad2antrr	$⊢ ((φ \land c \in P) \land a \in (0 ..^S)) \to dom T = (0 ..^S)$
59	55 58	eleqtrrd	$⊢ ((φ \land c \in P) \land a \in (0 ..^S)) \to a \in dom T$
60		fvco	$⊢ (Fun T \land a \in dom T) \to (c \circ T) (a) = c (T (a))$
61	54 59 60	syl2anc	$⊢ ((φ \land c \in P) \land a \in (0 ..^S)) \to (c \circ T) (a) = c (T (a))$
62	61	adantlr	$⊢ (((φ \land c \in P) \land d = c \circ T) \land a \in (0 ..^S)) \to (c \circ T) (a) = c (T (a))$
63	51 62	eqtrd	$⊢ (((φ \land c \in P) \land d = c \circ T) \land a \in (0 ..^S)) \to d (a) = c (T (a))$
64	63	sumeq2dv	$⊢ ((φ \land c \in P) \land d = c \circ T) \to \sum_{a \in (0 ..^S)} d (a) = \sum_{a \in (0 ..^S)} c (T (a))$
65		fveq2	$⊢ b = T (a) \to c (b) = c (T (a))$
66		fzofi	$⊢ (0 ..^S) \in Fin$
67	66	a1i	$⊢ (φ \land c \in P) \to (0 ..^S) \in Fin$
68	17	adantr	$⊢ (φ \land c \in P) \to T : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S)$
69		eqidd	$⊢ ((φ \land c \in P) \land a \in (0 ..^S)) \to T (a) = T (a)$
70	3	ad2antrr	$⊢ ((φ \land c \in P) \land b \in (0 ..^S)) \to A \subseteq ℕ$
71	3	adantr	$⊢ (φ \land c \in P) \to A \subseteq ℕ$
72	2	adantr	$⊢ (φ \land c \in P) \to M \in ℤ$
73	24	adantr	$⊢ (φ \land c \in P) \to S \in ℕ_{0}$
74	23	sselda	$⊢ (φ \land c \in P) \to c \in (A repr (S) M)$
75	71 72 73 74	reprf	$⊢ (φ \land c \in P) \to c : (0 ..^S) ⟶ A$
76	75	ffvelcdmda	$⊢ ((φ \land c \in P) \land b \in (0 ..^S)) \to c (b) \in A$
77	70 76	sseldd	$⊢ ((φ \land c \in P) \land b \in (0 ..^S)) \to c (b) \in ℕ$
78	77	nncnd	$⊢ ((φ \land c \in P) \land b \in (0 ..^S)) \to c (b) \in ℂ$
79	65 67 68 69 78	fsumf1o	$⊢ (φ \land c \in P) \to \sum_{b \in (0 ..^S)} c (b) = \sum_{a \in (0 ..^S)} c (T (a))$
80	79	adantr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to \sum_{b \in (0 ..^S)} c (b) = \sum_{a \in (0 ..^S)} c (T (a))$
81	71 72 73 74	reprsum	$⊢ (φ \land c \in P) \to \sum_{b \in (0 ..^S)} c (b) = M$
82	81	adantr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to \sum_{b \in (0 ..^S)} c (b) = M$
83	64 80 82	3eqtr2d	$⊢ ((φ \land c \in P) \land d = c \circ T) \to \sum_{a \in (0 ..^S)} d (a) = M$
84		fveq1	$⊢ c = d \to c (a) = d (a)$
85	84	sumeq2sdv	$⊢ c = d \to \sum_{a \in (0 ..^S)} c (a) = \sum_{a \in (0 ..^S)} d (a)$
86	85	eqeq1d	$⊢ c = d \to (\sum_{a \in (0 ..^S)} c (a) = M \leftrightarrow \sum_{a \in (0 ..^S)} d (a) = M)$
87	86	elrab	$⊢ d \in \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\} \leftrightarrow (d \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} d (a) = M)$
88	49 83 87	sylanbrc	$⊢ ((φ \land c \in P) \land d = c \circ T) \to d \in \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
89	25	ad2antrr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to A repr (S) M = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
90	88 89	eleqtrrd	$⊢ ((φ \land c \in P) \land d = c \circ T) \to d \in (A repr (S) M)$
91	40	fveq1d	$⊢ ((φ \land c \in P) \land d = c \circ T) \to d (0) = (c \circ T) (0)$
92	53	ad2antrr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to Fun T$
93	16 57	eleqtrrd	$⊢ φ \to 0 \in dom T$
94	93	ad2antrr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to 0 \in dom T$
95		fvco	$⊢ (Fun T \land 0 \in dom T) \to (c \circ T) (0) = c (T (0))$
96	92 94 95	syl2anc	$⊢ ((φ \land c \in P) \land d = c \circ T) \to (c \circ T) (0) = c (T (0))$
97	11 4 16 7	pmtridfv2	$⊢ φ \to T (0) = X$
98	97	ad2antrr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to T (0) = X$
99	98	fveq2d	$⊢ ((φ \land c \in P) \land d = c \circ T) \to c (T (0)) = c (X)$
100		simpr	$⊢ (φ \land c \in P) \to c \in P$
101	100 6	eleqtrdi	$⊢ (φ \land c \in P) \to c \in \{c \in (A repr (S) M) \| \neg c (X) \in B\}$
102		rabid	$⊢ c \in \{c \in (A repr (S) M) \| \neg c (X) \in B\} \leftrightarrow (c \in (A repr (S) M) \land \neg c (X) \in B)$
103	101 102	sylib	$⊢ (φ \land c \in P) \to (c \in (A repr (S) M) \land \neg c (X) \in B)$
104	103	simprd	$⊢ (φ \land c \in P) \to \neg c (X) \in B$
105	104	adantr	$⊢ ((φ \land c \in P) \land d = c \circ T) \to \neg c (X) \in B$
106	99 105	eqneltrd	$⊢ ((φ \land c \in P) \land d = c \circ T) \to \neg c (T (0)) \in B$
107	96 106	eqneltrd	$⊢ ((φ \land c \in P) \land d = c \circ T) \to \neg (c \circ T) (0) \in B$
108	91 107	eqneltrd	$⊢ ((φ \land c \in P) \land d = c \circ T) \to \neg d (0) \in B$
109	90 108	jca	$⊢ ((φ \land c \in P) \land d = c \circ T) \to (d \in (A repr (S) M) \land \neg d (0) \in B)$
110	109	r19.29an	$⊢ (φ \land \exists c \in P d = c \circ T) \to (d \in (A repr (S) M) \land \neg d (0) \in B)$
111	3	adantr	$⊢ (φ \land d \in (A repr (S) M)) \to A \subseteq ℕ$
112	2	adantr	$⊢ (φ \land d \in (A repr (S) M)) \to M \in ℤ$
113	24	adantr	$⊢ (φ \land d \in (A repr (S) M)) \to S \in ℕ_{0}$
114		simpr	$⊢ (φ \land d \in (A repr (S) M)) \to d \in (A repr (S) M)$
115	111 112 113 114	reprf	$⊢ (φ \land d \in (A repr (S) M)) \to d : (0 ..^S) ⟶ A$
116		f1ocnv	$⊢ T : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S) \to T^{-1} : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S)$
117		f1of	$⊢ T^{-1} : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S) \to T^{-1} : (0 ..^S) ⟶ (0 ..^S)$
118	17 116 117	3syl	$⊢ φ \to T^{-1} : (0 ..^S) ⟶ (0 ..^S)$
119	118	adantr	$⊢ (φ \land d \in (A repr (S) M)) \to T^{-1} : (0 ..^S) ⟶ (0 ..^S)$
120		fco	$⊢ (d : (0 ..^S) ⟶ A \land T^{-1} : (0 ..^S) ⟶ (0 ..^S)) \to (d \circ T^{-1}) : (0 ..^S) ⟶ A$
121	115 119 120	syl2anc	$⊢ (φ \land d \in (A repr (S) M)) \to (d \circ T^{-1}) : (0 ..^S) ⟶ A$
122		elmapg	$⊢ (A \in V \land (0 ..^S) \in V) \to (d \circ T^{-1} \in (A^{(0 ..^S)}) \leftrightarrow (d \circ T^{-1}) : (0 ..^S) ⟶ A)$
123	14 11 122	syl2anc	$⊢ φ \to (d \circ T^{-1} \in (A^{(0 ..^S)}) \leftrightarrow (d \circ T^{-1}) : (0 ..^S) ⟶ A)$
124	123	adantr	$⊢ (φ \land d \in (A repr (S) M)) \to (d \circ T^{-1} \in (A^{(0 ..^S)}) \leftrightarrow (d \circ T^{-1}) : (0 ..^S) ⟶ A)$
125	121 124	mpbird	$⊢ (φ \land d \in (A repr (S) M)) \to d \circ T^{-1} \in (A^{(0 ..^S)})$
126	125	adantr	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to d \circ T^{-1} \in (A^{(0 ..^S)})$
127		f1ofun	$⊢ T^{-1} : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S) \to Fun T^{-1}$
128	17 116 127	3syl	$⊢ φ \to Fun T^{-1}$
129	128	ad2antrr	$⊢ ((φ \land d \in (A repr (S) M)) \land a \in (0 ..^S)) \to Fun T^{-1}$
130		simpr	$⊢ (φ \land a \in (0 ..^S)) \to a \in (0 ..^S)$
131		f1odm	$⊢ T^{-1} : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S) \to dom T^{-1} = (0 ..^S)$
132	17 116 131	3syl	$⊢ φ \to dom T^{-1} = (0 ..^S)$
133	132	adantr	$⊢ (φ \land a \in (0 ..^S)) \to dom T^{-1} = (0 ..^S)$
134	130 133	eleqtrrd	$⊢ (φ \land a \in (0 ..^S)) \to a \in dom T^{-1}$
135	134	adantlr	$⊢ ((φ \land d \in (A repr (S) M)) \land a \in (0 ..^S)) \to a \in dom T^{-1}$
136		fvco	$⊢ (Fun T^{-1} \land a \in dom T^{-1}) \to (d \circ T^{-1}) (a) = d (T^{-1} (a))$
137	129 135 136	syl2anc	$⊢ ((φ \land d \in (A repr (S) M)) \land a \in (0 ..^S)) \to (d \circ T^{-1}) (a) = d (T^{-1} (a))$
138	137	sumeq2dv	$⊢ (φ \land d \in (A repr (S) M)) \to \sum_{a \in (0 ..^S)} (d \circ T^{-1}) (a) = \sum_{a \in (0 ..^S)} d (T^{-1} (a))$
139		fveq2	$⊢ b = T^{-1} (a) \to d (b) = d (T^{-1} (a))$
140	66	a1i	$⊢ (φ \land d \in (A repr (S) M)) \to (0 ..^S) \in Fin$
141	17 116	syl	$⊢ φ \to T^{-1} : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S)$
142	141	adantr	$⊢ (φ \land d \in (A repr (S) M)) \to T^{-1} : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S)$
143		eqidd	$⊢ ((φ \land d \in (A repr (S) M)) \land a \in (0 ..^S)) \to T^{-1} (a) = T^{-1} (a)$
144	111	adantr	$⊢ ((φ \land d \in (A repr (S) M)) \land b \in (0 ..^S)) \to A \subseteq ℕ$
145	115	ffvelcdmda	$⊢ ((φ \land d \in (A repr (S) M)) \land b \in (0 ..^S)) \to d (b) \in A$
146	144 145	sseldd	$⊢ ((φ \land d \in (A repr (S) M)) \land b \in (0 ..^S)) \to d (b) \in ℕ$
147	146	nncnd	$⊢ ((φ \land d \in (A repr (S) M)) \land b \in (0 ..^S)) \to d (b) \in ℂ$
148	139 140 142 143 147	fsumf1o	$⊢ (φ \land d \in (A repr (S) M)) \to \sum_{b \in (0 ..^S)} d (b) = \sum_{a \in (0 ..^S)} d (T^{-1} (a))$
149	111 112 113 114	reprsum	$⊢ (φ \land d \in (A repr (S) M)) \to \sum_{b \in (0 ..^S)} d (b) = M$
150	138 148 149	3eqtr2d	$⊢ (φ \land d \in (A repr (S) M)) \to \sum_{a \in (0 ..^S)} (d \circ T^{-1}) (a) = M$
151	150	adantr	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to \sum_{a \in (0 ..^S)} (d \circ T^{-1}) (a) = M$
152		fveq1	$⊢ c = d \circ T^{-1} \to c (a) = (d \circ T^{-1}) (a)$
153	152	sumeq2sdv	$⊢ c = d \circ T^{-1} \to \sum_{a \in (0 ..^S)} c (a) = \sum_{a \in (0 ..^S)} (d \circ T^{-1}) (a)$
154	153	eqeq1d	$⊢ c = d \circ T^{-1} \to (\sum_{a \in (0 ..^S)} c (a) = M \leftrightarrow \sum_{a \in (0 ..^S)} (d \circ T^{-1}) (a) = M)$
155	154	elrab	$⊢ d \circ T^{-1} \in \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\} \leftrightarrow (d \circ T^{-1} \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} (d \circ T^{-1}) (a) = M)$
156	126 151 155	sylanbrc	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to d \circ T^{-1} \in \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
157	25	ad2antrr	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to A repr (S) M = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
158	156 157	eleqtrrd	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to d \circ T^{-1} \in (A repr (S) M)$
159	128	ad2antrr	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to Fun T^{-1}$
160	4 132	eleqtrrd	$⊢ φ \to X \in dom T^{-1}$
161	160	ad2antrr	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to X \in dom T^{-1}$
162		fvco	$⊢ (Fun T^{-1} \land X \in dom T^{-1}) \to (d \circ T^{-1}) (X) = d (T^{-1} (X))$
163	159 161 162	syl2anc	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to (d \circ T^{-1}) (X) = d (T^{-1} (X))$
164		f1ocnvfv	$⊢ (T : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S) \land 0 \in (0 ..^S)) \to (T (0) = X \to T^{-1} (X) = 0)$
165	164	imp	$⊢ ((T : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S) \land 0 \in (0 ..^S)) \land T (0) = X) \to T^{-1} (X) = 0$
166	17 16 97 165	syl21anc	$⊢ φ \to T^{-1} (X) = 0$
167	166	ad2antrr	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to T^{-1} (X) = 0$
168	167	fveq2d	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to d (T^{-1} (X)) = d (0)$
169		simpr	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to \neg d (0) \in B$
170	168 169	eqneltrd	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to \neg d (T^{-1} (X)) \in B$
171	163 170	eqneltrd	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to \neg (d \circ T^{-1}) (X) \in B$
172		fveq1	$⊢ c = d \circ T^{-1} \to c (X) = (d \circ T^{-1}) (X)$
173	172	eleq1d	$⊢ c = d \circ T^{-1} \to (c (X) \in B \leftrightarrow (d \circ T^{-1}) (X) \in B)$
174	173	notbid	$⊢ c = d \circ T^{-1} \to (\neg c (X) \in B \leftrightarrow \neg (d \circ T^{-1}) (X) \in B)$
175	174	elrab	$⊢ d \circ T^{-1} \in \{c \in (A repr (S) M) \| \neg c (X) \in B\} \leftrightarrow (d \circ T^{-1} \in (A repr (S) M) \land \neg (d \circ T^{-1}) (X) \in B)$
176	158 171 175	sylanbrc	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to d \circ T^{-1} \in \{c \in (A repr (S) M) \| \neg c (X) \in B\}$
177	176 6	eleqtrrdi	$⊢ ((φ \land d \in (A repr (S) M)) \land \neg d (0) \in B) \to d \circ T^{-1} \in P$
178	177	anasss	$⊢ (φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \to d \circ T^{-1} \in P$
179		simpr	$⊢ ((φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \land c = d \circ T^{-1}) \to c = d \circ T^{-1}$
180	179	coeq1d	$⊢ ((φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \land c = d \circ T^{-1}) \to c \circ T = (d \circ T^{-1}) \circ T$
181	180	eqeq2d	$⊢ ((φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \land c = d \circ T^{-1}) \to (d = c \circ T \leftrightarrow d = (d \circ T^{-1}) \circ T)$
182		f1ococnv1	$⊢ T : (0 ..^S) \underset{1-1 onto}{⟶} (0 ..^S) \to T^{-1} \circ T = {I ↾}_{(0 ..^S)}$
183	17 182	syl	$⊢ φ \to T^{-1} \circ T = {I ↾}_{(0 ..^S)}$
184	183	adantr	$⊢ (φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \to T^{-1} \circ T = {I ↾}_{(0 ..^S)}$
185	184	coeq2d	$⊢ (φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \to d \circ (T^{-1} \circ T) = d \circ ({I ↾}_{(0 ..^S)})$
186	115	adantrr	$⊢ (φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \to d : (0 ..^S) ⟶ A$
187		fcoi1	$⊢ d : (0 ..^S) ⟶ A \to d \circ ({I ↾}_{(0 ..^S)}) = d$
188	186 187	syl	$⊢ (φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \to d \circ ({I ↾}_{(0 ..^S)}) = d$
189	185 188	eqtr2d	$⊢ (φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \to d = d \circ (T^{-1} \circ T)$
190		coass	$⊢ (d \circ T^{-1}) \circ T = d \circ (T^{-1} \circ T)$
191	189 190	eqtr4di	$⊢ (φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \to d = (d \circ T^{-1}) \circ T$
192	178 181 191	rspcedvd	$⊢ (φ \land (d \in (A repr (S) M) \land \neg d (0) \in B)) \to \exists c \in P d = c \circ T$
193	110 192	impbida	$⊢ φ \to (\exists c \in P d = c \circ T \leftrightarrow (d \in (A repr (S) M) \land \neg d (0) \in B))$
194	39 193	bitrd	$⊢ φ \to (d \in (c \in (A^{(0 ..^S)}) ⟼ c \circ T) [P] \leftrightarrow (d \in (A repr (S) M) \land \neg d (0) \in B))$
195		fveq1	$⊢ c = d \to c (0) = d (0)$
196	195	eleq1d	$⊢ c = d \to (c (0) \in B \leftrightarrow d (0) \in B)$
197	196	notbid	$⊢ c = d \to (\neg c (0) \in B \leftrightarrow \neg d (0) \in B)$
198	197	elrab	$⊢ d \in \{c \in (A repr (S) M) \| \neg c (0) \in B\} \leftrightarrow (d \in (A repr (S) M) \land \neg d (0) \in B)$
199	194 198	bitr4di	$⊢ φ \to (d \in (c \in (A^{(0 ..^S)}) ⟼ c \circ T) [P] \leftrightarrow d \in \{c \in (A repr (S) M) \| \neg c (0) \in B\})$
200	199	eqrdv	$⊢ φ \to (c \in (A^{(0 ..^S)}) ⟼ c \circ T) [P] = \{c \in (A repr (S) M) \| \neg c (0) \in B\}$
201	200 5	eqtr4di	$⊢ φ \to (c \in (A^{(0 ..^S)}) ⟼ c \circ T) [P] = O$
202	35 36 201	f1oeq123d	$⊢ φ \to (({(c \in (A^{(0 ..^S)}) ⟼ c \circ T) ↾}_{P}) : P \underset{1-1 onto}{⟶} (c \in (A^{(0 ..^S)}) ⟼ c \circ T) [P] \leftrightarrow F : P \underset{1-1 onto}{⟶} O)$
203	32 202	mpbid	$⊢ φ \to F : P \underset{1-1 onto}{⟶} O$

Metamath Proof Explorer

Theorem reprpmtf1o

Proof