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 ⨉ 𝑠 R
dsmmcl.h ⊢ H = Base S ⊕ m R
dsmmcl.i ⊢ φ → I ∈ W
dsmmcl.s ⊢ φ → S ∈ V
dsmmcl.r ⊢ φ → R : I ⟶ Mnd
dsmm0cl.z ⊢ 0 ˙ = 0 P
Assertion dsmm0cl ⊢ φ → 0 ˙ ∈ H

Proof

Step Hyp Ref Expression
1 dsmmcl.p ⊢ P = S ⨉ 𝑠 R
2 dsmmcl.h ⊢ H = Base S ⊕ m R
3 dsmmcl.i ⊢ φ → I ∈ W
4 dsmmcl.s ⊢ φ → S ∈ V
5 dsmmcl.r ⊢ φ → R : I ⟶ Mnd
6 dsmm0cl.z ⊢ 0 ˙ = 0 P
7 1 3 4 5 prdsmndd ⊢ φ → P ∈ Mnd
8 eqid ⊢ Base P = Base P
9 8 6 mndidcl ⊢ P ∈ Mnd → 0 ˙ ∈ Base P
10 7 9 syl ⊢ φ → 0 ˙ ∈ Base P
11 1 3 4 5 prds0g ⊢ φ → 0 𝑔 ∘ R = 0 P
12 11 6 eqtr4di ⊢ φ → 0 𝑔 ∘ R = 0 ˙
13 12 adantr ⊢ φ ∧ a ∈ I → 0 𝑔 ∘ R = 0 ˙
14 13 fveq1d ⊢ φ ∧ a ∈ I → 0 𝑔 ∘ R ⁡ a = 0 ˙ ⁡ a
15 5 ffnd ⊢ φ → R Fn I
16 fvco2 ⊢ R Fn I ∧ a ∈ I → 0 𝑔 ∘ R ⁡ a = 0 R ⁡ a
17 15 16 sylan ⊢ φ ∧ a ∈ I → 0 𝑔 ∘ R ⁡ a = 0 R ⁡ a
18 14 17 eqtr3d ⊢ φ ∧ a ∈ I → 0 ˙ ⁡ a = 0 R ⁡ a
19 nne ⊢ ¬ 0 ˙ ⁡ a ≠ 0 R ⁡ a ↔ 0 ˙ ⁡ a = 0 R ⁡ a
20 18 19 sylibr ⊢ φ ∧ a ∈ I → ¬ 0 ˙ ⁡ a ≠ 0 R ⁡ a
21 20 ralrimiva ⊢ φ → ∀ a ∈ I ¬ 0 ˙ ⁡ a ≠ 0 R ⁡ a
22 rabeq0 ⊢ a ∈ I | 0 ˙ ⁡ a ≠ 0 R ⁡ a = ∅ ↔ ∀ a ∈ I ¬ 0 ˙ ⁡ a ≠ 0 R ⁡ a
23 21 22 sylibr ⊢ φ → a ∈ I | 0 ˙ ⁡ a ≠ 0 R ⁡ a = ∅
24 0fi ⊢ ∅ ∈ Fin
25 23 24 eqeltrdi ⊢ φ → a ∈ I | 0 ˙ ⁡ a ≠ 0 R ⁡ a ∈ Fin
26 eqid ⊢ S ⊕ m R = S ⊕ m R
27 1 26 8 2 3 15 dsmmelbas ⊢ φ → 0 ˙ ∈ H ↔ 0 ˙ ∈ Base P ∧ a ∈ I | 0 ˙ ⁡ a ≠ 0 R ⁡ a ∈ Fin
28 10 25 27 mpbir2and ⊢ φ → 0 ˙ ∈ H