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=BaseSmR
dsmmcl.i φIW
dsmmcl.s φSV
dsmmcl.r φR:IMnd
dsmm0cl.z 0˙=0P
Assertion dsmm0cl φ0˙H

Proof

Step Hyp Ref Expression
1 dsmmcl.p P=S𝑠R
2 dsmmcl.h H=BaseSmR
3 dsmmcl.i φIW
4 dsmmcl.s φSV
5 dsmmcl.r φR:IMnd
6 dsmm0cl.z 0˙=0P
7 1 3 4 5 prdsmndd φPMnd
8 eqid BaseP=BaseP
9 8 6 mndidcl PMnd0˙BaseP
10 7 9 syl φ0˙BaseP
11 1 3 4 5 prds0g φ0𝑔R=0P
12 11 6 eqtr4di φ0𝑔R=0˙
13 12 adantr φaI0𝑔R=0˙
14 13 fveq1d φaI0𝑔Ra=0˙a
15 5 ffnd φRFnI
16 fvco2 RFnIaI0𝑔Ra=0Ra
17 15 16 sylan φaI0𝑔Ra=0Ra
18 14 17 eqtr3d φaI0˙a=0Ra
19 nne ¬0˙a0Ra0˙a=0Ra
20 18 19 sylibr φaI¬0˙a0Ra
21 20 ralrimiva φaI¬0˙a0Ra
22 rabeq0 aI|0˙a0Ra=aI¬0˙a0Ra
23 21 22 sylibr φaI|0˙a0Ra=
24 0fin Fin
25 23 24 eqeltrdi φaI|0˙a0RaFin
26 eqid SmR=SmR
27 1 26 8 2 3 15 dsmmelbas φ0˙H0˙BasePaI|0˙a0RaFin
28 10 25 27 mpbir2and φ0˙H