Metamath Proof Explorer

Theorem lco0

Description: The set of empty linear combinations over a monoid is the singleton with the identity element of the monoid. (Contributed by AV, 12-Apr-2019)

Ref Expression
Assertion lco0 
|- ( M e. Mnd -> ( M LinCo (/) ) = { ( 0g ` M ) } )

Proof

Step Hyp Ref Expression
1 0elpw 
 |-  (/) e. ~P ( Base ` M )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
4 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
5 2 3 4 lcoop 
 |-  ( ( M e. Mnd /\ (/) e. ~P ( Base ` M ) ) -> ( M LinCo (/) ) = { v e. ( Base ` M ) | E. w e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) ( w finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( w ( linC ` M ) (/) ) ) } )
6 1 5 mpan2 
 |-  ( M e. Mnd -> ( M LinCo (/) ) = { v e. ( Base ` M ) | E. w e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) ( w finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( w ( linC ` M ) (/) ) ) } )
7 fvex 
 |-  ( Base ` ( Scalar ` M ) ) e. _V
8 map0e 
 |-  ( ( Base ` ( Scalar ` M ) ) e. _V -> ( ( Base ` ( Scalar ` M ) ) ^m (/) ) = 1o )
9 7 8 mp1i 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> ( ( Base ` ( Scalar ` M ) ) ^m (/) ) = 1o )
10 df1o2 
 |-  1o = { (/) }
11 9 10 eqtrdi 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> ( ( Base ` ( Scalar ` M ) ) ^m (/) ) = { (/) } )
12 11 rexeqdv 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> ( E. w e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) ( w finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( w ( linC ` M ) (/) ) ) <-> E. w e. { (/) } ( w finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( w ( linC ` M ) (/) ) ) ) )
13 lincval0 
 |-  ( M e. Mnd -> ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) )
14 13 adantr 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) )
15 14 eqeq2d 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> ( v = ( (/) ( linC ` M ) (/) ) <-> v = ( 0g ` M ) ) )
16 15 anbi2d 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> ( ( (/) e. Fin /\ v = ( (/) ( linC ` M ) (/) ) ) <-> ( (/) e. Fin /\ v = ( 0g ` M ) ) ) )
17 0ex 
 |-  (/) e. _V
18 breq1 
 |-  ( w = (/) -> ( w finSupp ( 0g ` ( Scalar ` M ) ) <-> (/) finSupp ( 0g ` ( Scalar ` M ) ) ) )
19 fvex 
 |-  ( 0g ` ( Scalar ` M ) ) e. _V
20 0fsupp 
 |-  ( ( 0g ` ( Scalar ` M ) ) e. _V -> (/) finSupp ( 0g ` ( Scalar ` M ) ) )
21 19 20 ax-mp 
 |-  (/) finSupp ( 0g ` ( Scalar ` M ) )
22 0fin 
 |-  (/) e. Fin
23 21 22 2th 
 |-  ( (/) finSupp ( 0g ` ( Scalar ` M ) ) <-> (/) e. Fin )
24 18 23 bitrdi 
 |-  ( w = (/) -> ( w finSupp ( 0g ` ( Scalar ` M ) ) <-> (/) e. Fin ) )
25 oveq1 
 |-  ( w = (/) -> ( w ( linC ` M ) (/) ) = ( (/) ( linC ` M ) (/) ) )
26 25 eqeq2d 
 |-  ( w = (/) -> ( v = ( w ( linC ` M ) (/) ) <-> v = ( (/) ( linC ` M ) (/) ) ) )
27 24 26 anbi12d 
 |-  ( w = (/) -> ( ( w finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( w ( linC ` M ) (/) ) ) <-> ( (/) e. Fin /\ v = ( (/) ( linC ` M ) (/) ) ) ) )
28 27 rexsng 
 |-  ( (/) e. _V -> ( E. w e. { (/) } ( w finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( w ( linC ` M ) (/) ) ) <-> ( (/) e. Fin /\ v = ( (/) ( linC ` M ) (/) ) ) ) )
29 17 28 mp1i 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> ( E. w e. { (/) } ( w finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( w ( linC ` M ) (/) ) ) <-> ( (/) e. Fin /\ v = ( (/) ( linC ` M ) (/) ) ) ) )
30 22 a1i 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> (/) e. Fin )
31 30 biantrurd 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> ( v = ( 0g ` M ) <-> ( (/) e. Fin /\ v = ( 0g ` M ) ) ) )
32 16 29 31 3bitr4d 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> ( E. w e. { (/) } ( w finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( w ( linC ` M ) (/) ) ) <-> v = ( 0g ` M ) ) )
33 12 32 bitrd 
 |-  ( ( M e. Mnd /\ v e. ( Base ` M ) ) -> ( E. w e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) ( w finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( w ( linC ` M ) (/) ) ) <-> v = ( 0g ` M ) ) )
34 33 rabbidva 
 |-  ( M e. Mnd -> { v e. ( Base ` M ) | E. w e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) ( w finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( w ( linC ` M ) (/) ) ) } = { v e. ( Base ` M ) | v = ( 0g ` M ) } )
35 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
36 2 35 mndidcl 
 |-  ( M e. Mnd -> ( 0g ` M ) e. ( Base ` M ) )
37 rabsn 
 |-  ( ( 0g ` M ) e. ( Base ` M ) -> { v e. ( Base ` M ) | v = ( 0g ` M ) } = { ( 0g ` M ) } )
38 36 37 syl 
 |-  ( M e. Mnd -> { v e. ( Base ` M ) | v = ( 0g ` M ) } = { ( 0g ` M ) } )
39 6 34 38 3eqtrd 
 |-  ( M e. Mnd -> ( M LinCo (/) ) = { ( 0g ` M ) } )