Theorem mapfienlem2

Description: Lemma 2 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	mapfienlem2	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) 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	10	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑍 ∈ 𝐵 )
12		f1of	⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → 𝐺 : 𝐵 ⟶ 𝐷 )
13	5 12	syl	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐷 )
14	13 10	ffvelcdmd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑍 ) ∈ 𝐷 )
15	3 14	eqeltrid	⊢ ( 𝜑 → 𝑊 ∈ 𝐷 )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑊 ∈ 𝐷 )
17		elrabi	⊢ ( 𝑔 ∈ { 𝑥 ∈ ( 𝐷 ↑m 𝐶 ) ∣ 𝑥 finSupp 𝑊 } → 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) )
18		elmapi	⊢ ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
19	17 18	syl	⊢ ( 𝑔 ∈ { 𝑥 ∈ ( 𝐷 ↑m 𝐶 ) ∣ 𝑥 finSupp 𝑊 } → 𝑔 : 𝐶 ⟶ 𝐷 )
20	19 2	eleq2s	⊢ ( 𝑔 ∈ 𝑇 → 𝑔 : 𝐶 ⟶ 𝐷 )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
22		f1ocnv	⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 )
23		f1of	⊢ ( ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐵 → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
24	5 22 23	3syl	⊢ ( 𝜑 → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ◡ 𝐺 : 𝐷 ⟶ 𝐵 )
26		ssidd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝐷 ⊆ 𝐷 )
27	8	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝐶 ∈ 𝑋 )
28	9	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝐷 ∈ 𝑌 )
29		breq1	⊢ ( 𝑥 = 𝑔 → ( 𝑥 finSupp 𝑊 ↔ 𝑔 finSupp 𝑊 ) )
30	29	elrab	⊢ ( 𝑔 ∈ { 𝑥 ∈ ( 𝐷 ↑m 𝐶 ) ∣ 𝑥 finSupp 𝑊 } ↔ ( 𝑔 ∈ ( 𝐷 ↑m 𝐶 ) ∧ 𝑔 finSupp 𝑊 ) )
31	30	simprbi	⊢ ( 𝑔 ∈ { 𝑥 ∈ ( 𝐷 ↑m 𝐶 ) ∣ 𝑥 finSupp 𝑊 } → 𝑔 finSupp 𝑊 )
32	31 2	eleq2s	⊢ ( 𝑔 ∈ 𝑇 → 𝑔 finSupp 𝑊 )
33	32	adantl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → 𝑔 finSupp 𝑊 )
34	5 10	jca	⊢ ( 𝜑 → ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 ∧ 𝑍 ∈ 𝐵 ) )
35	3	eqcomi	⊢ ( 𝐺 ‘ 𝑍 ) = 𝑊
36	34 35	jctir	⊢ ( 𝜑 → ( ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑍 ) = 𝑊 ) )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑍 ) = 𝑊 ) )
38		f1ocnvfv	⊢ ( ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑍 ) = 𝑊 → ( ◡ 𝐺 ‘ 𝑊 ) = 𝑍 ) )
39	38	imp	⊢ ( ( ( 𝐺 : 𝐵 –1-1-onto→ 𝐷 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑍 ) = 𝑊 ) → ( ◡ 𝐺 ‘ 𝑊 ) = 𝑍 )
40	37 39	syl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ◡ 𝐺 ‘ 𝑊 ) = 𝑍 )
41	11 16 21 25 26 27 28 33 40	fsuppcor	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ◡ 𝐺 ∘ 𝑔 ) finSupp 𝑍 )
42		f1ocnv	⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 )
43		f1of1	⊢ ( ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 → ◡ 𝐹 : 𝐴 –1-1→ 𝐶 )
44	4 42 43	3syl	⊢ ( 𝜑 → ◡ 𝐹 : 𝐴 –1-1→ 𝐶 )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ◡ 𝐹 : 𝐴 –1-1→ 𝐶 )
46	13 7	jca	⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐷 ∧ 𝐵 ∈ 𝑉 ) )
47		fex	⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐷 ∧ 𝐵 ∈ 𝑉 ) → 𝐺 ∈ V )
48		cnvexg	⊢ ( 𝐺 ∈ V → ◡ 𝐺 ∈ V )
49	46 47 48	3syl	⊢ ( 𝜑 → ◡ 𝐺 ∈ V )
50		coexg	⊢ ( ( ◡ 𝐺 ∈ V ∧ 𝑔 ∈ 𝑇 ) → ( ◡ 𝐺 ∘ 𝑔 ) ∈ V )
51	49 50	sylan	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ◡ 𝐺 ∘ 𝑔 ) ∈ V )
52	41 45 11 51	fsuppco	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ◡ 𝐺 ∘ 𝑔 ) ∘ ◡ 𝐹 ) finSupp 𝑍 )