Theorem psrbagev1OLD

Description: Obsolete version of psrbagev1 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 18-Jul-2019) (Revised by AV, 11-Apr-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	psrbagev1.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	psrbagev1.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
	psrbagev1.x	⊢ · = ( .g ‘ 𝑇 )
	psrbagev1.z	⊢ 0 = ( 0g ‘ 𝑇 )
	psrbagev1.t	⊢ ( 𝜑 → 𝑇 ∈ CMnd )
	psrbagev1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	psrbagev1.g	⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
	psrbagev1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
Assertion	psrbagev1OLD	⊢ ( 𝜑 → ( ( 𝐵 ∘f · 𝐺 ) : 𝐼 ⟶ 𝐶 ∧ ( 𝐵 ∘f · 𝐺 ) finSupp 0 ) )

Proof

Step	Hyp	Ref	Expression
1		psrbagev1.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2		psrbagev1.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
3		psrbagev1.x	⊢ · = ( .g ‘ 𝑇 )
4		psrbagev1.z	⊢ 0 = ( 0g ‘ 𝑇 )
5		psrbagev1.t	⊢ ( 𝜑 → 𝑇 ∈ CMnd )
6		psrbagev1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
7		psrbagev1.g	⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
8		psrbagev1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
9	5	cmnmndd	⊢ ( 𝜑 → 𝑇 ∈ Mnd )
10	2 3	mulgnn0cl	⊢ ( ( 𝑇 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 · 𝑧 ) ∈ 𝐶 )
11	10	3expb	⊢ ( ( 𝑇 ∈ Mnd ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝐶 )
12	9 11	sylan	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝐶 )
13	1	psrbagfOLD	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝐵 ∈ 𝐷 ) → 𝐵 : 𝐼 ⟶ ℕ0 )
14	8 6 13	syl2anc	⊢ ( 𝜑 → 𝐵 : 𝐼 ⟶ ℕ0 )
15		inidm	⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
16	12 14 7 8 8 15	off	⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) : 𝐼 ⟶ 𝐶 )
17		ovexd	⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) ∈ V )
18	14	ffnd	⊢ ( 𝜑 → 𝐵 Fn 𝐼 )
19	7	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐼 )
20	18 19 8 8	offun	⊢ ( 𝜑 → Fun ( 𝐵 ∘f · 𝐺 ) )
21	4	fvexi	⊢ 0 ∈ V
22	21	a1i	⊢ ( 𝜑 → 0 ∈ V )
23	1	psrbagfsuppOLD	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝐼 ∈ 𝑊 ) → 𝐵 finSupp 0 )
24	6 8 23	syl2anc	⊢ ( 𝜑 → 𝐵 finSupp 0 )
25	24	fsuppimpd	⊢ ( 𝜑 → ( 𝐵 supp 0 ) ∈ Fin )
26		ssidd	⊢ ( 𝜑 → ( 𝐵 supp 0 ) ⊆ ( 𝐵 supp 0 ) )
27	2 4 3	mulg0	⊢ ( 𝑧 ∈ 𝐶 → ( 0 · 𝑧 ) = 0 )
28	27	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( 0 · 𝑧 ) = 0 )
29		c0ex	⊢ 0 ∈ V
30	29	a1i	⊢ ( 𝜑 → 0 ∈ V )
31	26 28 14 7 8 30	suppssof1	⊢ ( 𝜑 → ( ( 𝐵 ∘f · 𝐺 ) supp 0 ) ⊆ ( 𝐵 supp 0 ) )
32		suppssfifsupp	⊢ ( ( ( ( 𝐵 ∘f · 𝐺 ) ∈ V ∧ Fun ( 𝐵 ∘f · 𝐺 ) ∧ 0 ∈ V ) ∧ ( ( 𝐵 supp 0 ) ∈ Fin ∧ ( ( 𝐵 ∘f · 𝐺 ) supp 0 ) ⊆ ( 𝐵 supp 0 ) ) ) → ( 𝐵 ∘f · 𝐺 ) finSupp 0 )
33	17 20 22 25 31 32	syl32anc	⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) finSupp 0 )
34	16 33	jca	⊢ ( 𝜑 → ( ( 𝐵 ∘f · 𝐺 ) : 𝐼 ⟶ 𝐶 ∧ ( 𝐵 ∘f · 𝐺 ) finSupp 0 ) )