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{⨉}_{𝑠}R$$
	dsmmcl.h	$$⊢H={\mathrm{Base}}_{\left(S{\oplus }_{m}R\right)}$$
	dsmmcl.i	$$⊢\phi \to I\in W$$
	dsmmcl.s	$$⊢\phi \to S\in V$$
	dsmmcl.r	$$⊢\phi \to R:I⟶\mathrm{Mnd}$$
	dsmm0cl.z	$$⊢\underset{\dot{}}{0}=0_P$$
Assertion	dsmm0cl	$$⊢\phi \to \underset{\dot{}}{0}\in H$$

Proof

Step	Hyp	Ref	Expression
1		dsmmcl.p	$$⊢P=S{⨉}_{𝑠}R$$
2		dsmmcl.h	$$⊢H={\mathrm{Base}}_{\left(S{\oplus }_{m}R\right)}$$
3		dsmmcl.i	$$⊢\phi \to I\in W$$
4		dsmmcl.s	$$⊢\phi \to S\in V$$
5		dsmmcl.r	$$⊢\phi \to R:I⟶\mathrm{Mnd}$$
6		dsmm0cl.z	$$⊢\underset{\dot{}}{0}=0_P$$
7	1 3 4 5	prdsmndd	$$⊢\phi \to P\in \mathrm{Mnd}$$
8		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
9	8 6	mndidcl	$$⊢P\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_P$$
10	7 9	syl	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_P$$
11	1 3 4 5	prds0g	$$⊢\phi \to 0_{𝑔}\circ R=0_P$$
12	11 6	eqtr4di	$$⊢\phi \to 0_{𝑔}\circ R=\underset{\dot{}}{0}$$
13	12	adantr	$$⊢\left(\phi \wedge a\in I\right)\to 0_{𝑔}\circ R=\underset{\dot{}}{0}$$
14	13	fveq1d	$$⊢\left(\phi \wedge a\in I\right)\to \left(0_{𝑔}\circ R\right)\left(a\right)=\underset{\dot{}}{0}\left(a\right)$$
15	5	ffnd	$$⊢\phi \to RFnI$$
16		fvco2	$$⊢\left(RFnI\wedge a\in I\right)\to \left(0_{𝑔}\circ R\right)\left(a\right)=0_{R\left(a\right)}$$
17	15 16	sylan	$$⊢\left(\phi \wedge a\in I\right)\to \left(0_{𝑔}\circ R\right)\left(a\right)=0_{R\left(a\right)}$$
18	14 17	eqtr3d	$$⊢\left(\phi \wedge a\in I\right)\to \underset{\dot{}}{0}\left(a\right)=0_{R\left(a\right)}$$
19		nne	$$⊢\neg \underset{\dot{}}{0}\left(a\right)\ne 0_{R\left(a\right)}\leftrightarrow \underset{\dot{}}{0}\left(a\right)=0_{R\left(a\right)}$$
20	18 19	sylibr	$$⊢\left(\phi \wedge a\in I\right)\to \neg \underset{\dot{}}{0}\left(a\right)\ne 0_{R\left(a\right)}$$
21	20	ralrimiva	$$⊢\phi \to \forall a\in I\neg \underset{\dot{}}{0}\left(a\right)\ne 0_{R\left(a\right)}$$
22		rabeq0	$$⊢\left\{a\in I|\underset{\dot{}}{0}\left(a\right)\ne 0_{R\left(a\right)}\right\}=\varnothing \leftrightarrow \forall a\in I\neg \underset{\dot{}}{0}\left(a\right)\ne 0_{R\left(a\right)}$$
23	21 22	sylibr	$$⊢\phi \to \left\{a\in I|\underset{\dot{}}{0}\left(a\right)\ne 0_{R\left(a\right)}\right\}=\varnothing$$
24		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
25	23 24	eqeltrdi	$$⊢\phi \to \left\{a\in I|\underset{\dot{}}{0}\left(a\right)\ne 0_{R\left(a\right)}\right\}\in \mathrm{Fin}$$
26		eqid	$$⊢S{\oplus }_{m}R=S{\oplus }_{m}R$$
27	1 26 8 2 3 15	dsmmelbas	$$⊢\phi \to \left(\underset{\dot{}}{0}\in H\leftrightarrow \left(\underset{\dot{}}{0}\in {\mathrm{Base}}_P\wedge \left\{a\in I|\underset{\dot{}}{0}\left(a\right)\ne 0_{R\left(a\right)}\right\}\in \mathrm{Fin}\right)\right)$$
28	10 25 27	mpbir2and	$$⊢\phi \to \underset{\dot{}}{0}\in H$$