mapfienlem1

Description: Lemma 1 for mapfien . (Contributed by AV, 3-Jul-2019) (Revised by AV, 28-Jul-2024)

	Ref	Expression
Hypotheses	mapfien.s	⊢ 𝑆 = { 𝑥 ∈ ( 𝐵 ↑_m 𝐴 ) ∣ 𝑥 finSupp 𝑍 }
	mapfien.t	⊢ 𝑇 = { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp 𝑊 }
	mapfien.w	⊢ 𝑊 = ( 𝐺 ‘ 𝑍 )
	mapfien.f	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
	mapfien.g	⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
	mapfien.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	mapfien.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	mapfien.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	mapfien.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
	mapfien.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	mapfienlem1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) finSupp 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		mapfien.s	⊢ 𝑆 = { 𝑥 ∈ ( 𝐵 ↑_m 𝐴 ) ∣ 𝑥 finSupp 𝑍 }
2		mapfien.t	⊢ 𝑇 = { 𝑥 ∈ ( 𝐷 ↑_m 𝐶 ) ∣ 𝑥 finSupp 𝑊 }
3		mapfien.w	⊢ 𝑊 = ( 𝐺 ‘ 𝑍 )
4		mapfien.f	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
5		mapfien.g	⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1-onto→ 𝐷 )
6		mapfien.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
7		mapfien.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
8		mapfien.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
9		mapfien.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
10		mapfien.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
11	3	fvexi	⊢ 𝑊 ∈ V
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝑊 ∈ V )
13	10	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝑍 ∈ 𝐵 )
14		elrabi	⊢ ( 𝑓 ∈ { 𝑥 ∈ ( 𝐵 ↑_m 𝐴 ) ∣ 𝑥 finSupp 𝑍 } → 𝑓 ∈ ( 𝐵 ↑_m 𝐴 ) )
15		elmapi	⊢ ( 𝑓 ∈ ( 𝐵 ↑_m 𝐴 ) → 𝑓 : 𝐴 ⟶ 𝐵 )
16	14 15	syl	⊢ ( 𝑓 ∈ { 𝑥 ∈ ( 𝐵 ↑_m 𝐴 ) ∣ 𝑥 finSupp 𝑍 } → 𝑓 : 𝐴 ⟶ 𝐵 )
17	16 1	eleq2s	⊢ ( 𝑓 ∈ 𝑆 → 𝑓 : 𝐴 ⟶ 𝐵 )
18		f1of	⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 ⟶ 𝐴 )
19	4 18	syl	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐴 )
20		fco	⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : 𝐶 ⟶ 𝐴 ) → ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 )
21	17 19 20	syl2anr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝑓 ∘ 𝐹 ) : 𝐶 ⟶ 𝐵 )
22		f1of	⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → 𝐺 : 𝐵 ⟶ 𝐷 )
23	5 22	syl	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐷 )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝐺 : 𝐵 ⟶ 𝐷 )
25		ssidd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝐵 ⊆ 𝐵 )
26	8	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝐶 ∈ 𝑋 )
27	7	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
28		breq1	⊢ ( 𝑥 = 𝑓 → ( 𝑥 finSupp 𝑍 ↔ 𝑓 finSupp 𝑍 ) )
29	28 1	elrab2	⊢ ( 𝑓 ∈ 𝑆 ↔ ( 𝑓 ∈ ( 𝐵 ↑_m 𝐴 ) ∧ 𝑓 finSupp 𝑍 ) )
30	29	simprbi	⊢ ( 𝑓 ∈ 𝑆 → 𝑓 finSupp 𝑍 )
31	30	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝑓 finSupp 𝑍 )
32		f1of1	⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 –1-1→ 𝐴 )
33	4 32	syl	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1→ 𝐴 )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝐹 : 𝐶 –1-1→ 𝐴 )
35		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → 𝑓 ∈ 𝑆 )
36	31 34 13 35	fsuppco	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝑓 ∘ 𝐹 ) finSupp 𝑍 )
37	3	eqcomi	⊢ ( 𝐺 ‘ 𝑍 ) = 𝑊
38	37	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑍 ) = 𝑊 )
39	12 13 21 24 25 26 27 36 38	fsuppcor	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ( 𝐺 ∘ ( 𝑓 ∘ 𝐹 ) ) finSupp 𝑊 )

Metamath Proof Explorer

Theorem mapfienlem1

Proof