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 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𝐻 )