eulerpartlemgu

Description: Lemma for eulerpart : Rewriting the U set for an odd partition Note that interestingly, this proof reuses marypha2lem2 . (Contributed by Thierry Arnoux, 10-Aug-2018)

	Ref	Expression
Hypotheses	eulerpart.p	$⊢ P = \{f \in ({ℕ_{0}}^{ℕ}) \| (f^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} f (k) k = N)\}$
	eulerpart.o	$⊢ O = \{g \in P \| \forall n \in g^{-1} [ℕ] \neg 2 ∥ n\}$
	eulerpart.d	$⊢ D = \{g \in P \| \forall n \in ℕ g (n) \leq 1\}$
	eulerpart.j	$⊢ J = \{z \in ℕ \| \neg 2 ∥ z\}$
	eulerpart.f	$⊢ F = (x \in J, y \in ℕ_{0} ⟼ 2^{y} x)$
	eulerpart.h	$⊢ H = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
	eulerpart.m	$⊢ M = (r \in H ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
	eulerpart.r	$⊢ R = \{f \| f^{-1} [ℕ] \in Fin\}$
	eulerpart.t	$⊢ T = \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq J\}$
	eulerpart.g	$⊢ G = (o \in (T \cap R) ⟼ 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
	eulerpartlemgh.1	$⊢ U = ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))$
Assertion	eulerpartlemgu	$⊢ A \in (T \cap R) \to U = \{⟨t, n⟩ \| (t \in (A^{-1} [ℕ] \cap J) \land n \in (bits \circ A) (t))\}$

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	$⊢ P = \{f \in ({ℕ_{0}}^{ℕ}) \| (f^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} f (k) k = N)\}$
2		eulerpart.o	$⊢ O = \{g \in P \| \forall n \in g^{-1} [ℕ] \neg 2 ∥ n\}$
3		eulerpart.d	$⊢ D = \{g \in P \| \forall n \in ℕ g (n) \leq 1\}$
4		eulerpart.j	$⊢ J = \{z \in ℕ \| \neg 2 ∥ z\}$
5		eulerpart.f	$⊢ F = (x \in J, y \in ℕ_{0} ⟼ 2^{y} x)$
6		eulerpart.h	$⊢ H = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
7		eulerpart.m	$⊢ M = (r \in H ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
8		eulerpart.r	$⊢ R = \{f \| f^{-1} [ℕ] \in Fin\}$
9		eulerpart.t	$⊢ T = \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq J\}$
10		eulerpart.g	$⊢ G = (o \in (T \cap R) ⟼ 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
11		eulerpartlemgh.1	$⊢ U = ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))$
12	1 2 3 4 5 6 7 8 9	eulerpartlemt0	$⊢ A \in (T \cap R) \leftrightarrow (A \in ({ℕ_{0}}^{ℕ}) \land A^{-1} [ℕ] \in Fin \land A^{-1} [ℕ] \subseteq J)$
13	12	simp1bi	$⊢ A \in (T \cap R) \to A \in ({ℕ_{0}}^{ℕ})$
14		elmapi	$⊢ A \in ({ℕ_{0}}^{ℕ}) \to A : ℕ ⟶ ℕ_{0}$
15	13 14	syl	$⊢ A \in (T \cap R) \to A : ℕ ⟶ ℕ_{0}$
16	15	adantr	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to A : ℕ ⟶ ℕ_{0}$
17	16	ffund	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to Fun A$
18		inss1	$⊢ A^{-1} [ℕ] \cap J \subseteq A^{-1} [ℕ]$
19		cnvimass	$⊢ A^{-1} [ℕ] \subseteq dom A$
20	19 15	fssdm	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \subseteq ℕ$
21	18 20	sstrid	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \cap J \subseteq ℕ$
22	21	sselda	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in ℕ$
23	15	fdmd	$⊢ A \in (T \cap R) \to dom A = ℕ$
24	23	eleq2d	$⊢ A \in (T \cap R) \to (t \in dom A \leftrightarrow t \in ℕ)$
25	24	adantr	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to (t \in dom A \leftrightarrow t \in ℕ)$
26	22 25	mpbird	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in dom A$
27		fvco	$⊢ (Fun A \land t \in dom A) \to (bits \circ A) (t) = bits (A (t))$
28	17 26 27	syl2anc	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to (bits \circ A) (t) = bits (A (t))$
29	28	xpeq2d	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to \{t\} \times (bits \circ A) (t) = \{t\} \times bits (A (t))$
30	29	iuneq2dv	$⊢ A \in (T \cap R) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times (bits \circ A) (t)) = ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))$
31		eqid	$⊢ ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times (bits \circ A) (t)) = ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times (bits \circ A) (t))$
32	31	marypha2lem2	$⊢ ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times (bits \circ A) (t)) = \{⟨t, n⟩ \| (t \in (A^{-1} [ℕ] \cap J) \land n \in (bits \circ A) (t))\}$
33	30 32	eqtr3di	$⊢ A \in (T \cap R) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) = \{⟨t, n⟩ \| (t \in (A^{-1} [ℕ] \cap J) \land n \in (bits \circ A) (t))\}$
34	11 33	eqtrid	$⊢ A \in (T \cap R) \to U = \{⟨t, n⟩ \| (t \in (A^{-1} [ℕ] \cap J) \land n \in (bits \circ A) (t))\}$

Metamath Proof Explorer

Theorem eulerpartlemgu

Proof