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