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 ffvelcdmda 
 |-  ( ( 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 biimtrid 
 |-  ( ( 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 )