Theorem 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	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
	eulerpart.o	⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
	eulerpart.d	⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
	eulerpart.j	⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
	eulerpart.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
	eulerpart.h	⊢ 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
	eulerpart.m	⊢ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
	eulerpart.r	⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	eulerpart.t	⊢ 𝑇 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 }
	eulerpart.g	⊢ 𝐺 = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
	eulerpartlemgh.1	⊢ 𝑈 = ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
Assertion	eulerpartlemgu	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝑈 = { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2		eulerpart.o	⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
3		eulerpart.d	⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
4		eulerpart.j	⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
5		eulerpart.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
6		eulerpart.h	⊢ 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
7		eulerpart.m	⊢ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
8		eulerpart.r	⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
9		eulerpart.t	⊢ 𝑇 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 }
10		eulerpart.g	⊢ 𝐺 = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
11		eulerpartlemgh.1	⊢ 𝑈 = ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
12	1 2 3 4 5 6 7 8 9	eulerpartlemt0	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) )
13	12	simp1bi	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ ( ℕ0 ↑m ℕ ) )
14		elmapi	⊢ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) → 𝐴 : ℕ ⟶ ℕ0 )
15	13 14	syl	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
16	15	adantr	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝐴 : ℕ ⟶ ℕ0 )
17	16	ffund	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → Fun 𝐴 )
18		inss1	⊢ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ ( ◡ 𝐴 “ ℕ )
19		cnvimass	⊢ ( ◡ 𝐴 “ ℕ ) ⊆ dom 𝐴
20	19 15	fssdm	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ 𝐴 “ ℕ ) ⊆ ℕ )
21	18 20	sstrid	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ ℕ )
22	21	sselda	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ℕ )
23	15	fdmd	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → dom 𝐴 = ℕ )
24	23	eleq2d	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑡 ∈ dom 𝐴 ↔ 𝑡 ∈ ℕ ) )
25	24	adantr	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( 𝑡 ∈ dom 𝐴 ↔ 𝑡 ∈ ℕ ) )
26	22 25	mpbird	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ dom 𝐴 )
27		fvco	⊢ ( ( Fun 𝐴 ∧ 𝑡 ∈ dom 𝐴 ) → ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) = ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
28	17 26 27	syl2anc	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) = ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) )
29	28	xpeq2d	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( { 𝑡 } × ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) ) = ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) )
30	29	iuneq2dv	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) ) = ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) )
31		eqid	⊢ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) ) = ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) )
32	31	marypha2lem2	⊢ ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) ) = { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) ) }
33	30 32	eqtr3di	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ∪ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴 ‘ 𝑡 ) ) ) = { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) ) } )
34	11 33	eqtrid	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝑈 = { ⟨ 𝑡 , 𝑛 ⟩ ∣ ( 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( ( bits ∘ 𝐴 ) ‘ 𝑡 ) ) } )