Metamath Proof Explorer

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 ) )