This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dsmm0cl

Description: The all-zero vector is contained in the finite hull, since its support is empty and therefore finite. This theorem along with the next one effectively proves that the finite hull is a "submonoid", although that does not exist as a defined concept yet. (Contributed by Stefan O'Rear, 11-Jan-2015)

Ref Expression
Hypotheses dsmmcl.p 
|- P = ( S Xs_ R )
dsmmcl.h 
|- H = ( Base ` ( S (+)m R ) )
dsmmcl.i 
|- ( ph -> I e. W )
dsmmcl.s 
|- ( ph -> S e. V )
dsmmcl.r 
|- ( ph -> R : I --> Mnd )
dsmm0cl.z 
|- .0. = ( 0g ` P )
Assertion dsmm0cl 
|- ( ph -> .0. e. H )

Proof

Step Hyp Ref Expression
1 dsmmcl.p 
 |-  P = ( S Xs_ R )
2 dsmmcl.h 
 |-  H = ( Base ` ( S (+)m R ) )
3 dsmmcl.i 
 |-  ( ph -> I e. W )
4 dsmmcl.s 
 |-  ( ph -> S e. V )
5 dsmmcl.r 
 |-  ( ph -> R : I --> Mnd )
6 dsmm0cl.z 
 |-  .0. = ( 0g ` P )
7 1 3 4 5 prdsmndd 
 |-  ( ph -> P e. Mnd )
8 eqid 
 |-  ( Base ` P ) = ( Base ` P )
9 8 6 mndidcl 
 |-  ( P e. Mnd -> .0. e. ( Base ` P ) )
10 7 9 syl 
 |-  ( ph -> .0. e. ( Base ` P ) )
11 1 3 4 5 prds0g 
 |-  ( ph -> ( 0g o. R ) = ( 0g ` P ) )
12 11 6 eqtr4di 
 |-  ( ph -> ( 0g o. R ) = .0. )
13 12 adantr 
 |-  ( ( ph /\ a e. I ) -> ( 0g o. R ) = .0. )
14 13 fveq1d 
 |-  ( ( ph /\ a e. I ) -> ( ( 0g o. R ) ` a ) = ( .0. ` a ) )
15 5 ffnd 
 |-  ( ph -> R Fn I )
16 fvco2 
 |-  ( ( R Fn I /\ a e. I ) -> ( ( 0g o. R ) ` a ) = ( 0g ` ( R ` a ) ) )
17 15 16 sylan 
 |-  ( ( ph /\ a e. I ) -> ( ( 0g o. R ) ` a ) = ( 0g ` ( R ` a ) ) )
18 14 17 eqtr3d 
 |-  ( ( ph /\ a e. I ) -> ( .0. ` a ) = ( 0g ` ( R ` a ) ) )
19 nne 
 |-  ( -. ( .0. ` a ) =/= ( 0g ` ( R ` a ) ) <-> ( .0. ` a ) = ( 0g ` ( R ` a ) ) )
20 18 19 sylibr 
 |-  ( ( ph /\ a e. I ) -> -. ( .0. ` a ) =/= ( 0g ` ( R ` a ) ) )
21 20 ralrimiva 
 |-  ( ph -> A. a e. I -. ( .0. ` a ) =/= ( 0g ` ( R ` a ) ) )
22 rabeq0 
 |-  ( { a e. I | ( .0. ` a ) =/= ( 0g ` ( R ` a ) ) } = (/) <-> A. a e. I -. ( .0. ` a ) =/= ( 0g ` ( R ` a ) ) )
23 21 22 sylibr 
 |-  ( ph -> { a e. I | ( .0. ` a ) =/= ( 0g ` ( R ` a ) ) } = (/) )
24 0fi 
 |-  (/) e. Fin
25 23 24 eqeltrdi 
 |-  ( ph -> { a e. I | ( .0. ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin )
26 eqid 
 |-  ( S (+)m R ) = ( S (+)m R )
27 1 26 8 2 3 15 dsmmelbas 
 |-  ( ph -> ( .0. e. H <-> ( .0. e. ( Base ` P ) /\ { a e. I | ( .0. ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin ) ) )
28 10 25 27 mpbir2and 
 |-  ( ph -> .0. e. H )