Theorem psrbagev2OLD

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

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

Proof

Step	Hyp	Ref	Expression
1		psrbagev2.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2		psrbagev2.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
3		psrbagev2.x	⊢ · = ( .g ‘ 𝑇 )
4		psrbagev2.t	⊢ ( 𝜑 → 𝑇 ∈ CMnd )
5		psrbagev2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
6		psrbagev2.g	⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
7		psrbagev2OLD.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
8		eqid	⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
9	1 2 3 8 4 5 6 7	psrbagev1OLD	⊢ ( 𝜑 → ( ( 𝐵 ∘f · 𝐺 ) : 𝐼 ⟶ 𝐶 ∧ ( 𝐵 ∘f · 𝐺 ) finSupp ( 0g ‘ 𝑇 ) ) )
10	9	simpld	⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) : 𝐼 ⟶ 𝐶 )
11	9	simprd	⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) finSupp ( 0g ‘ 𝑇 ) )
12	2 8 4 7 10 11	gsumcl	⊢ ( 𝜑 → ( 𝑇 Σg ( 𝐵 ∘f · 𝐺 ) ) ∈ 𝐶 )