psrbagaddclOLD

Description: Obsolete version of psrbagaddcl as of 7-Aug-2024. (Contributed by Mario Carneiro, 9-Jan-2015) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	Assertion	psrbagaddclOLD	$⊢ (I \in V \land F \in D \land G \in D) \to F +_{f} G \in D$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		nn0addcl	$⊢ (x \in ℕ_{0} \land y \in ℕ_{0}) \to x + y \in ℕ_{0}$
3	2	adantl	$⊢ ((I \in V \land F \in D \land G \in D) \land (x \in ℕ_{0} \land y \in ℕ_{0})) \to x + y \in ℕ_{0}$
4		simp2	$⊢ (I \in V \land F \in D \land G \in D) \to F \in D$
5	1	psrbag	$⊢ I \in V \to (F \in D \leftrightarrow (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin))$
6	5	3ad2ant1	$⊢ (I \in V \land F \in D \land G \in D) \to (F \in D \leftrightarrow (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin))$
7	4 6	mpbid	$⊢ (I \in V \land F \in D \land G \in D) \to (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin)$
8	7	simpld	$⊢ (I \in V \land F \in D \land G \in D) \to F : I ⟶ ℕ_{0}$
9		simp3	$⊢ (I \in V \land F \in D \land G \in D) \to G \in D$
10	1	psrbag	$⊢ I \in V \to (G \in D \leftrightarrow (G : I ⟶ ℕ_{0} \land G^{-1} [ℕ] \in Fin))$
11	10	3ad2ant1	$⊢ (I \in V \land F \in D \land G \in D) \to (G \in D \leftrightarrow (G : I ⟶ ℕ_{0} \land G^{-1} [ℕ] \in Fin))$
12	9 11	mpbid	$⊢ (I \in V \land F \in D \land G \in D) \to (G : I ⟶ ℕ_{0} \land G^{-1} [ℕ] \in Fin)$
13	12	simpld	$⊢ (I \in V \land F \in D \land G \in D) \to G : I ⟶ ℕ_{0}$
14		simp1	$⊢ (I \in V \land F \in D \land G \in D) \to I \in V$
15		inidm	$⊢ I \cap I = I$
16	3 8 13 14 14 15	off	$⊢ (I \in V \land F \in D \land G \in D) \to (F +_{f} G) : I ⟶ ℕ_{0}$
17		fcdmnn0supp	$⊢ (I \in V \land (F +_{f} G) : I ⟶ ℕ_{0}) \to (F +_{f} G) supp 0 = {(F +_{f} G)}^{-1} [ℕ]$
18	14 16 17	syl2anc	$⊢ (I \in V \land F \in D \land G \in D) \to (F +_{f} G) supp 0 = {(F +_{f} G)}^{-1} [ℕ]$
19		fvexd	$⊢ ((I \in V \land F \in D \land G \in D) \land x \in I) \to F (x) \in V$
20		fvexd	$⊢ ((I \in V \land F \in D \land G \in D) \land x \in I) \to G (x) \in V$
21	8	feqmptd	$⊢ (I \in V \land F \in D \land G \in D) \to F = (x \in I ⟼ F (x))$
22	13	feqmptd	$⊢ (I \in V \land F \in D \land G \in D) \to G = (x \in I ⟼ G (x))$
23	14 19 20 21 22	offval2	$⊢ (I \in V \land F \in D \land G \in D) \to F +_{f} G = (x \in I ⟼ F (x) + G (x))$
24	23	oveq1d	$⊢ (I \in V \land F \in D \land G \in D) \to (F +_{f} G) supp 0 = (x \in I ⟼ F (x) + G (x)) supp 0$
25	18 24	eqtr3d	$⊢ (I \in V \land F \in D \land G \in D) \to {(F +_{f} G)}^{-1} [ℕ] = (x \in I ⟼ F (x) + G (x)) supp 0$
26		fcdmnn0supp	$⊢ (I \in V \land F : I ⟶ ℕ_{0}) \to F supp 0 = F^{-1} [ℕ]$
27	14 8 26	syl2anc	$⊢ (I \in V \land F \in D \land G \in D) \to F supp 0 = F^{-1} [ℕ]$
28	7	simprd	$⊢ (I \in V \land F \in D \land G \in D) \to F^{-1} [ℕ] \in Fin$
29	27 28	eqeltrd	$⊢ (I \in V \land F \in D \land G \in D) \to F supp 0 \in Fin$
30		fcdmnn0supp	$⊢ (I \in V \land G : I ⟶ ℕ_{0}) \to G supp 0 = G^{-1} [ℕ]$
31	14 13 30	syl2anc	$⊢ (I \in V \land F \in D \land G \in D) \to G supp 0 = G^{-1} [ℕ]$
32	12	simprd	$⊢ (I \in V \land F \in D \land G \in D) \to G^{-1} [ℕ] \in Fin$
33	31 32	eqeltrd	$⊢ (I \in V \land F \in D \land G \in D) \to G supp 0 \in Fin$
34		unfi	$⊢ (F supp 0 \in Fin \land G supp 0 \in Fin) \to {supp}_{0} (F) \cup {supp}_{0} (G) \in Fin$
35	29 33 34	syl2anc	$⊢ (I \in V \land F \in D \land G \in D) \to {supp}_{0} (F) \cup {supp}_{0} (G) \in Fin$
36		ssun1	$⊢ F supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$
37	36	a1i	$⊢ (I \in V \land F \in D \land G \in D) \to F supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$
38		c0ex	$⊢ 0 \in V$
39	38	a1i	$⊢ (I \in V \land F \in D \land G \in D) \to 0 \in V$
40	8 37 14 39	suppssr	$⊢ ((I \in V \land F \in D \land G \in D) \land x \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F (x) = 0$
41		ssun2	$⊢ G supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$
42	41	a1i	$⊢ (I \in V \land F \in D \land G \in D) \to G supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$
43	13 42 14 39	suppssr	$⊢ ((I \in V \land F \in D \land G \in D) \land x \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to G (x) = 0$
44	40 43	oveq12d	$⊢ ((I \in V \land F \in D \land G \in D) \land x \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F (x) + G (x) = 0 + 0$
45		00id	$⊢ 0 + 0 = 0$
46	44 45	eqtrdi	$⊢ ((I \in V \land F \in D \land G \in D) \land x \in (I ∖ ({supp}_{0} (F) \cup {supp}_{0} (G)))) \to F (x) + G (x) = 0$
47	46 14	suppss2	$⊢ (I \in V \land F \in D \land G \in D) \to (x \in I ⟼ F (x) + G (x)) supp 0 \subseteq {supp}_{0} (F) \cup {supp}_{0} (G)$
48	35 47	ssfid	$⊢ (I \in V \land F \in D \land G \in D) \to (x \in I ⟼ F (x) + G (x)) supp 0 \in Fin$
49	25 48	eqeltrd	$⊢ (I \in V \land F \in D \land G \in D) \to {(F +_{f} G)}^{-1} [ℕ] \in Fin$
50	1	psrbag	$⊢ I \in V \to (F +_{f} G \in D \leftrightarrow ((F +_{f} G) : I ⟶ ℕ_{0} \land {(F +_{f} G)}^{-1} [ℕ] \in Fin))$
51	50	3ad2ant1	$⊢ (I \in V \land F \in D \land G \in D) \to (F +_{f} G \in D \leftrightarrow ((F +_{f} G) : I ⟶ ℕ_{0} \land {(F +_{f} G)}^{-1} [ℕ] \in Fin))$
52	16 49 51	mpbir2and	$⊢ (I \in V \land F \in D \land G \in D) \to F +_{f} G \in D$

Metamath Proof Explorer

Theorem psrbagaddclOLD

Proof