Theorem fcobijfs

Description: Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien . (Contributed by Thierry Arnoux, 25-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

	Ref	Expression
Hypotheses	fcobij.1	⊢ ( 𝜑 → 𝐺 : 𝑆 –1-1-onto→ 𝑇 )
	fcobij.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
	fcobij.3	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	fcobij.4	⊢ ( 𝜑 → 𝑇 ∈ 𝑊 )
	fcobijfs.5	⊢ ( 𝜑 → 𝑂 ∈ 𝑆 )
	fcobijfs.6	⊢ 𝑄 = ( 𝐺 ‘ 𝑂 )
	fcobijfs.7	⊢ 𝑋 = { 𝑔 ∈ ( 𝑆 ↑m 𝑅 ) ∣ 𝑔 finSupp 𝑂 }
	fcobijfs.8	⊢ 𝑌 = { ℎ ∈ ( 𝑇 ↑m 𝑅 ) ∣ ℎ finSupp 𝑄 }
Assertion	fcobijfs	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ 𝑓 ) ) : 𝑋 –1-1-onto→ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		fcobij.1	⊢ ( 𝜑 → 𝐺 : 𝑆 –1-1-onto→ 𝑇 )
2		fcobij.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
3		fcobij.3	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		fcobij.4	⊢ ( 𝜑 → 𝑇 ∈ 𝑊 )
5		fcobijfs.5	⊢ ( 𝜑 → 𝑂 ∈ 𝑆 )
6		fcobijfs.6	⊢ 𝑄 = ( 𝐺 ‘ 𝑂 )
7		fcobijfs.7	⊢ 𝑋 = { 𝑔 ∈ ( 𝑆 ↑m 𝑅 ) ∣ 𝑔 finSupp 𝑂 }
8		fcobijfs.8	⊢ 𝑌 = { ℎ ∈ ( 𝑇 ↑m 𝑅 ) ∣ ℎ finSupp 𝑄 }
9		breq1	⊢ ( ℎ = 𝑔 → ( ℎ finSupp 𝑂 ↔ 𝑔 finSupp 𝑂 ) )
10	9	cbvrabv	⊢ { ℎ ∈ ( 𝑆 ↑m 𝑅 ) ∣ ℎ finSupp 𝑂 } = { 𝑔 ∈ ( 𝑆 ↑m 𝑅 ) ∣ 𝑔 finSupp 𝑂 }
11	7 10	eqtr4i	⊢ 𝑋 = { ℎ ∈ ( 𝑆 ↑m 𝑅 ) ∣ ℎ finSupp 𝑂 }
12		f1oi	⊢ ( I ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑅
13	12	a1i	⊢ ( 𝜑 → ( I ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑅 )
14	11 8 6 13 1 2 3 2 4 5	mapfien	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ ( 𝑓 ∘ ( I ↾ 𝑅 ) ) ) ) : 𝑋 –1-1-onto→ 𝑌 )
15	7	ssrab3	⊢ 𝑋 ⊆ ( 𝑆 ↑m 𝑅 )
16	15	sseli	⊢ ( 𝑓 ∈ 𝑋 → 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) )
17		coass	⊢ ( ( 𝐺 ∘ 𝑓 ) ∘ ( I ↾ 𝑅 ) ) = ( 𝐺 ∘ ( 𝑓 ∘ ( I ↾ 𝑅 ) ) )
18		f1of	⊢ ( 𝐺 : 𝑆 –1-1-onto→ 𝑇 → 𝐺 : 𝑆 ⟶ 𝑇 )
19	1 18	syl	⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ 𝑇 )
20		elmapi	⊢ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) → 𝑓 : 𝑅 ⟶ 𝑆 )
21		fco	⊢ ( ( 𝐺 : 𝑆 ⟶ 𝑇 ∧ 𝑓 : 𝑅 ⟶ 𝑆 ) → ( 𝐺 ∘ 𝑓 ) : 𝑅 ⟶ 𝑇 )
22	19 20 21	syl2an	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ) → ( 𝐺 ∘ 𝑓 ) : 𝑅 ⟶ 𝑇 )
23		fcoi1	⊢ ( ( 𝐺 ∘ 𝑓 ) : 𝑅 ⟶ 𝑇 → ( ( 𝐺 ∘ 𝑓 ) ∘ ( I ↾ 𝑅 ) ) = ( 𝐺 ∘ 𝑓 ) )
24	22 23	syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ) → ( ( 𝐺 ∘ 𝑓 ) ∘ ( I ↾ 𝑅 ) ) = ( 𝐺 ∘ 𝑓 ) )
25	17 24	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ) → ( 𝐺 ∘ ( 𝑓 ∘ ( I ↾ 𝑅 ) ) ) = ( 𝐺 ∘ 𝑓 ) )
26	16 25	sylan2	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝐺 ∘ ( 𝑓 ∘ ( I ↾ 𝑅 ) ) ) = ( 𝐺 ∘ 𝑓 ) )
27	26	mpteq2dva	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ ( 𝑓 ∘ ( I ↾ 𝑅 ) ) ) ) = ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ 𝑓 ) ) )
28		f1oeq1	⊢ ( ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ ( 𝑓 ∘ ( I ↾ 𝑅 ) ) ) ) = ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ 𝑓 ) ) → ( ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ ( 𝑓 ∘ ( I ↾ 𝑅 ) ) ) ) : 𝑋 –1-1-onto→ 𝑌 ↔ ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ 𝑓 ) ) : 𝑋 –1-1-onto→ 𝑌 ) )
29	27 28	syl	⊢ ( 𝜑 → ( ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ ( 𝑓 ∘ ( I ↾ 𝑅 ) ) ) ) : 𝑋 –1-1-onto→ 𝑌 ↔ ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ 𝑓 ) ) : 𝑋 –1-1-onto→ 𝑌 ) )
30	14 29	mpbid	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑋 ↦ ( 𝐺 ∘ 𝑓 ) ) : 𝑋 –1-1-onto→ 𝑌 )