poimirlem10

Description: Lemma for poimir establishing the cube that yields the simplex that yields a face if the opposite vertex was first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
	poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
	poimirlem12.2	$⊢ φ \to T \in S$
	poimirlem11.3	$⊢ φ \to 2^{nd} (T) = 0$
Assertion	poimirlem10	$⊢ φ \to F (N - 1) -_{f} ((1 \dots N) \times \{1\}) = 1^{st} (1^{st} (T))$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
3		poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
4		poimirlem12.2	$⊢ φ \to T \in S$
5		poimirlem11.3	$⊢ φ \to 2^{nd} (T) = 0$
6		ovexd	$⊢ φ \to (1 \dots N) \in V$
7		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
8	1 7	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
9		nn0fz0	$⊢ N - 1 \in ℕ_{0} \leftrightarrow N - 1 \in (0 \dots N - 1)$
10	8 9	sylib	$⊢ φ \to N - 1 \in (0 \dots N - 1)$
11	3 10	ffvelrnd	$⊢ φ \to F (N - 1) \in ({(0 \dots K)}^{(1 \dots N)})$
12		elmapfn	$⊢ F (N - 1) \in ({(0 \dots K)}^{(1 \dots N)}) \to F (N - 1) Fn (1 \dots N)$
13	11 12	syl	$⊢ φ \to F (N - 1) Fn (1 \dots N)$
14		1ex	$⊢ 1 \in V$
15		fnconstg	$⊢ 1 \in V \to ((1 \dots N) \times \{1\}) Fn (1 \dots N)$
16	14 15	mp1i	$⊢ φ \to ((1 \dots N) \times \{1\}) Fn (1 \dots N)$
17		elrabi	$⊢ T \in \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\} \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
18	17 2	eleq2s	$⊢ T \in S \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
19	4 18	syl	$⊢ φ \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
20		xp1st	$⊢ T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
21	19 20	syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
22		xp1st	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
23	21 22	syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
24		elmapfn	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
25	23 24	syl	$⊢ φ \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
26		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
27	26	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
28	27	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
29	28	csbeq1d	$⊢ t = T \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))$
30		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
31		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
32	31	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
33	32	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
34	31	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
35	34	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}$
36	33 35	uneq12d	$⊢ t = T \to (2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})$
37	30 36	oveq12d	$⊢ t = T \to 1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))$
38	37	csbeq2dv	$⊢ t = T \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
39	29 38	eqtrd	$⊢ t = T \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
40	39	mpteq2dv	$⊢ t = T \to (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
41	40	eqeq2d	$⊢ t = T \to (F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) \leftrightarrow F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))))$
42	41 2	elrab2	$⊢ T \in S \leftrightarrow (T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))))$
43	42	simprbi	$⊢ T \in S \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
44	4 43	syl	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
45		breq12	$⊢ (y = N - 1 \land 2^{nd} (T) = 0) \to (y < 2^{nd} (T) \leftrightarrow N - 1 < 0)$
46	5 45	sylan2	$⊢ (y = N - 1 \land φ) \to (y < 2^{nd} (T) \leftrightarrow N - 1 < 0)$
47	46	ancoms	$⊢ (φ \land y = N - 1) \to (y < 2^{nd} (T) \leftrightarrow N - 1 < 0)$
48		oveq1	$⊢ y = N - 1 \to y + 1 = N - 1 + 1$
49	1	nncnd	$⊢ φ \to N \in ℂ$
50		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
51	49 50	syl	$⊢ φ \to N - 1 + 1 = N$
52	48 51	sylan9eqr	$⊢ (φ \land y = N - 1) \to y + 1 = N$
53	47 52	ifbieq2d	$⊢ (φ \land y = N - 1) \to if (y < 2^{nd} (T), y, y + 1) = if (N - 1 < 0, y, N)$
54	8	nn0ge0d	$⊢ φ \to 0 \leq N - 1$
55		0red	$⊢ φ \to 0 \in ℝ$
56	8	nn0red	$⊢ φ \to N - 1 \in ℝ$
57	55 56	lenltd	$⊢ φ \to (0 \leq N - 1 \leftrightarrow \neg N - 1 < 0)$
58	54 57	mpbid	$⊢ φ \to \neg N - 1 < 0$
59	58	iffalsed	$⊢ φ \to if (N - 1 < 0, y, N) = N$
60	59	adantr	$⊢ (φ \land y = N - 1) \to if (N - 1 < 0, y, N) = N$
61	53 60	eqtrd	$⊢ (φ \land y = N - 1) \to if (y < 2^{nd} (T), y, y + 1) = N$
62	61	csbeq1d	$⊢ (φ \land y = N - 1) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ N / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
63		oveq2	$⊢ j = N \to (1 \dots j) = (1 \dots N)$
64	63	imaeq2d	$⊢ j = N \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots N)]$
65		xp2nd	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
66	21 65	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
67		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
68		f1oeq1	$⊢ f = 2^{nd} (1^{st} (T)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
69	67 68	elab	$⊢ 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
70	66 69	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
71		f1ofo	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
72		foima	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
73	70 71 72	3syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
74	64 73	sylan9eqr	$⊢ (φ \land j = N) \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = (1 \dots N)$
75	74	xpeq1d	$⊢ (φ \land j = N) \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = (1 \dots N) \times \{1\}$
76		oveq1	$⊢ j = N \to j + 1 = N + 1$
77	76	oveq1d	$⊢ j = N \to (j + 1 \dots N) = (N + 1 \dots N)$
78	1	nnred	$⊢ φ \to N \in ℝ$
79	78	ltp1d	$⊢ φ \to N < N + 1$
80	1	nnzd	$⊢ φ \to N \in ℤ$
81	80	peano2zd	$⊢ φ \to N + 1 \in ℤ$
82		fzn	$⊢ (N + 1 \in ℤ \land N \in ℤ) \to (N < N + 1 \leftrightarrow (N + 1 \dots N) = \emptyset)$
83	81 80 82	syl2anc	$⊢ φ \to (N < N + 1 \leftrightarrow (N + 1 \dots N) = \emptyset)$
84	79 83	mpbid	$⊢ φ \to (N + 1 \dots N) = \emptyset$
85	77 84	sylan9eqr	$⊢ (φ \land j = N) \to (j + 1 \dots N) = \emptyset$
86	85	imaeq2d	$⊢ (φ \land j = N) \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
87	86	xpeq1d	$⊢ (φ \land j = N) \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [\emptyset] \times \{0\}$
88		ima0	$⊢ 2^{nd} (1^{st} (T)) [\emptyset] = \emptyset$
89	88	xpeq1i	$⊢ 2^{nd} (1^{st} (T)) [\emptyset] \times \{0\} = \emptyset \times \{0\}$
90		0xp	$⊢ \emptyset \times \{0\} = \emptyset$
91	89 90	eqtri	$⊢ 2^{nd} (1^{st} (T)) [\emptyset] \times \{0\} = \emptyset$
92	87 91	eqtrdi	$⊢ (φ \land j = N) \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = \emptyset$
93	75 92	uneq12d	$⊢ (φ \land j = N) \to (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}) = ((1 \dots N) \times \{1\}) \cup \emptyset$
94		un0	$⊢ ((1 \dots N) \times \{1\}) \cup \emptyset = (1 \dots N) \times \{1\}$
95	93 94	eqtrdi	$⊢ (φ \land j = N) \to (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}) = (1 \dots N) \times \{1\}$
96	95	oveq2d	$⊢ (φ \land j = N) \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((1 \dots N) \times \{1\})$
97	1 96	csbied	$⊢ φ \to ⦋ N / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((1 \dots N) \times \{1\})$
98	97	adantr	$⊢ (φ \land y = N - 1) \to ⦋ N / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((1 \dots N) \times \{1\})$
99	62 98	eqtrd	$⊢ (φ \land y = N - 1) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((1 \dots N) \times \{1\})$
100		ovexd	$⊢ φ \to 1^{st} (1^{st} (T)) +_{f} ((1 \dots N) \times \{1\}) \in V$
101	44 99 10 100	fvmptd	$⊢ φ \to F (N - 1) = 1^{st} (1^{st} (T)) +_{f} ((1 \dots N) \times \{1\})$
102	101	fveq1d	$⊢ φ \to F (N - 1) (n) = (1^{st} (1^{st} (T)) +_{f} ((1 \dots N) \times \{1\})) (n)$
103	102	adantr	$⊢ (φ \land n \in (1 \dots N)) \to F (N - 1) (n) = (1^{st} (1^{st} (T)) +_{f} ((1 \dots N) \times \{1\})) (n)$
104		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
105		eqidd	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) = 1^{st} (1^{st} (T)) (n)$
106	14	fvconst2	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{1\}) (n) = 1$
107	106	adantl	$⊢ (φ \land n \in (1 \dots N)) \to ((1 \dots N) \times \{1\}) (n) = 1$
108	25 16 6 6 104 105 107	ofval	$⊢ (φ \land n \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((1 \dots N) \times \{1\})) (n) = 1^{st} (1^{st} (T)) (n) + 1$
109	103 108	eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to F (N - 1) (n) = 1^{st} (1^{st} (T)) (n) + 1$
110		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
111	23 110	syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
112	111	ffvelrnda	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) \in (0 ..^K)$
113		elfzonn0	$⊢ 1^{st} (1^{st} (T)) (n) \in (0 ..^K) \to 1^{st} (1^{st} (T)) (n) \in ℕ_{0}$
114	112 113	syl	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) \in ℕ_{0}$
115	114	nn0cnd	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) \in ℂ$
116		pncan1	$⊢ 1^{st} (1^{st} (T)) (n) \in ℂ \to 1^{st} (1^{st} (T)) (n) + 1 - 1 = 1^{st} (1^{st} (T)) (n)$
117	115 116	syl	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) + 1 - 1 = 1^{st} (1^{st} (T)) (n)$
118	6 13 16 25 109 107 117	offveq	$⊢ φ \to F (N - 1) -_{f} ((1 \dots N) \times \{1\}) = 1^{st} (1^{st} (T))$

Metamath Proof Explorer

Theorem poimirlem10

Proof