mapfienlem1

Description: Lemma 1 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	mapfienlem1	$⊢ (φ \land f \in S) \to {finSupp}_{W} ((G \circ (f \circ F)))$

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	3	fvexi	$⊢ W \in V$
12	11	a1i	$⊢ (φ \land f \in S) \to W \in V$
13	10	adantr	$⊢ (φ \land f \in S) \to Z \in B$
14		elrabi	$⊢ f \in \{x \in (B^{A}) \| {finSupp}_{Z} (x)\} \to f \in (B^{A})$
15		elmapi	$⊢ f \in (B^{A}) \to f : A ⟶ B$
16	14 15	syl	$⊢ f \in \{x \in (B^{A}) \| {finSupp}_{Z} (x)\} \to f : A ⟶ B$
17	16 1	eleq2s	$⊢ f \in S \to f : A ⟶ B$
18		f1of	$⊢ F : C \underset{1-1 onto}{⟶} A \to F : C ⟶ A$
19	4 18	syl	$⊢ φ \to F : C ⟶ A$
20		fco	$⊢ (f : A ⟶ B \land F : C ⟶ A) \to (f \circ F) : C ⟶ B$
21	17 19 20	syl2anr	$⊢ (φ \land f \in S) \to (f \circ F) : C ⟶ B$
22		f1of	$⊢ G : B \underset{1-1 onto}{⟶} D \to G : B ⟶ D$
23	5 22	syl	$⊢ φ \to G : B ⟶ D$
24	23	adantr	$⊢ (φ \land f \in S) \to G : B ⟶ D$
25		ssidd	$⊢ (φ \land f \in S) \to B \subseteq B$
26	8	adantr	$⊢ (φ \land f \in S) \to C \in X$
27	7	adantr	$⊢ (φ \land f \in S) \to B \in V$
28		breq1	$⊢ x = f \to ({finSupp}_{Z} (x) \leftrightarrow {finSupp}_{Z} (f))$
29	28 1	elrab2	$⊢ f \in S \leftrightarrow (f \in (B^{A}) \land {finSupp}_{Z} (f))$
30	29	simprbi	$⊢ f \in S \to {finSupp}_{Z} (f)$
31	30	adantl	$⊢ (φ \land f \in S) \to {finSupp}_{Z} (f)$
32		f1of1	$⊢ F : C \underset{1-1 onto}{⟶} A \to F : C \underset{1-1}{⟶} A$
33	4 32	syl	$⊢ φ \to F : C \underset{1-1}{⟶} A$
34	33	adantr	$⊢ (φ \land f \in S) \to F : C \underset{1-1}{⟶} A$
35		simpr	$⊢ (φ \land f \in S) \to f \in S$
36	31 34 13 35	fsuppco	$⊢ (φ \land f \in S) \to {finSupp}_{Z} ((f \circ F))$
37	3	eqcomi	$⊢ G (Z) = W$
38	37	a1i	$⊢ (φ \land f \in S) \to G (Z) = W$
39	12 13 21 24 25 26 27 36 38	fsuppcor	$⊢ (φ \land f \in S) \to {finSupp}_{W} ((G \circ (f \circ F)))$

Metamath Proof Explorer

Theorem mapfienlem1

Proof