fsuppssind

Description: Induction on functions F : A --> B with finite support (see fsuppind ) whose supports are subsets of S . (Contributed by SN, 15-Jun-2024)

	Ref	Expression
Hypotheses	fsuppssind.b	$⊢ B = {Base}_{G}$
	fsuppssind.z	$⊢ \underset{˙}{0} = 0_{G}$
	fsuppssind.p	$⊢ \underset{˙}{+} = +_{G}$
	fsuppssind.g	$⊢ φ \to G \in Grp$
	fsuppssind.v	$⊢ φ \to I \in V$
	fsuppssind.s	$⊢ φ \to S \subseteq I$
	fsuppssind.0	$⊢ φ \to I \times \{\underset{˙}{0}\} \in H$
	fsuppssind.1	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in I ⟼ if (s = a, b, \underset{˙}{0})) \in H$
	fsuppssind.2	$⊢ (φ \land (x \in H \land y \in H)) \to x {\underset{˙}{+}}_{f} y \in H$
	fsuppssind.3	$⊢ φ \to X : I ⟶ B$
	fsuppssind.4	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (X)$
	fsuppssind.5	$⊢ φ \to X supp \underset{˙}{0} \subseteq S$
Assertion	fsuppssind	$⊢ φ \to X \in H$

Proof

