This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑍 )