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		0fin	|- (/) 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 )