Step	Hyp	Ref	Expression
1		fsuppssind.b	$⊢ B = {Base}_{G}$
2		fsuppssind.z	$⊢ \underset{˙}{0} = 0_{G}$
3		fsuppssind.p	$⊢ \underset{˙}{+} = +_{G}$
4		fsuppssind.g	$⊢ φ \to G \in Grp$
5		fsuppssind.v	$⊢ φ \to I \in V$
6		fsuppssind.s	$⊢ φ \to S \subseteq I$
7		fsuppssind.0	$⊢ φ \to I \times \{\underset{˙}{0}\} \in H$
8		fsuppssind.1	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in I ⟼ if (s = a, b, \underset{˙}{0})) \in H$
9		fsuppssind.2	$⊢ (φ \land (x \in H \land y \in H)) \to x {\underset{˙}{+}}_{f} y \in H$
10		fsuppssind.3	$⊢ φ \to X : I ⟶ B$
11		fsuppssind.4	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (X)$
12		fsuppssind.5	$⊢ φ \to X supp \underset{˙}{0} \subseteq S$
13	10 6	fssresd	$⊢ φ \to ({X ↾}_{S}) : S ⟶ B$
14	2	fvexi	$⊢ \underset{˙}{0} \in V$
15	14	a1i	$⊢ φ \to \underset{˙}{0} \in V$
16	11 15	fsuppres	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (({X ↾}_{S}))$
17	13 16	jca	$⊢ φ \to (({X ↾}_{S}) : S ⟶ B \land {finSupp}_{\underset{˙}{0}} (({X ↾}_{S})))$
18	5 6	ssexd	$⊢ φ \to S \in V$
19	1 2	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in B$
20	4 19	syl	$⊢ φ \to \underset{˙}{0} \in B$
21		fconst6g	$⊢ \underset{˙}{0} \in B \to (S \times \{\underset{˙}{0}\}) : S ⟶ B$
22	20 21	syl	$⊢ φ \to (S \times \{\underset{˙}{0}\}) : S ⟶ B$
23		xpundir	$⊢ (S \cup (I ∖ S)) \times \{\underset{˙}{0}\} = (S \times \{\underset{˙}{0}\}) \cup ((I ∖ S) \times \{\underset{˙}{0}\})$
24		undif	$⊢ S \subseteq I \leftrightarrow S \cup (I ∖ S) = I$
25	6 24	sylib	$⊢ φ \to S \cup (I ∖ S) = I$
26	25	xpeq1d	$⊢ φ \to (S \cup (I ∖ S)) \times \{\underset{˙}{0}\} = I \times \{\underset{˙}{0}\}$
27	23 26	eqtr3id	$⊢ φ \to (S \times \{\underset{˙}{0}\}) \cup ((I ∖ S) \times \{\underset{˙}{0}\}) = I \times \{\underset{˙}{0}\}$
28	27 7	eqeltrd	$⊢ φ \to (S \times \{\underset{˙}{0}\}) \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H$
29	1	fvexi	$⊢ B \in V$
30	29	a1i	$⊢ φ \to B \in V$
31	30 5 6	fsuppssindlem2	$⊢ φ \to (S \times \{\underset{˙}{0}\} \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \leftrightarrow ((S \times \{\underset{˙}{0}\}) : S ⟶ B \land (S \times \{\underset{˙}{0}\}) \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))$
32	22 28 31	mpbir2and	$⊢ φ \to S \times \{\underset{˙}{0}\} \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\}$
33		simplrr	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in S) \to b \in B$
34	20	ad2antrr	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in S) \to \underset{˙}{0} \in B$
35	33 34	ifcld	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in S) \to if (s = a, b, \underset{˙}{0}) \in B$
36	35	fmpttd	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in S ⟼ if (s = a, b, \underset{˙}{0})) : S ⟶ B$
37		fconstmpt	$⊢ (I ∖ S) \times \{\underset{˙}{0}\} = (s \in (I ∖ S) ⟼ \underset{˙}{0})$
38	37	uneq2i	$⊢ (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \cup ((I ∖ S) \times \{\underset{˙}{0}\}) = (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \cup (s \in (I ∖ S) ⟼ \underset{˙}{0})$
39		eldifn	$⊢ s \in (I ∖ S) \to \neg s \in S$
40		eleq1a	$⊢ a \in S \to (s = a \to s \in S)$
41	40	con3dimp	$⊢ (a \in S \land \neg s \in S) \to \neg s = a$
42	41	adantlr	$⊢ ((a \in S \land b \in B) \land \neg s \in S) \to \neg s = a$
43	42	adantll	$⊢ ((φ \land (a \in S \land b \in B)) \land \neg s \in S) \to \neg s = a$
44	39 43	sylan2	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in (I ∖ S)) \to \neg s = a$
45	44	iffalsed	$⊢ ((φ \land (a \in S \land b \in B)) \land s \in (I ∖ S)) \to if (s = a, b, \underset{˙}{0}) = \underset{˙}{0}$
46	45	mpteq2dva	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in (I ∖ S) ⟼ if (s = a, b, \underset{˙}{0})) = (s \in (I ∖ S) ⟼ \underset{˙}{0})$
47	46	uneq2d	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \cup (s \in (I ∖ S) ⟼ if (s = a, b, \underset{˙}{0})) = (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \cup (s \in (I ∖ S) ⟼ \underset{˙}{0})$
48		mptun	$⊢ (s \in (S \cup (I ∖ S)) ⟼ if (s = a, b, \underset{˙}{0})) = (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \cup (s \in (I ∖ S) ⟼ if (s = a, b, \underset{˙}{0}))$
49	6	adantr	$⊢ (φ \land (a \in S \land b \in B)) \to S \subseteq I$
50	49 24	sylib	$⊢ (φ \land (a \in S \land b \in B)) \to S \cup (I ∖ S) = I$
51	50	mpteq1d	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in (S \cup (I ∖ S)) ⟼ if (s = a, b, \underset{˙}{0})) = (s \in I ⟼ if (s = a, b, \underset{˙}{0}))$
52	48 51	eqtr3id	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \cup (s \in (I ∖ S) ⟼ if (s = a, b, \underset{˙}{0})) = (s \in I ⟼ if (s = a, b, \underset{˙}{0}))$
53	47 52	eqtr3d	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \cup (s \in (I ∖ S) ⟼ \underset{˙}{0}) = (s \in I ⟼ if (s = a, b, \underset{˙}{0}))$
54	38 53	syl5eq	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \cup ((I ∖ S) \times \{\underset{˙}{0}\}) = (s \in I ⟼ if (s = a, b, \underset{˙}{0}))$
55	54 8	eqeltrd	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H$
56	29	a1i	$⊢ (φ \land (a \in S \land b \in B)) \to B \in V$
57	5	adantr	$⊢ (φ \land (a \in S \land b \in B)) \to I \in V$
58	56 57 49	fsuppssindlem2	$⊢ (φ \land (a \in S \land b \in B)) \to ((s \in S ⟼ if (s = a, b, \underset{˙}{0})) \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \leftrightarrow ((s \in S ⟼ if (s = a, b, \underset{˙}{0})) : S ⟶ B \land (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))$
59	36 55 58	mpbir2and	$⊢ (φ \land (a \in S \land b \in B)) \to (s \in S ⟼ if (s = a, b, \underset{˙}{0})) \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\}$
60	30 5 6	fsuppssindlem2	$⊢ φ \to (s \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \leftrightarrow (s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))$
61	30 5 6	fsuppssindlem2	$⊢ φ \to (t \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \leftrightarrow (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))$
62	60 61	anbi12d	$⊢ φ \to ((s \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \land t \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\}) \leftrightarrow ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H)))$
63	1 3	grpcl	$⊢ (G \in Grp \land u \in B \land v \in B) \to u \underset{˙}{+} v \in B$
64	4 63	syl3an1	$⊢ (φ \land u \in B \land v \in B) \to u \underset{˙}{+} v \in B$
65	64	3expb	$⊢ (φ \land (u \in B \land v \in B)) \to u \underset{˙}{+} v \in B$
66	65	adantlr	$⊢ ((φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \land (u \in B \land v \in B)) \to u \underset{˙}{+} v \in B$
67		simprll	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to s : S ⟶ B$
68		simprrl	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to t : S ⟶ B$
69	18	adantr	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to S \in V$
70		inidm	$⊢ S \cap S = S$
71	66 67 68 69 69 70	off	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to (s {\underset{˙}{+}}_{f} t) : S ⟶ B$
72	67	ffnd	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to s Fn S$
73	68	ffnd	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to t Fn S$
74		fnconstg	$⊢ \underset{˙}{0} \in V \to ((I ∖ S) \times \{\underset{˙}{0}\}) Fn (I ∖ S)$
75	14 74	mp1i	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to ((I ∖ S) \times \{\underset{˙}{0}\}) Fn (I ∖ S)$
76	5	difexd	$⊢ φ \to I ∖ S \in V$
77	76	adantr	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to I ∖ S \in V$
78		disjdif	$⊢ S \cap (I ∖ S) = \emptyset$
79	78	a1i	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to S \cap (I ∖ S) = \emptyset$
80	72 73 75 75 69 77 79	ofun	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to (s \cup ((I ∖ S) \times \{\underset{˙}{0}\})) {\underset{˙}{+}}_{f} (t \cup ((I ∖ S) \times \{\underset{˙}{0}\})) = (s {\underset{˙}{+}}_{f} t) \cup (((I ∖ S) \times \{\underset{˙}{0}\}) {\underset{˙}{+}}_{f} ((I ∖ S) \times \{\underset{˙}{0}\}))$
81	14 74	mp1i	$⊢ φ \to ((I ∖ S) \times \{\underset{˙}{0}\}) Fn (I ∖ S)$
82		fvconst2g	$⊢ (\underset{˙}{0} \in V \land j \in (I ∖ S)) \to ((I ∖ S) \times \{\underset{˙}{0}\}) (j) = \underset{˙}{0}$
83	15 82	sylan	$⊢ (φ \land j \in (I ∖ S)) \to ((I ∖ S) \times \{\underset{˙}{0}\}) (j) = \underset{˙}{0}$
84	1 3 2	grplid	$⊢ (G \in Grp \land \underset{˙}{0} \in B) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
85	4 20 84	syl2anc	$⊢ φ \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
86	85	adantr	$⊢ (φ \land j \in (I ∖ S)) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
87	14	a1i	$⊢ (φ \land j \in (I ∖ S)) \to \underset{˙}{0} \in V$
88	87 82	sylancom	$⊢ (φ \land j \in (I ∖ S)) \to ((I ∖ S) \times \{\underset{˙}{0}\}) (j) = \underset{˙}{0}$
89	86 88	eqtr4d	$⊢ (φ \land j \in (I ∖ S)) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = ((I ∖ S) \times \{\underset{˙}{0}\}) (j)$
90	76 81 81 81 83 83 89	offveq	$⊢ φ \to ((I ∖ S) \times \{\underset{˙}{0}\}) {\underset{˙}{+}}_{f} ((I ∖ S) \times \{\underset{˙}{0}\}) = (I ∖ S) \times \{\underset{˙}{0}\}$
91	90	uneq2d	$⊢ φ \to (s {\underset{˙}{+}}_{f} t) \cup (((I ∖ S) \times \{\underset{˙}{0}\}) {\underset{˙}{+}}_{f} ((I ∖ S) \times \{\underset{˙}{0}\})) = (s {\underset{˙}{+}}_{f} t) \cup ((I ∖ S) \times \{\underset{˙}{0}\})$
92	91	adantr	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to (s {\underset{˙}{+}}_{f} t) \cup (((I ∖ S) \times \{\underset{˙}{0}\}) {\underset{˙}{+}}_{f} ((I ∖ S) \times \{\underset{˙}{0}\})) = (s {\underset{˙}{+}}_{f} t) \cup ((I ∖ S) \times \{\underset{˙}{0}\})$
93	80 92	eqtrd	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to (s \cup ((I ∖ S) \times \{\underset{˙}{0}\})) {\underset{˙}{+}}_{f} (t \cup ((I ∖ S) \times \{\underset{˙}{0}\})) = (s {\underset{˙}{+}}_{f} t) \cup ((I ∖ S) \times \{\underset{˙}{0}\})$
94	9	caovclg	$⊢ (φ \land (s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H)) \to (s \cup ((I ∖ S) \times \{\underset{˙}{0}\})) {\underset{˙}{+}}_{f} (t \cup ((I ∖ S) \times \{\underset{˙}{0}\})) \in H$
95	94	adantrrl	$⊢ (φ \land (s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to (s \cup ((I ∖ S) \times \{\underset{˙}{0}\})) {\underset{˙}{+}}_{f} (t \cup ((I ∖ S) \times \{\underset{˙}{0}\})) \in H$
96	95	adantrll	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to (s \cup ((I ∖ S) \times \{\underset{˙}{0}\})) {\underset{˙}{+}}_{f} (t \cup ((I ∖ S) \times \{\underset{˙}{0}\})) \in H$
97	93 96	eqeltrrd	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to (s {\underset{˙}{+}}_{f} t) \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H$
98	30 5 6	fsuppssindlem2	$⊢ φ \to (s {\underset{˙}{+}}_{f} t \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \leftrightarrow ((s {\underset{˙}{+}}_{f} t) : S ⟶ B \land (s {\underset{˙}{+}}_{f} t) \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))$
99	98	adantr	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to (s {\underset{˙}{+}}_{f} t \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \leftrightarrow ((s {\underset{˙}{+}}_{f} t) : S ⟶ B \land (s {\underset{˙}{+}}_{f} t) \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))$
100	71 97 99	mpbir2and	$⊢ (φ \land ((s : S ⟶ B \land s \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H) \land (t : S ⟶ B \land t \cup ((I ∖ S) \times \{\underset{˙}{0}\}) \in H))) \to s {\underset{˙}{+}}_{f} t \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\}$
101	62 100	sylbida	$⊢ (φ \land (s \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \land t \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\})) \to s {\underset{˙}{+}}_{f} t \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\}$
102	1 2 3 4 18 32 59 101	fsuppind	$⊢ (φ \land (({X ↾}_{S}) : S ⟶ B \land {finSupp}_{\underset{˙}{0}} (({X ↾}_{S})))) \to {X ↾}_{S} \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\}$
103	17 102	mpdan	$⊢ φ \to {X ↾}_{S} \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\}$
104	30 18	elmapd	$⊢ φ \to ({X ↾}_{S} \in (B^{S}) \leftrightarrow ({X ↾}_{S}) : S ⟶ B)$
105	13 104	mpbird	$⊢ φ \to {X ↾}_{S} \in (B^{S})$
106		fveq1	$⊢ f = {X ↾}_{S} \to f (i) = ({X ↾}_{S}) (i)$
107	106	ifeq1d	$⊢ f = {X ↾}_{S} \to if (i \in S, f (i), \underset{˙}{0}) = if (i \in S, ({X ↾}_{S}) (i), \underset{˙}{0})$
108	107	mpteq2dv	$⊢ f = {X ↾}_{S} \to (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) = (i \in I ⟼ if (i \in S, ({X ↾}_{S}) (i), \underset{˙}{0}))$
109	108	eleq1d	$⊢ f = {X ↾}_{S} \to ((i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H \leftrightarrow (i \in I ⟼ if (i \in S, ({X ↾}_{S}) (i), \underset{˙}{0})) \in H)$
110	109	elrab3	$⊢ {X ↾}_{S} \in (B^{S}) \to ({X ↾}_{S} \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \leftrightarrow (i \in I ⟼ if (i \in S, ({X ↾}_{S}) (i), \underset{˙}{0})) \in H)$
111	105 110	syl	$⊢ φ \to ({X ↾}_{S} \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \leftrightarrow (i \in I ⟼ if (i \in S, ({X ↾}_{S}) (i), \underset{˙}{0})) \in H)$
112	15 5 10 12	fsuppssindlem1	$⊢ φ \to X = (i \in I ⟼ if (i \in S, ({X ↾}_{S}) (i), \underset{˙}{0}))$
113	112	eleq1d	$⊢ φ \to (X \in H \leftrightarrow (i \in I ⟼ if (i \in S, ({X ↾}_{S}) (i), \underset{˙}{0})) \in H)$
114	111 113	bitr4d	$⊢ φ \to ({X ↾}_{S} \in \{f \in (B^{S}) \| (i \in I ⟼ if (i \in S, f (i), \underset{˙}{0})) \in H\} \leftrightarrow X \in H)$
115	103 114	mpbid	$⊢ φ \to X \in H$

Metamath Proof Explorer

Theorem fsuppssind

Proof