Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
fsuppssind.z ⊢ 0 = ( 0g ‘ 𝐺 )
fsuppssind.p ⊢ + = ( +g ‘ 𝐺 )
fsuppssind.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
fsuppssind.v ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
fsuppssind.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐼 )
fsuppssind.0 ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ 𝐻 )
fsuppssind.1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐼 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 )
fsuppssind.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ∘f + 𝑦 ) ∈ 𝐻 )
fsuppssind.3 ⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ 𝐵 )
fsuppssind.4 ⊢ ( 𝜑 → 𝑋 finSupp 0 )
fsuppssind.5 ⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ 𝑆 )
Assertion fsuppssind ( 𝜑 → 𝑋 ∈ 𝐻 )

Proof

Step Hyp Ref Expression
1 fsuppssind.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 fsuppssind.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 fsuppssind.p ⊢ + = ( +g ‘ 𝐺 )
4 fsuppssind.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
5 fsuppssind.v ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 fsuppssind.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐼 )
7 fsuppssind.0 ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ 𝐻 )
8 fsuppssind.1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐼 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 )
9 fsuppssind.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ∘f + 𝑦 ) ∈ 𝐻 )
10 fsuppssind.3 ⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ 𝐵 )
11 fsuppssind.4 ⊢ ( 𝜑 → 𝑋 finSupp 0 )
12 fsuppssind.5 ⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ 𝑆 )
13 10 6 fssresd ⊢ ( 𝜑 → ( 𝑋 ↾ 𝑆 ) : 𝑆 ⟶ 𝐵 )
14 2 fvexi ⊢ 0 ∈ V
15 14 a1i ⊢ ( 𝜑 → 0 ∈ V )
16 11 15 fsuppres ⊢ ( 𝜑 → ( 𝑋 ↾ 𝑆 ) finSupp 0 )
17 13 16 jca ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑆 ) : 𝑆 ⟶ 𝐵 ∧ ( 𝑋 ↾ 𝑆 ) finSupp 0 ) )
18 5 6 ssexd ⊢ ( 𝜑 → 𝑆 ∈ V )
19 1 2 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
20 4 19 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
21 fconst6g ⊢ ( 0 ∈ 𝐵 → ( 𝑆 × { 0 } ) : 𝑆 ⟶ 𝐵 )
22 20 21 syl ⊢ ( 𝜑 → ( 𝑆 × { 0 } ) : 𝑆 ⟶ 𝐵 )
23 xpundir ⊢ ( ( 𝑆 ∪ ( 𝐼 ∖ 𝑆 ) ) × { 0 } ) = ( ( 𝑆 × { 0 } ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) )
24 undif ⊢ ( 𝑆 ⊆ 𝐼 ↔ ( 𝑆 ∪ ( 𝐼 ∖ 𝑆 ) ) = 𝐼 )
25 6 24 sylib ⊢ ( 𝜑 → ( 𝑆 ∪ ( 𝐼 ∖ 𝑆 ) ) = 𝐼 )
26 25 xpeq1d ⊢ ( 𝜑 → ( ( 𝑆 ∪ ( 𝐼 ∖ 𝑆 ) ) × { 0 } ) = ( 𝐼 × { 0 } ) )
27 23 26 eqtr3id ⊢ ( 𝜑 → ( ( 𝑆 × { 0 } ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) = ( 𝐼 × { 0 } ) )
28 27 7 eqeltrd ⊢ ( 𝜑 → ( ( 𝑆 × { 0 } ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 )
29 1 fvexi ⊢ 𝐵 ∈ V
30 29 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
31 30 5 6 fsuppssindlem2 ⊢ ( 𝜑 → ( ( 𝑆 × { 0 } ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ↔ ( ( 𝑆 × { 0 } ) : 𝑆 ⟶ 𝐵 ∧ ( ( 𝑆 × { 0 } ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )
32 22 28 31 mpbir2and ⊢ ( 𝜑 → ( 𝑆 × { 0 } ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } )
33 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ 𝑆 ) → 𝑏 ∈ 𝐵 )
34 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ 𝑆 ) → 0 ∈ 𝐵 )
35 33 34 ifcld ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ 𝑆 ) → if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ∈ 𝐵 )
36 35 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) : 𝑆 ⟶ 𝐵 )
37 fconstmpt ⊢ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) = ( 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ↦ 0 )
38 37 uneq2i ⊢ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) = ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∪ ( 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ↦ 0 ) )
39 eldifn ⊢ ( 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) → ¬ 𝑠 ∈ 𝑆 )
40 eleq1a ⊢ ( 𝑎 ∈ 𝑆 → ( 𝑠 = 𝑎 → 𝑠 ∈ 𝑆 ) )
41 40 con3dimp ⊢ ( ( 𝑎 ∈ 𝑆 ∧ ¬ 𝑠 ∈ 𝑆 ) → ¬ 𝑠 = 𝑎 )
42 41 adantlr ⊢ ( ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ∧ ¬ 𝑠 ∈ 𝑆 ) → ¬ 𝑠 = 𝑎 )
43 42 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ¬ 𝑠 ∈ 𝑆 ) → ¬ 𝑠 = 𝑎 )
44 39 43 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ) → ¬ 𝑠 = 𝑎 )
45 44 iffalsed ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ) → if ( 𝑠 = 𝑎 , 𝑏 , 0 ) = 0 )
46 45 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) = ( 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ↦ 0 ) )
47 46 uneq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∪ ( 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ) = ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∪ ( 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ↦ 0 ) ) )
48 mptun ⊢ ( 𝑠 ∈ ( 𝑆 ∪ ( 𝐼 ∖ 𝑆 ) ) ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) = ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∪ ( 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) )
49 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑆 ⊆ 𝐼 )
50 49 24 sylib ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑆 ∪ ( 𝐼 ∖ 𝑆 ) ) = 𝐼 )
51 50 mpteq1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ ( 𝑆 ∪ ( 𝐼 ∖ 𝑆 ) ) ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) = ( 𝑠 ∈ 𝐼 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) )
52 48 51 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∪ ( 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ) = ( 𝑠 ∈ 𝐼 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) )
53 47 52 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∪ ( 𝑠 ∈ ( 𝐼 ∖ 𝑆 ) ↦ 0 ) ) = ( 𝑠 ∈ 𝐼 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) )
54 38 53 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) = ( 𝑠 ∈ 𝐼 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) )
55 54 8 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 )
56 29 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐵 ∈ V )
57 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑉 )
58 56 57 49 fsuppssindlem2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ↔ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) : 𝑆 ⟶ 𝐵 ∧ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )
59 36 55 58 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } )
60 30 5 6 fsuppssindlem2 ⊢ ( 𝜑 → ( 𝑠 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ↔ ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )
61 30 5 6 fsuppssindlem2 ⊢ ( 𝜑 → ( 𝑡 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ↔ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )
62 60 61 anbi12d ⊢ ( 𝜑 → ( ( 𝑠 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ∧ 𝑡 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ) ↔ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) )
63 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 + 𝑣 ) ∈ 𝐵 )
64 4 63 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 + 𝑣 ) ∈ 𝐵 )
65 64 3expb ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 + 𝑣 ) ∈ 𝐵 )
66 65 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( 𝑢 + 𝑣 ) ∈ 𝐵 )
67 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → 𝑠 : 𝑆 ⟶ 𝐵 )
68 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → 𝑡 : 𝑆 ⟶ 𝐵 )
69 18 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → 𝑆 ∈ V )
70 inidm ⊢ ( 𝑆 ∩ 𝑆 ) = 𝑆
71 66 67 68 69 69 70 off ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( 𝑠 ∘f + 𝑡 ) : 𝑆 ⟶ 𝐵 )
72 67 ffnd ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → 𝑠 Fn 𝑆 )
73 68 ffnd ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → 𝑡 Fn 𝑆 )
74 fnconstg ⊢ ( 0 ∈ V → ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) Fn ( 𝐼 ∖ 𝑆 ) )
75 14 74 mp1i ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) Fn ( 𝐼 ∖ 𝑆 ) )
76 5 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ 𝑆 ) ∈ V )
77 76 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( 𝐼 ∖ 𝑆 ) ∈ V )
78 disjdif ⊢ ( 𝑆 ∩ ( 𝐼 ∖ 𝑆 ) ) = ∅
79 78 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( 𝑆 ∩ ( 𝐼 ∖ 𝑆 ) ) = ∅ )
80 72 73 75 75 69 77 79 ofun ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∘f + ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ) = ( ( 𝑠 ∘f + 𝑡 ) ∪ ( ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ∘f + ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ) )
81 14 74 mp1i ⊢ ( 𝜑 → ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) Fn ( 𝐼 ∖ 𝑆 ) )
82 fvconst2g ⊢ ( ( 0 ∈ V ∧ 𝑗 ∈ ( 𝐼 ∖ 𝑆 ) ) → ( ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ‘ 𝑗 ) = 0 )
83 15 82 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐼 ∖ 𝑆 ) ) → ( ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ‘ 𝑗 ) = 0 )
84 1 3 2 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 0 ∈ 𝐵 ) → ( 0 + 0 ) = 0 )
85 4 20 84 syl2anc ⊢ ( 𝜑 → ( 0 + 0 ) = 0 )
86 85 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐼 ∖ 𝑆 ) ) → ( 0 + 0 ) = 0 )
87 14 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐼 ∖ 𝑆 ) ) → 0 ∈ V )
88 87 82 sylancom ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐼 ∖ 𝑆 ) ) → ( ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ‘ 𝑗 ) = 0 )
89 86 88 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐼 ∖ 𝑆 ) ) → ( 0 + 0 ) = ( ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ‘ 𝑗 ) )
90 76 81 81 81 83 83 89 offveq ⊢ ( 𝜑 → ( ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ∘f + ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) = ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) )
91 90 uneq2d ⊢ ( 𝜑 → ( ( 𝑠 ∘f + 𝑡 ) ∪ ( ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ∘f + ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ) = ( ( 𝑠 ∘f + 𝑡 ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) )
92 91 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( ( 𝑠 ∘f + 𝑡 ) ∪ ( ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ∘f + ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ) = ( ( 𝑠 ∘f + 𝑡 ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) )
93 80 92 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∘f + ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ) = ( ( 𝑠 ∘f + 𝑡 ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) )
94 9 caovclg ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) → ( ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∘f + ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ) ∈ 𝐻 )
95 94 adantrrl ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∘f + ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ) ∈ 𝐻 )
96 95 adantrll ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∘f + ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ) ∈ 𝐻 )
97 93 96 eqeltrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( ( 𝑠 ∘f + 𝑡 ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 )
98 30 5 6 fsuppssindlem2 ⊢ ( 𝜑 → ( ( 𝑠 ∘f + 𝑡 ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ↔ ( ( 𝑠 ∘f + 𝑡 ) : 𝑆 ⟶ 𝐵 ∧ ( ( 𝑠 ∘f + 𝑡 ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )
99 98 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( ( 𝑠 ∘f + 𝑡 ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ↔ ( ( 𝑠 ∘f + 𝑡 ) : 𝑆 ⟶ 𝐵 ∧ ( ( 𝑠 ∘f + 𝑡 ) ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) )
100 71 97 99 mpbir2and ⊢ ( ( 𝜑 ∧ ( ( 𝑠 : 𝑆 ⟶ 𝐵 ∧ ( 𝑠 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ∧ ( 𝑡 : 𝑆 ⟶ 𝐵 ∧ ( 𝑡 ∪ ( ( 𝐼 ∖ 𝑆 ) × { 0 } ) ) ∈ 𝐻 ) ) ) → ( 𝑠 ∘f + 𝑡 ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } )
101 62 100 sylibda ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ∧ 𝑡 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ) ) → ( 𝑠 ∘f + 𝑡 ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } )
102 1 2 3 4 18 32 59 101 fsuppind ⊢ ( ( 𝜑 ∧ ( ( 𝑋 ↾ 𝑆 ) : 𝑆 ⟶ 𝐵 ∧ ( 𝑋 ↾ 𝑆 ) finSupp 0 ) ) → ( 𝑋 ↾ 𝑆 ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } )
103 17 102 mpdan ⊢ ( 𝜑 → ( 𝑋 ↾ 𝑆 ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } )
104 30 18 elmapd ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑆 ) ∈ ( 𝐵 ↑m 𝑆 ) ↔ ( 𝑋 ↾ 𝑆 ) : 𝑆 ⟶ 𝐵 ) )
105 13 104 mpbird ⊢ ( 𝜑 → ( 𝑋 ↾ 𝑆 ) ∈ ( 𝐵 ↑m 𝑆 ) )
106 fveq1 ⊢ ( 𝑓 = ( 𝑋 ↾ 𝑆 ) → ( 𝑓 ‘ 𝑖 ) = ( ( 𝑋 ↾ 𝑆 ) ‘ 𝑖 ) )
107 106 ifeq1d ⊢ ( 𝑓 = ( 𝑋 ↾ 𝑆 ) → if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) = if ( 𝑖 ∈ 𝑆 , ( ( 𝑋 ↾ 𝑆 ) ‘ 𝑖 ) , 0 ) )
108 107 mpteq2dv ⊢ ( 𝑓 = ( 𝑋 ↾ 𝑆 ) → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( ( 𝑋 ↾ 𝑆 ) ‘ 𝑖 ) , 0 ) ) )
109 108 eleq1d ⊢ ( 𝑓 = ( 𝑋 ↾ 𝑆 ) → ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 ↔ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( ( 𝑋 ↾ 𝑆 ) ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 ) )
110 109 elrab3 ⊢ ( ( 𝑋 ↾ 𝑆 ) ∈ ( 𝐵 ↑m 𝑆 ) → ( ( 𝑋 ↾ 𝑆 ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ↔ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( ( 𝑋 ↾ 𝑆 ) ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 ) )
111 105 110 syl ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑆 ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ↔ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( ( 𝑋 ↾ 𝑆 ) ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 ) )
112 15 5 10 12 fsuppssindlem1 ⊢ ( 𝜑 → 𝑋 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( ( 𝑋 ↾ 𝑆 ) ‘ 𝑖 ) , 0 ) ) )
113 112 eleq1d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐻 ↔ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( ( 𝑋 ↾ 𝑆 ) ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 ) )
114 111 113 bitr4d ⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑆 ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝑆 ) ∣ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑆 , ( 𝑓 ‘ 𝑖 ) , 0 ) ) ∈ 𝐻 } ↔ 𝑋 ∈ 𝐻 ) )
115 103 114 mpbid ⊢ ( 𝜑 → 𝑋 ∈ 𝐻 )