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 ⊢ 𝑃 = ( 𝑆 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 0fi ⊢ ∅ ∈ 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 ∈ 𝐻 )