mapfienlem2

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

	Ref	Expression
Hypotheses	mapfien.s	$⊢ S = \{x \in (B^{A}) \| {finSupp}_{Z} (x)\}$
	mapfien.t	$⊢ T = \{x \in (D^{C}) \| {finSupp}_{W} (x)\}$
	mapfien.w	$⊢ W = G (Z)$
	mapfien.f	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
	mapfien.g	$⊢ φ \to G : B \underset{1-1 onto}{⟶} D$
	mapfien.a	$⊢ φ \to A \in U$
	mapfien.b	$⊢ φ \to B \in V$
	mapfien.c	$⊢ φ \to C \in X$
	mapfien.d	$⊢ φ \to D \in Y$
	mapfien.z	$⊢ φ \to Z \in B$
Assertion	mapfienlem2	$⊢ (φ \land g \in T) \to {finSupp}_{Z} (((G^{-1} \circ g) \circ F^{-1}))$

Proof

Step	Hyp	Ref	Expression
1		mapfien.s	$⊢ S = \{x \in (B^{A}) \| {finSupp}_{Z} (x)\}$
2		mapfien.t	$⊢ T = \{x \in (D^{C}) \| {finSupp}_{W} (x)\}$
3		mapfien.w	$⊢ W = G (Z)$
4		mapfien.f	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
5		mapfien.g	$⊢ φ \to G : B \underset{1-1 onto}{⟶} D$
6		mapfien.a	$⊢ φ \to A \in U$
7		mapfien.b	$⊢ φ \to B \in V$
8		mapfien.c	$⊢ φ \to C \in X$
9		mapfien.d	$⊢ φ \to D \in Y$
10		mapfien.z	$⊢ φ \to Z \in B$
11	10	adantr	$⊢ (φ \land g \in T) \to Z \in B$
12		f1of	$⊢ G : B \underset{1-1 onto}{⟶} D \to G : B ⟶ D$
13	5 12	syl	$⊢ φ \to G : B ⟶ D$
14	13 10	ffvelcdmd	$⊢ φ \to G (Z) \in D$
15	3 14	eqeltrid	$⊢ φ \to W \in D$
16	15	adantr	$⊢ (φ \land g \in T) \to W \in D$
17		elrabi	$⊢ g \in \{x \in (D^{C}) \| {finSupp}_{W} (x)\} \to g \in (D^{C})$
18		elmapi	$⊢ g \in (D^{C}) \to g : C ⟶ D$
19	17 18	syl	$⊢ g \in \{x \in (D^{C}) \| {finSupp}_{W} (x)\} \to g : C ⟶ D$
20	19 2	eleq2s	$⊢ g \in T \to g : C ⟶ D$
21	20	adantl	$⊢ (φ \land g \in T) \to g : C ⟶ D$
22		f1ocnv	$⊢ G : B \underset{1-1 onto}{⟶} D \to G^{-1} : D \underset{1-1 onto}{⟶} B$
23		f1of	$⊢ G^{-1} : D \underset{1-1 onto}{⟶} B \to G^{-1} : D ⟶ B$
24	5 22 23	3syl	$⊢ φ \to G^{-1} : D ⟶ B$
25	24	adantr	$⊢ (φ \land g \in T) \to G^{-1} : D ⟶ B$
26		ssidd	$⊢ (φ \land g \in T) \to D \subseteq D$
27	8	adantr	$⊢ (φ \land g \in T) \to C \in X$
28	9	adantr	$⊢ (φ \land g \in T) \to D \in Y$
29		breq1	$⊢ x = g \to ({finSupp}_{W} (x) \leftrightarrow {finSupp}_{W} (g))$
30	29	elrab	$⊢ g \in \{x \in (D^{C}) \| {finSupp}_{W} (x)\} \leftrightarrow (g \in (D^{C}) \land {finSupp}_{W} (g))$
31	30	simprbi	$⊢ g \in \{x \in (D^{C}) \| {finSupp}_{W} (x)\} \to {finSupp}_{W} (g)$
32	31 2	eleq2s	$⊢ g \in T \to {finSupp}_{W} (g)$
33	32	adantl	$⊢ (φ \land g \in T) \to {finSupp}_{W} (g)$
34	5 10	jca	$⊢ φ \to (G : B \underset{1-1 onto}{⟶} D \land Z \in B)$
35	3	eqcomi	$⊢ G (Z) = W$
36	34 35	jctir	$⊢ φ \to ((G : B \underset{1-1 onto}{⟶} D \land Z \in B) \land G (Z) = W)$
37	36	adantr	$⊢ (φ \land g \in T) \to ((G : B \underset{1-1 onto}{⟶} D \land Z \in B) \land G (Z) = W)$
38		f1ocnvfv	$⊢ (G : B \underset{1-1 onto}{⟶} D \land Z \in B) \to (G (Z) = W \to G^{-1} (W) = Z)$
39	38	imp	$⊢ ((G : B \underset{1-1 onto}{⟶} D \land Z \in B) \land G (Z) = W) \to G^{-1} (W) = Z$
40	37 39	syl	$⊢ (φ \land g \in T) \to G^{-1} (W) = Z$
41	11 16 21 25 26 27 28 33 40	fsuppcor	$⊢ (φ \land g \in T) \to {finSupp}_{Z} ((G^{-1} \circ g))$
42		f1ocnv	$⊢ F : C \underset{1-1 onto}{⟶} A \to F^{-1} : A \underset{1-1 onto}{⟶} C$
43		f1of1	$⊢ F^{-1} : A \underset{1-1 onto}{⟶} C \to F^{-1} : A \underset{1-1}{⟶} C$
44	4 42 43	3syl	$⊢ φ \to F^{-1} : A \underset{1-1}{⟶} C$
45	44	adantr	$⊢ (φ \land g \in T) \to F^{-1} : A \underset{1-1}{⟶} C$
46	13 7	jca	$⊢ φ \to (G : B ⟶ D \land B \in V)$
47		fex	$⊢ (G : B ⟶ D \land B \in V) \to G \in V$
48		cnvexg	$⊢ G \in V \to G^{-1} \in V$
49	46 47 48	3syl	$⊢ φ \to G^{-1} \in V$
50		coexg	$⊢ (G^{-1} \in V \land g \in T) \to G^{-1} \circ g \in V$
51	49 50	sylan	$⊢ (φ \land g \in T) \to G^{-1} \circ g \in V$
52	41 45 11 51	fsuppco	$⊢ (φ \land g \in T) \to {finSupp}_{Z} (((G^{-1} \circ g) \circ F^{-1}))$

Metamath Proof Explorer

Theorem mapfienlem2

Proof