Metamath Proof Explorer


Theorem dsmmacl

Description: The finite hull is closed under addition. (Contributed by Stefan O'Rear, 11-Jan-2015)

Ref Expression
Hypotheses dsmmcl.p
|- P = ( S Xs_ R )
dsmmcl.h
|- H = ( Base ` ( S (+)m R ) )
dsmmcl.i
|- ( ph -> I e. W )
dsmmcl.s
|- ( ph -> S e. V )
dsmmcl.r
|- ( ph -> R : I --> Mnd )
dsmmacl.j
|- ( ph -> J e. H )
dsmmacl.k
|- ( ph -> K e. H )
dsmmacl.a
|- .+ = ( +g ` P )
Assertion dsmmacl
|- ( ph -> ( J .+ K ) e. H )

Proof

Step Hyp Ref Expression
1 dsmmcl.p
 |-  P = ( S Xs_ R )
2 dsmmcl.h
 |-  H = ( Base ` ( S (+)m R ) )
3 dsmmcl.i
 |-  ( ph -> I e. W )
4 dsmmcl.s
 |-  ( ph -> S e. V )
5 dsmmcl.r
 |-  ( ph -> R : I --> Mnd )
6 dsmmacl.j
 |-  ( ph -> J e. H )
7 dsmmacl.k
 |-  ( ph -> K e. H )
8 dsmmacl.a
 |-  .+ = ( +g ` P )
9 eqid
 |-  ( Base ` P ) = ( Base ` P )
10 eqid
 |-  ( S (+)m R ) = ( S (+)m R )
11 5 ffnd
 |-  ( ph -> R Fn I )
12 1 10 9 2 3 11 dsmmelbas
 |-  ( ph -> ( J e. H <-> ( J e. ( Base ` P ) /\ { a e. I | ( J ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin ) ) )
13 6 12 mpbid
 |-  ( ph -> ( J e. ( Base ` P ) /\ { a e. I | ( J ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin ) )
14 13 simpld
 |-  ( ph -> J e. ( Base ` P ) )
15 1 10 9 2 3 11 dsmmelbas
 |-  ( ph -> ( K e. H <-> ( K e. ( Base ` P ) /\ { a e. I | ( K ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin ) ) )
16 7 15 mpbid
 |-  ( ph -> ( K e. ( Base ` P ) /\ { a e. I | ( K ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin ) )
17 16 simpld
 |-  ( ph -> K e. ( Base ` P ) )
18 1 9 8 4 3 5 14 17 prdsplusgcl
 |-  ( ph -> ( J .+ K ) e. ( Base ` P ) )
19 4 adantr
 |-  ( ( ph /\ a e. I ) -> S e. V )
20 3 adantr
 |-  ( ( ph /\ a e. I ) -> I e. W )
21 11 adantr
 |-  ( ( ph /\ a e. I ) -> R Fn I )
22 14 adantr
 |-  ( ( ph /\ a e. I ) -> J e. ( Base ` P ) )
23 17 adantr
 |-  ( ( ph /\ a e. I ) -> K e. ( Base ` P ) )
24 simpr
 |-  ( ( ph /\ a e. I ) -> a e. I )
25 1 9 19 20 21 22 23 8 24 prdsplusgfval
 |-  ( ( ph /\ a e. I ) -> ( ( J .+ K ) ` a ) = ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) )
26 25 neeq1d
 |-  ( ( ph /\ a e. I ) -> ( ( ( J .+ K ) ` a ) =/= ( 0g ` ( R ` a ) ) <-> ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) =/= ( 0g ` ( R ` a ) ) ) )
27 26 rabbidva
 |-  ( ph -> { a e. I | ( ( J .+ K ) ` a ) =/= ( 0g ` ( R ` a ) ) } = { a e. I | ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) =/= ( 0g ` ( R ` a ) ) } )
28 13 simprd
 |-  ( ph -> { a e. I | ( J ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin )
29 16 simprd
 |-  ( ph -> { a e. I | ( K ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin )
30 unfi
 |-  ( ( { a e. I | ( J ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin /\ { a e. I | ( K ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin ) -> ( { a e. I | ( J ` a ) =/= ( 0g ` ( R ` a ) ) } u. { a e. I | ( K ` a ) =/= ( 0g ` ( R ` a ) ) } ) e. Fin )
31 28 29 30 syl2anc
 |-  ( ph -> ( { a e. I | ( J ` a ) =/= ( 0g ` ( R ` a ) ) } u. { a e. I | ( K ` a ) =/= ( 0g ` ( R ` a ) ) } ) e. Fin )
32 neorian
 |-  ( ( ( J ` a ) =/= ( 0g ` ( R ` a ) ) \/ ( K ` a ) =/= ( 0g ` ( R ` a ) ) ) <-> -. ( ( J ` a ) = ( 0g ` ( R ` a ) ) /\ ( K ` a ) = ( 0g ` ( R ` a ) ) ) )
33 32 bicomi
 |-  ( -. ( ( J ` a ) = ( 0g ` ( R ` a ) ) /\ ( K ` a ) = ( 0g ` ( R ` a ) ) ) <-> ( ( J ` a ) =/= ( 0g ` ( R ` a ) ) \/ ( K ` a ) =/= ( 0g ` ( R ` a ) ) ) )
34 33 con1bii
 |-  ( -. ( ( J ` a ) =/= ( 0g ` ( R ` a ) ) \/ ( K ` a ) =/= ( 0g ` ( R ` a ) ) ) <-> ( ( J ` a ) = ( 0g ` ( R ` a ) ) /\ ( K ` a ) = ( 0g ` ( R ` a ) ) ) )
35 5 ffvelrnda
 |-  ( ( ph /\ a e. I ) -> ( R ` a ) e. Mnd )
36 eqid
 |-  ( Base ` ( R ` a ) ) = ( Base ` ( R ` a ) )
37 eqid
 |-  ( 0g ` ( R ` a ) ) = ( 0g ` ( R ` a ) )
38 36 37 mndidcl
 |-  ( ( R ` a ) e. Mnd -> ( 0g ` ( R ` a ) ) e. ( Base ` ( R ` a ) ) )
39 eqid
 |-  ( +g ` ( R ` a ) ) = ( +g ` ( R ` a ) )
40 36 39 37 mndlid
 |-  ( ( ( R ` a ) e. Mnd /\ ( 0g ` ( R ` a ) ) e. ( Base ` ( R ` a ) ) ) -> ( ( 0g ` ( R ` a ) ) ( +g ` ( R ` a ) ) ( 0g ` ( R ` a ) ) ) = ( 0g ` ( R ` a ) ) )
41 35 38 40 syl2anc2
 |-  ( ( ph /\ a e. I ) -> ( ( 0g ` ( R ` a ) ) ( +g ` ( R ` a ) ) ( 0g ` ( R ` a ) ) ) = ( 0g ` ( R ` a ) ) )
42 oveq12
 |-  ( ( ( J ` a ) = ( 0g ` ( R ` a ) ) /\ ( K ` a ) = ( 0g ` ( R ` a ) ) ) -> ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) = ( ( 0g ` ( R ` a ) ) ( +g ` ( R ` a ) ) ( 0g ` ( R ` a ) ) ) )
43 42 eqeq1d
 |-  ( ( ( J ` a ) = ( 0g ` ( R ` a ) ) /\ ( K ` a ) = ( 0g ` ( R ` a ) ) ) -> ( ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) = ( 0g ` ( R ` a ) ) <-> ( ( 0g ` ( R ` a ) ) ( +g ` ( R ` a ) ) ( 0g ` ( R ` a ) ) ) = ( 0g ` ( R ` a ) ) ) )
44 41 43 syl5ibrcom
 |-  ( ( ph /\ a e. I ) -> ( ( ( J ` a ) = ( 0g ` ( R ` a ) ) /\ ( K ` a ) = ( 0g ` ( R ` a ) ) ) -> ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) = ( 0g ` ( R ` a ) ) ) )
45 34 44 syl5bi
 |-  ( ( ph /\ a e. I ) -> ( -. ( ( J ` a ) =/= ( 0g ` ( R ` a ) ) \/ ( K ` a ) =/= ( 0g ` ( R ` a ) ) ) -> ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) = ( 0g ` ( R ` a ) ) ) )
46 45 necon1ad
 |-  ( ( ph /\ a e. I ) -> ( ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) =/= ( 0g ` ( R ` a ) ) -> ( ( J ` a ) =/= ( 0g ` ( R ` a ) ) \/ ( K ` a ) =/= ( 0g ` ( R ` a ) ) ) ) )
47 46 ss2rabdv
 |-  ( ph -> { a e. I | ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) =/= ( 0g ` ( R ` a ) ) } C_ { a e. I | ( ( J ` a ) =/= ( 0g ` ( R ` a ) ) \/ ( K ` a ) =/= ( 0g ` ( R ` a ) ) ) } )
48 unrab
 |-  ( { a e. I | ( J ` a ) =/= ( 0g ` ( R ` a ) ) } u. { a e. I | ( K ` a ) =/= ( 0g ` ( R ` a ) ) } ) = { a e. I | ( ( J ` a ) =/= ( 0g ` ( R ` a ) ) \/ ( K ` a ) =/= ( 0g ` ( R ` a ) ) ) }
49 47 48 sseqtrrdi
 |-  ( ph -> { a e. I | ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) =/= ( 0g ` ( R ` a ) ) } C_ ( { a e. I | ( J ` a ) =/= ( 0g ` ( R ` a ) ) } u. { a e. I | ( K ` a ) =/= ( 0g ` ( R ` a ) ) } ) )
50 31 49 ssfid
 |-  ( ph -> { a e. I | ( ( J ` a ) ( +g ` ( R ` a ) ) ( K ` a ) ) =/= ( 0g ` ( R ` a ) ) } e. Fin )
51 27 50 eqeltrd
 |-  ( ph -> { a e. I | ( ( J .+ K ) ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin )
52 1 10 9 2 3 11 dsmmelbas
 |-  ( ph -> ( ( J .+ K ) e. H <-> ( ( J .+ K ) e. ( Base ` P ) /\ { a e. I | ( ( J .+ K ) ` a ) =/= ( 0g ` ( R ` a ) ) } e. Fin ) ) )
53 18 51 52 mpbir2and
 |-  ( ph -> ( J .+ K ) e. H )