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	⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
	dsmmcl.h	⊢ 𝐻 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
	dsmmcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	dsmmcl.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	dsmmcl.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
	dsmm0cl.z	⊢ 0 = ( 0g ‘ 𝑃 )
Assertion	dsmm0cl	⊢ ( 𝜑 → 0 ∈ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		dsmmcl.p	⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
2		dsmmcl.h	⊢ 𝐻 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
3		dsmmcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4		dsmmcl.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
5		dsmmcl.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
6		dsmm0cl.z	⊢ 0 = ( 0g ‘ 𝑃 )
7	1 3 4 5	prdsmndd	⊢ ( 𝜑 → 𝑃 ∈ Mnd )
8		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
9	8 6	mndidcl	⊢ ( 𝑃 ∈ Mnd → 0 ∈ ( Base ‘ 𝑃 ) )
10	7 9	syl	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑃 ) )
11	1 3 4 5	prds0g	⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) = ( 0g ‘ 𝑃 ) )
12	11 6	eqtr4di	⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) = 0 )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 0g ∘ 𝑅 ) = 0 )
14	13	fveq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( 0g ∘ 𝑅 ) ‘ 𝑎 ) = ( 0 ‘ 𝑎 ) )
15	5	ffnd	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
16		fvco2	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝑎 ∈ 𝐼 ) → ( ( 0g ∘ 𝑅 ) ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) )
17	15 16	sylan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( 0g ∘ 𝑅 ) ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) )
18	14 17	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( 0 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) )
19		nne	⊢ ( ¬ ( 0 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) ↔ ( 0 ‘ 𝑎 ) = ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) )
20	18 19	sylibr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ¬ ( 0 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) )
21	20	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐼 ¬ ( 0 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) )
22		rabeq0	⊢ ( { 𝑎 ∈ 𝐼 ∣ ( 0 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } = ∅ ↔ ∀ 𝑎 ∈ 𝐼 ¬ ( 0 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) )
23	21 22	sylibr	⊢ ( 𝜑 → { 𝑎 ∈ 𝐼 ∣ ( 0 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } = ∅ )
24		0fin	⊢ ∅ ∈ Fin
25	23 24	eqeltrdi	⊢ ( 𝜑 → { 𝑎 ∈ 𝐼 ∣ ( 0 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin )
26		eqid	⊢ ( 𝑆 ⊕m 𝑅 ) = ( 𝑆 ⊕m 𝑅 )
27	1 26 8 2 3 15	dsmmelbas	⊢ ( 𝜑 → ( 0 ∈ 𝐻 ↔ ( 0 ∈ ( Base ‘ 𝑃 ) ∧ { 𝑎 ∈ 𝐼 ∣ ( 0 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin ) ) )
28	10 25 27	mpbir2and	⊢ ( 𝜑 → 0 ∈ 𝐻 )