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 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
psrbagev1.c 
|- C = ( Base ` T )
psrbagev1.x 
|- .x. = ( .g ` T )
psrbagev1.z 
|- .0. = ( 0g ` T )
psrbagev1.t 
|- ( ph -> T e. CMnd )
psrbagev1.b 
|- ( ph -> B e. D )
psrbagev1.g 
|- ( ph -> G : I --> C )
psrbagev1.i 
|- ( ph -> I e. W )
Assertion psrbagev1OLD 
|- ( ph -> ( ( B oF .x. G ) : I --> C /\ ( B oF .x. G ) finSupp .0. ) )

Proof

Step Hyp Ref Expression
1 psrbagev1.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
2 psrbagev1.c 
 |-  C = ( Base ` T )
3 psrbagev1.x 
 |-  .x. = ( .g ` T )
4 psrbagev1.z 
 |-  .0. = ( 0g ` T )
5 psrbagev1.t 
 |-  ( ph -> T e. CMnd )
6 psrbagev1.b 
 |-  ( ph -> B e. D )
7 psrbagev1.g 
 |-  ( ph -> G : I --> C )
8 psrbagev1.i 
 |-  ( ph -> I e. W )
9 5 cmnmndd 
 |-  ( ph -> T e. Mnd )
10 2 3 mulgnn0cl 
 |-  ( ( T e. Mnd /\ y e. NN0 /\ z e. C ) -> ( y .x. z ) e. C )
11 10 3expb 
 |-  ( ( T e. Mnd /\ ( y e. NN0 /\ z e. C ) ) -> ( y .x. z ) e. C )
12 9 11 sylan 
 |-  ( ( ph /\ ( y e. NN0 /\ z e. C ) ) -> ( y .x. z ) e. C )
13 1 psrbagfOLD 
 |-  ( ( I e. W /\ B e. D ) -> B : I --> NN0 )
14 8 6 13 syl2anc 
 |-  ( ph -> B : I --> NN0 )
15 inidm 
 |-  ( I i^i I ) = I
16 12 14 7 8 8 15 off 
 |-  ( ph -> ( B oF .x. G ) : I --> C )
17 ovexd 
 |-  ( ph -> ( B oF .x. G ) e. _V )
18 14 ffnd 
 |-  ( ph -> B Fn I )
19 7 ffnd 
 |-  ( ph -> G Fn I )
20 18 19 8 8 offun 
 |-  ( ph -> Fun ( B oF .x. G ) )
21 4 fvexi 
 |-  .0. e. _V
22 21 a1i 
 |-  ( ph -> .0. e. _V )
23 1 psrbagfsuppOLD 
 |-  ( ( B e. D /\ I e. W ) -> B finSupp 0 )
24 6 8 23 syl2anc 
 |-  ( ph -> B finSupp 0 )
25 24 fsuppimpd 
 |-  ( ph -> ( B supp 0 ) e. Fin )
26 ssidd 
 |-  ( ph -> ( B supp 0 ) C_ ( B supp 0 ) )
27 2 4 3 mulg0 
 |-  ( z e. C -> ( 0 .x. z ) = .0. )
28 27 adantl 
 |-  ( ( ph /\ z e. C ) -> ( 0 .x. z ) = .0. )
29 c0ex 
 |-  0 e. _V
30 29 a1i 
 |-  ( ph -> 0 e. _V )
31 26 28 14 7 8 30 suppssof1 
 |-  ( ph -> ( ( B oF .x. G ) supp .0. ) C_ ( B supp 0 ) )
32 suppssfifsupp 
 |-  ( ( ( ( B oF .x. G ) e. _V /\ Fun ( B oF .x. G ) /\ .0. e. _V ) /\ ( ( B supp 0 ) e. Fin /\ ( ( B oF .x. G ) supp .0. ) C_ ( B supp 0 ) ) ) -> ( B oF .x. G ) finSupp .0. )
33 17 20 22 25 31 32 syl32anc 
 |-  ( ph -> ( B oF .x. G ) finSupp .0. )
34 16 33 jca 
 |-  ( ph -> ( ( B oF .x. G ) : I --> C /\ ( B oF .x. G ) finSupp .0. ) )