diophrw

Description: Renaming and adding unused witness variables does not change the Diophantine set coded by a polynomial. (Contributed by Stefan O'Rear, 7-Oct-2014)

		Ref	Expression
	Assertion	diophrw	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to \{a \| \exists b \in ({ℕ_{0}}^{S}) (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)\} = \{a \| \exists c \in ({ℕ_{0}}^{T}) (a = {c ↾}_{O} \land P (c) = 0)\}$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \to b \in ({ℕ_{0}}^{S})$
2		nn0ex	$⊢ ℕ_{0} \in V$
3		simp1	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to S \in V$
4	3	adantr	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \to S \in V$
5		elmapg	$⊢ (ℕ_{0} \in V \land S \in V) \to (b \in ({ℕ_{0}}^{S}) \leftrightarrow b : S ⟶ ℕ_{0})$
6	2 4 5	sylancr	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \to (b \in ({ℕ_{0}}^{S}) \leftrightarrow b : S ⟶ ℕ_{0})$
7	1 6	mpbid	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \to b : S ⟶ ℕ_{0}$
8	7	adantr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to b : S ⟶ ℕ_{0}$
9		simp2	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to M : T \underset{1-1}{⟶} S$
10		f1f	$⊢ M : T \underset{1-1}{⟶} S \to M : T ⟶ S$
11	9 10	syl	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to M : T ⟶ S$
12	11	ad2antrr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to M : T ⟶ S$
13		fco	$⊢ (b : S ⟶ ℕ_{0} \land M : T ⟶ S) \to (b \circ M) : T ⟶ ℕ_{0}$
14	8 12 13	syl2anc	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to (b \circ M) : T ⟶ ℕ_{0}$
15		f1dmex	$⊢ (M : T \underset{1-1}{⟶} S \land S \in V) \to T \in V$
16	9 3 15	syl2anc	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to T \in V$
17	16	ad2antrr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to T \in V$
18		elmapg	$⊢ (ℕ_{0} \in V \land T \in V) \to (b \circ M \in ({ℕ_{0}}^{T}) \leftrightarrow (b \circ M) : T ⟶ ℕ_{0})$
19	2 17 18	sylancr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to (b \circ M \in ({ℕ_{0}}^{T}) \leftrightarrow (b \circ M) : T ⟶ ℕ_{0})$
20	14 19	mpbird	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to b \circ M \in ({ℕ_{0}}^{T})$
21		simprl	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to a = {b ↾}_{O}$
22		resco	$⊢ {(b \circ M) ↾}_{O} = b \circ ({M ↾}_{O})$
23		simpll3	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to {M ↾}_{O} = {I ↾}_{O}$
24	23	coeq2d	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to b \circ ({M ↾}_{O}) = b \circ ({I ↾}_{O})$
25		coires1	$⊢ b \circ ({I ↾}_{O}) = {b ↾}_{O}$
26	24 25	eqtrdi	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to b \circ ({M ↾}_{O}) = {b ↾}_{O}$
27	22 26	syl5eq	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to {(b \circ M) ↾}_{O} = {b ↾}_{O}$
28	21 27	eqtr4d	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to a = {(b \circ M) ↾}_{O}$
29		simpll1	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to S \in V$
30		oveq2	$⊢ a = S \to {ℕ_{0}}^{a} = {ℕ_{0}}^{S}$
31		oveq2	$⊢ a = S \to ℤ^{a} = ℤ^{S}$
32	30 31	sseq12d	$⊢ a = S \to ({ℕ_{0}}^{a} \subseteq ℤ^{a} \leftrightarrow {ℕ_{0}}^{S} \subseteq ℤ^{S})$
33		zex	$⊢ ℤ \in V$
34		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
35		mapss	$⊢ (ℤ \in V \land ℕ_{0} \subseteq ℤ) \to {ℕ_{0}}^{a} \subseteq ℤ^{a}$
36	33 34 35	mp2an	$⊢ {ℕ_{0}}^{a} \subseteq ℤ^{a}$
37	32 36	vtoclg	$⊢ S \in V \to {ℕ_{0}}^{S} \subseteq ℤ^{S}$
38	29 37	syl	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to {ℕ_{0}}^{S} \subseteq ℤ^{S}$
39		simplr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to b \in ({ℕ_{0}}^{S})$
40	38 39	sseldd	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to b \in (ℤ^{S})$
41		coeq1	$⊢ d = b \to d \circ M = b \circ M$
42	41	fveq2d	$⊢ d = b \to P (d \circ M) = P (b \circ M)$
43		eqid	$⊢ (d \in (ℤ^{S}) ⟼ P (d \circ M)) = (d \in (ℤ^{S}) ⟼ P (d \circ M))$
44		fvex	$⊢ P (b \circ M) \in V$
45	42 43 44	fvmpt	$⊢ b \in (ℤ^{S}) \to (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = P (b \circ M)$
46	40 45	syl	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = P (b \circ M)$
47		simprr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0$
48	46 47	eqtr3d	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to P (b \circ M) = 0$
49		reseq1	$⊢ c = b \circ M \to {c ↾}_{O} = {(b \circ M) ↾}_{O}$
50	49	eqeq2d	$⊢ c = b \circ M \to (a = {c ↾}_{O} \leftrightarrow a = {(b \circ M) ↾}_{O})$
51		fveqeq2	$⊢ c = b \circ M \to (P (c) = 0 \leftrightarrow P (b \circ M) = 0)$
52	50 51	anbi12d	$⊢ c = b \circ M \to ((a = {c ↾}_{O} \land P (c) = 0) \leftrightarrow (a = {(b \circ M) ↾}_{O} \land P (b \circ M) = 0))$
53	52	rspcev	$⊢ (b \circ M \in ({ℕ_{0}}^{T}) \land (a = {(b \circ M) ↾}_{O} \land P (b \circ M) = 0)) \to \exists c \in ({ℕ_{0}}^{T}) (a = {c ↾}_{O} \land P (c) = 0)$
54	20 28 48 53	syl12anc	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land b \in ({ℕ_{0}}^{S})) \land (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)) \to \exists c \in ({ℕ_{0}}^{T}) (a = {c ↾}_{O} \land P (c) = 0)$
55	54	rexlimdva2	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to (\exists b \in ({ℕ_{0}}^{S}) (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0) \to \exists c \in ({ℕ_{0}}^{T}) (a = {c ↾}_{O} \land P (c) = 0))$
56		simpr	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to c \in ({ℕ_{0}}^{T})$
57	16	adantr	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to T \in V$
58		elmapg	$⊢ (ℕ_{0} \in V \land T \in V) \to (c \in ({ℕ_{0}}^{T}) \leftrightarrow c : T ⟶ ℕ_{0})$
59	2 57 58	sylancr	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to (c \in ({ℕ_{0}}^{T}) \leftrightarrow c : T ⟶ ℕ_{0})$
60	56 59	mpbid	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to c : T ⟶ ℕ_{0}$
61	60	adantr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to c : T ⟶ ℕ_{0}$
62	9	ad2antrr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to M : T \underset{1-1}{⟶} S$
63		f1cnv	$⊢ M : T \underset{1-1}{⟶} S \to M^{-1} : ran M \underset{1-1 onto}{⟶} T$
64		f1of	$⊢ M^{-1} : ran M \underset{1-1 onto}{⟶} T \to M^{-1} : ran M ⟶ T$
65	62 63 64	3syl	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to M^{-1} : ran M ⟶ T$
66		fco	$⊢ (c : T ⟶ ℕ_{0} \land M^{-1} : ran M ⟶ T) \to (c \circ M^{-1}) : ran M ⟶ ℕ_{0}$
67	61 65 66	syl2anc	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to (c \circ M^{-1}) : ran M ⟶ ℕ_{0}$
68		c0ex	$⊢ 0 \in V$
69	68	fconst	$⊢ ((S ∖ ran M) \times \{0\}) : S ∖ ran M ⟶ \{0\}$
70	69	a1i	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((S ∖ ran M) \times \{0\}) : S ∖ ran M ⟶ \{0\}$
71		disjdif	$⊢ ran M \cap (S ∖ ran M) = \emptyset$
72	71	a1i	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ran M \cap (S ∖ ran M) = \emptyset$
73		fun	$⊢ (((c \circ M^{-1}) : ran M ⟶ ℕ_{0} \land ((S ∖ ran M) \times \{0\}) : S ∖ ran M ⟶ \{0\}) \land ran M \cap (S ∖ ran M) = \emptyset) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : ran M \cup (S ∖ ran M) ⟶ ℕ_{0} \cup \{0\}$
74	67 70 72 73	syl21anc	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : ran M \cup (S ∖ ran M) ⟶ ℕ_{0} \cup \{0\}$
75		frn	$⊢ M : T ⟶ S \to ran M \subseteq S$
76	9 10 75	3syl	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to ran M \subseteq S$
77	76	ad2antrr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ran M \subseteq S$
78		undif	$⊢ ran M \subseteq S \leftrightarrow ran M \cup (S ∖ ran M) = S$
79	77 78	sylib	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ran M \cup (S ∖ ran M) = S$
80		0nn0	$⊢ 0 \in ℕ_{0}$
81		snssi	$⊢ 0 \in ℕ_{0} \to \{0\} \subseteq ℕ_{0}$
82	80 81	ax-mp	$⊢ \{0\} \subseteq ℕ_{0}$
83		ssequn2	$⊢ \{0\} \subseteq ℕ_{0} \leftrightarrow ℕ_{0} \cup \{0\} = ℕ_{0}$
84	82 83	mpbi	$⊢ ℕ_{0} \cup \{0\} = ℕ_{0}$
85	84	a1i	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ℕ_{0} \cup \{0\} = ℕ_{0}$
86	79 85	feq23d	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to (((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : ran M \cup (S ∖ ran M) ⟶ ℕ_{0} \cup \{0\} \leftrightarrow ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : S ⟶ ℕ_{0})$
87	74 86	mpbid	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : S ⟶ ℕ_{0}$
88		elmapg	$⊢ (ℕ_{0} \in V \land S \in V) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \in ({ℕ_{0}}^{S}) \leftrightarrow ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : S ⟶ ℕ_{0})$
89	2 3 88	sylancr	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \in ({ℕ_{0}}^{S}) \leftrightarrow ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : S ⟶ ℕ_{0})$
90	89	ad2antrr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \in ({ℕ_{0}}^{S}) \leftrightarrow ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : S ⟶ ℕ_{0})$
91	87 90	mpbird	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to (c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \in ({ℕ_{0}}^{S})$
92		simprl	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to a = {c ↾}_{O}$
93		resundir	$⊢ {((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) ↾}_{O} = ({(c \circ M^{-1}) ↾}_{O}) \cup ({((S ∖ ran M) \times \{0\}) ↾}_{O})$
94		resco	$⊢ {(c \circ M^{-1}) ↾}_{O} = c \circ ({M^{-1} ↾}_{O})$
95		simpl2	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to M : T \underset{1-1}{⟶} S$
96		df-f1	$⊢ M : T \underset{1-1}{⟶} S \leftrightarrow (M : T ⟶ S \land Fun M^{-1})$
97	96	simprbi	$⊢ M : T \underset{1-1}{⟶} S \to Fun M^{-1}$
98		funcnvres	$⊢ Fun M^{-1} \to {({M ↾}_{O})}^{-1} = {M^{-1} ↾}_{M [O]}$
99	95 97 98	3syl	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to {({M ↾}_{O})}^{-1} = {M^{-1} ↾}_{M [O]}$
100		simpl3	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to {M ↾}_{O} = {I ↾}_{O}$
101	100	cnveqd	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to {({M ↾}_{O})}^{-1} = {({I ↾}_{O})}^{-1}$
102		df-ima	$⊢ M [O] = ran ({M ↾}_{O})$
103	100	rneqd	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to ran ({M ↾}_{O}) = ran ({I ↾}_{O})$
104		rnresi	$⊢ ran ({I ↾}_{O}) = O$
105	103 104	eqtrdi	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to ran ({M ↾}_{O}) = O$
106	102 105	syl5eq	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to M [O] = O$
107	106	reseq2d	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to {M^{-1} ↾}_{M [O]} = {M^{-1} ↾}_{O}$
108	99 101 107	3eqtr3d	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to {({I ↾}_{O})}^{-1} = {M^{-1} ↾}_{O}$
109		cnvresid	$⊢ {({I ↾}_{O})}^{-1} = {I ↾}_{O}$
110	108 109	eqtr3di	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to {M^{-1} ↾}_{O} = {I ↾}_{O}$
111	110	coeq2d	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to c \circ ({M^{-1} ↾}_{O}) = c \circ ({I ↾}_{O})$
112		coires1	$⊢ c \circ ({I ↾}_{O}) = {c ↾}_{O}$
113	111 112	eqtrdi	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to c \circ ({M^{-1} ↾}_{O}) = {c ↾}_{O}$
114	94 113	syl5eq	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to {(c \circ M^{-1}) ↾}_{O} = {c ↾}_{O}$
115		dmres	$⊢ dom ({((S ∖ ran M) \times \{0\}) ↾}_{O}) = O \cap dom ((S ∖ ran M) \times \{0\})$
116	68	snnz	$⊢ \{0\} \neq \emptyset$
117		dmxp	$⊢ \{0\} \neq \emptyset \to dom ((S ∖ ran M) \times \{0\}) = S ∖ ran M$
118	116 117	ax-mp	$⊢ dom ((S ∖ ran M) \times \{0\}) = S ∖ ran M$
119	118	ineq2i	$⊢ O \cap dom ((S ∖ ran M) \times \{0\}) = O \cap (S ∖ ran M)$
120		inss1	$⊢ O \cap S \subseteq O$
121	103 104	eqtr2di	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to O = ran ({M ↾}_{O})$
122		resss	$⊢ {M ↾}_{O} \subseteq M$
123		rnss	$⊢ {M ↾}_{O} \subseteq M \to ran ({M ↾}_{O}) \subseteq ran M$
124	122 123	mp1i	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to ran ({M ↾}_{O}) \subseteq ran M$
125	121 124	eqsstrd	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to O \subseteq ran M$
126	120 125	sstrid	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to O \cap S \subseteq ran M$
127		inssdif0	$⊢ O \cap S \subseteq ran M \leftrightarrow O \cap (S ∖ ran M) = \emptyset$
128	126 127	sylib	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to O \cap (S ∖ ran M) = \emptyset$
129	119 128	syl5eq	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to O \cap dom ((S ∖ ran M) \times \{0\}) = \emptyset$
130	115 129	syl5eq	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to dom ({((S ∖ ran M) \times \{0\}) ↾}_{O}) = \emptyset$
131		relres	$⊢ Rel ({((S ∖ ran M) \times \{0\}) ↾}_{O})$
132		reldm0	$⊢ Rel ({((S ∖ ran M) \times \{0\}) ↾}_{O}) \to ({((S ∖ ran M) \times \{0\}) ↾}_{O} = \emptyset \leftrightarrow dom ({((S ∖ ran M) \times \{0\}) ↾}_{O}) = \emptyset)$
133	131 132	ax-mp	$⊢ {((S ∖ ran M) \times \{0\}) ↾}_{O} = \emptyset \leftrightarrow dom ({((S ∖ ran M) \times \{0\}) ↾}_{O}) = \emptyset$
134	130 133	sylibr	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to {((S ∖ ran M) \times \{0\}) ↾}_{O} = \emptyset$
135	114 134	uneq12d	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to ({(c \circ M^{-1}) ↾}_{O}) \cup ({((S ∖ ran M) \times \{0\}) ↾}_{O}) = ({c ↾}_{O}) \cup \emptyset$
136	93 135	syl5eq	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to {((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) ↾}_{O} = ({c ↾}_{O}) \cup \emptyset$
137		un0	$⊢ ({c ↾}_{O}) \cup \emptyset = {c ↾}_{O}$
138	136 137	eqtr2di	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to {c ↾}_{O} = {((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) ↾}_{O}$
139	138	adantr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to {c ↾}_{O} = {((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) ↾}_{O}$
140	92 139	eqtrd	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to a = {((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) ↾}_{O}$
141		fss	$⊢ (c : T ⟶ ℕ_{0} \land ℕ_{0} \subseteq ℤ) \to c : T ⟶ ℤ$
142	60 34 141	sylancl	$⊢ ((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \to c : T ⟶ ℤ$
143	142	adantr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to c : T ⟶ ℤ$
144		fco	$⊢ (c : T ⟶ ℤ \land M^{-1} : ran M ⟶ T) \to (c \circ M^{-1}) : ran M ⟶ ℤ$
145	143 65 144	syl2anc	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to (c \circ M^{-1}) : ran M ⟶ ℤ$
146		fun	$⊢ (((c \circ M^{-1}) : ran M ⟶ ℤ \land ((S ∖ ran M) \times \{0\}) : S ∖ ran M ⟶ \{0\}) \land ran M \cap (S ∖ ran M) = \emptyset) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : ran M \cup (S ∖ ran M) ⟶ ℤ \cup \{0\}$
147	145 70 72 146	syl21anc	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : ran M \cup (S ∖ ran M) ⟶ ℤ \cup \{0\}$
148		0z	$⊢ 0 \in ℤ$
149		snssi	$⊢ 0 \in ℤ \to \{0\} \subseteq ℤ$
150	148 149	ax-mp	$⊢ \{0\} \subseteq ℤ$
151		ssequn2	$⊢ \{0\} \subseteq ℤ \leftrightarrow ℤ \cup \{0\} = ℤ$
152	150 151	mpbi	$⊢ ℤ \cup \{0\} = ℤ$
153	152	a1i	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ℤ \cup \{0\} = ℤ$
154	79 153	feq23d	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to (((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : ran M \cup (S ∖ ran M) ⟶ ℤ \cup \{0\} \leftrightarrow ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : S ⟶ ℤ)$
155	147 154	mpbid	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : S ⟶ ℤ$
156		elmapg	$⊢ (ℤ \in V \land S \in V) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \in (ℤ^{S}) \leftrightarrow ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : S ⟶ ℤ)$
157	33 3 156	sylancr	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \in (ℤ^{S}) \leftrightarrow ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : S ⟶ ℤ)$
158	157	ad2antrr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \in (ℤ^{S}) \leftrightarrow ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) : S ⟶ ℤ)$
159	155 158	mpbird	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to (c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \in (ℤ^{S})$
160		coeq1	$⊢ d = (c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \to d \circ M = ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) \circ M$
161	160	fveq2d	$⊢ d = (c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \to P (d \circ M) = P (((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) \circ M)$
162		fvex	$⊢ P (((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) \circ M) \in V$
163	161 43 162	fvmpt	$⊢ (c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \in (ℤ^{S}) \to (d \in (ℤ^{S}) ⟼ P (d \circ M)) ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) = P (((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) \circ M)$
164	159 163	syl	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to (d \in (ℤ^{S}) ⟼ P (d \circ M)) ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) = P (((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) \circ M)$
165		coundir	$⊢ ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) \circ M = ((c \circ M^{-1}) \circ M) \cup (((S ∖ ran M) \times \{0\}) \circ M)$
166		coass	$⊢ (c \circ M^{-1}) \circ M = c \circ (M^{-1} \circ M)$
167		f1cocnv1	$⊢ M : T \underset{1-1}{⟶} S \to M^{-1} \circ M = {I ↾}_{T}$
168	167	coeq2d	$⊢ M : T \underset{1-1}{⟶} S \to c \circ (M^{-1} \circ M) = c \circ ({I ↾}_{T})$
169	62 168	syl	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to c \circ (M^{-1} \circ M) = c \circ ({I ↾}_{T})$
170	166 169	syl5eq	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to (c \circ M^{-1}) \circ M = c \circ ({I ↾}_{T})$
171	118	ineq1i	$⊢ dom ((S ∖ ran M) \times \{0\}) \cap ran M = (S ∖ ran M) \cap ran M$
172		incom	$⊢ (S ∖ ran M) \cap ran M = ran M \cap (S ∖ ran M)$
173	171 172 71	3eqtri	$⊢ dom ((S ∖ ran M) \times \{0\}) \cap ran M = \emptyset$
174		coeq0	$⊢ ((S ∖ ran M) \times \{0\}) \circ M = \emptyset \leftrightarrow dom ((S ∖ ran M) \times \{0\}) \cap ran M = \emptyset$
175	173 174	mpbir	$⊢ ((S ∖ ran M) \times \{0\}) \circ M = \emptyset$
176	175	a1i	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((S ∖ ran M) \times \{0\}) \circ M = \emptyset$
177	170 176	uneq12d	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((c \circ M^{-1}) \circ M) \cup (((S ∖ ran M) \times \{0\}) \circ M) = (c \circ ({I ↾}_{T})) \cup \emptyset$
178		un0	$⊢ (c \circ ({I ↾}_{T})) \cup \emptyset = c \circ ({I ↾}_{T})$
179		fcoi1	$⊢ c : T ⟶ ℕ_{0} \to c \circ ({I ↾}_{T}) = c$
180	61 179	syl	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to c \circ ({I ↾}_{T}) = c$
181	178 180	syl5eq	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to (c \circ ({I ↾}_{T})) \cup \emptyset = c$
182	177 181	eqtrd	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((c \circ M^{-1}) \circ M) \cup (((S ∖ ran M) \times \{0\}) \circ M) = c$
183	165 182	syl5eq	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) \circ M = c$
184	183	fveq2d	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to P (((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) \circ M) = P (c)$
185		simprr	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to P (c) = 0$
186	164 184 185	3eqtrd	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to (d \in (ℤ^{S}) ⟼ P (d \circ M)) ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) = 0$
187		reseq1	$⊢ b = (c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \to {b ↾}_{O} = {((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) ↾}_{O}$
188	187	eqeq2d	$⊢ b = (c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \to (a = {b ↾}_{O} \leftrightarrow a = {((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) ↾}_{O})$
189		fveqeq2	$⊢ b = (c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \to ((d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0 \leftrightarrow (d \in (ℤ^{S}) ⟼ P (d \circ M)) ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) = 0)$
190	188 189	anbi12d	$⊢ b = (c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \to ((a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0) \leftrightarrow (a = {((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) = 0))$
191	190	rspcev	$⊢ ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\}) \in ({ℕ_{0}}^{S}) \land (a = {((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) ((c \circ M^{-1}) \cup ((S ∖ ran M) \times \{0\})) = 0)) \to \exists b \in ({ℕ_{0}}^{S}) (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)$
192	91 140 186 191	syl12anc	$⊢ (((S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \land c \in ({ℕ_{0}}^{T})) \land (a = {c ↾}_{O} \land P (c) = 0)) \to \exists b \in ({ℕ_{0}}^{S}) (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)$
193	192	rexlimdva2	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to (\exists c \in ({ℕ_{0}}^{T}) (a = {c ↾}_{O} \land P (c) = 0) \to \exists b \in ({ℕ_{0}}^{S}) (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0))$
194	55 193	impbid	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to (\exists b \in ({ℕ_{0}}^{S}) (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0) \leftrightarrow \exists c \in ({ℕ_{0}}^{T}) (a = {c ↾}_{O} \land P (c) = 0))$
195	194	abbidv	$⊢ (S \in V \land M : T \underset{1-1}{⟶} S \land {M ↾}_{O} = {I ↾}_{O}) \to \{a \| \exists b \in ({ℕ_{0}}^{S}) (a = {b ↾}_{O} \land (d \in (ℤ^{S}) ⟼ P (d \circ M)) (b) = 0)\} = \{a \| \exists c \in ({ℕ_{0}}^{T}) (a = {c ↾}_{O} \land P (c) = 0)\}$

Metamath Proof Explorer

Theorem diophrw

Proof