Step |
Hyp |
Ref |
Expression |
1 |
|
pwslnmlem2.a |
|- A e. _V |
2 |
|
pwslnmlem2.b |
|- B e. _V |
3 |
|
pwslnmlem2.x |
|- X = ( W ^s A ) |
4 |
|
pwslnmlem2.y |
|- Y = ( W ^s B ) |
5 |
|
pwslnmlem2.z |
|- Z = ( W ^s ( A u. B ) ) |
6 |
|
pwslnmlem2.w |
|- ( ph -> W e. LMod ) |
7 |
|
pwslnmlem2.dj |
|- ( ph -> ( A i^i B ) = (/) ) |
8 |
|
pwslnmlem2.xn |
|- ( ph -> X e. LNoeM ) |
9 |
|
pwslnmlem2.yn |
|- ( ph -> Y e. LNoeM ) |
10 |
1 2
|
unex |
|- ( A u. B ) e. _V |
11 |
10
|
a1i |
|- ( ph -> ( A u. B ) e. _V ) |
12 |
|
ssun1 |
|- A C_ ( A u. B ) |
13 |
12
|
a1i |
|- ( ph -> A C_ ( A u. B ) ) |
14 |
|
eqid |
|- ( Base ` Z ) = ( Base ` Z ) |
15 |
|
eqid |
|- ( Base ` X ) = ( Base ` X ) |
16 |
|
eqid |
|- ( x e. ( Base ` Z ) |-> ( x |` A ) ) = ( x e. ( Base ` Z ) |-> ( x |` A ) ) |
17 |
5 3 14 15 16
|
pwssplit3 |
|- ( ( W e. LMod /\ ( A u. B ) e. _V /\ A C_ ( A u. B ) ) -> ( x e. ( Base ` Z ) |-> ( x |` A ) ) e. ( Z LMHom X ) ) |
18 |
6 11 13 17
|
syl3anc |
|- ( ph -> ( x e. ( Base ` Z ) |-> ( x |` A ) ) e. ( Z LMHom X ) ) |
19 |
|
fvex |
|- ( 0g ` X ) e. _V |
20 |
16
|
mptiniseg |
|- ( ( 0g ` X ) e. _V -> ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) = { x e. ( Base ` Z ) | ( x |` A ) = ( 0g ` X ) } ) |
21 |
19 20
|
ax-mp |
|- ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) = { x e. ( Base ` Z ) | ( x |` A ) = ( 0g ` X ) } |
22 |
|
lmodgrp |
|- ( W e. LMod -> W e. Grp ) |
23 |
|
grpmnd |
|- ( W e. Grp -> W e. Mnd ) |
24 |
6 22 23
|
3syl |
|- ( ph -> W e. Mnd ) |
25 |
|
eqid |
|- ( 0g ` W ) = ( 0g ` W ) |
26 |
3 25
|
pws0g |
|- ( ( W e. Mnd /\ A e. _V ) -> ( A X. { ( 0g ` W ) } ) = ( 0g ` X ) ) |
27 |
24 1 26
|
sylancl |
|- ( ph -> ( A X. { ( 0g ` W ) } ) = ( 0g ` X ) ) |
28 |
27
|
eqcomd |
|- ( ph -> ( 0g ` X ) = ( A X. { ( 0g ` W ) } ) ) |
29 |
28
|
eqeq2d |
|- ( ph -> ( ( x |` A ) = ( 0g ` X ) <-> ( x |` A ) = ( A X. { ( 0g ` W ) } ) ) ) |
30 |
29
|
rabbidv |
|- ( ph -> { x e. ( Base ` Z ) | ( x |` A ) = ( 0g ` X ) } = { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) |
31 |
21 30
|
syl5eq |
|- ( ph -> ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) = { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) |
32 |
31
|
oveq2d |
|- ( ph -> ( Z |`s ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) ) = ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) ) |
33 |
|
eqid |
|- { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } = { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |
34 |
|
eqid |
|- ( y e. { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |-> ( y |` B ) ) = ( y e. { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |-> ( y |` B ) ) |
35 |
|
eqid |
|- ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) = ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) |
36 |
5 14 25 33 34 3 4 35
|
pwssplit4 |
|- ( ( W e. LMod /\ ( A u. B ) e. _V /\ ( A i^i B ) = (/) ) -> ( y e. { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |-> ( y |` B ) ) e. ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) LMIso Y ) ) |
37 |
6 11 7 36
|
syl3anc |
|- ( ph -> ( y e. { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |-> ( y |` B ) ) e. ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) LMIso Y ) ) |
38 |
|
brlmici |
|- ( ( y e. { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |-> ( y |` B ) ) e. ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) LMIso Y ) -> ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) ~=m Y ) |
39 |
|
lnmlmic |
|- ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) ~=m Y -> ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) e. LNoeM <-> Y e. LNoeM ) ) |
40 |
37 38 39
|
3syl |
|- ( ph -> ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) e. LNoeM <-> Y e. LNoeM ) ) |
41 |
9 40
|
mpbird |
|- ( ph -> ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) e. LNoeM ) |
42 |
32 41
|
eqeltrd |
|- ( ph -> ( Z |`s ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) ) e. LNoeM ) |
43 |
5 3 14 15 16
|
pwssplit1 |
|- ( ( W e. Mnd /\ ( A u. B ) e. _V /\ A C_ ( A u. B ) ) -> ( x e. ( Base ` Z ) |-> ( x |` A ) ) : ( Base ` Z ) -onto-> ( Base ` X ) ) |
44 |
24 11 13 43
|
syl3anc |
|- ( ph -> ( x e. ( Base ` Z ) |-> ( x |` A ) ) : ( Base ` Z ) -onto-> ( Base ` X ) ) |
45 |
|
forn |
|- ( ( x e. ( Base ` Z ) |-> ( x |` A ) ) : ( Base ` Z ) -onto-> ( Base ` X ) -> ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) = ( Base ` X ) ) |
46 |
44 45
|
syl |
|- ( ph -> ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) = ( Base ` X ) ) |
47 |
46
|
oveq2d |
|- ( ph -> ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) = ( X |`s ( Base ` X ) ) ) |
48 |
15
|
ressid |
|- ( X e. LNoeM -> ( X |`s ( Base ` X ) ) = X ) |
49 |
8 48
|
syl |
|- ( ph -> ( X |`s ( Base ` X ) ) = X ) |
50 |
47 49
|
eqtrd |
|- ( ph -> ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) = X ) |
51 |
50 8
|
eqeltrd |
|- ( ph -> ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) e. LNoeM ) |
52 |
|
eqid |
|- ( 0g ` X ) = ( 0g ` X ) |
53 |
|
eqid |
|- ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) = ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) |
54 |
|
eqid |
|- ( Z |`s ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) ) = ( Z |`s ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) ) |
55 |
|
eqid |
|- ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) = ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) |
56 |
52 53 54 55
|
lmhmlnmsplit |
|- ( ( ( x e. ( Base ` Z ) |-> ( x |` A ) ) e. ( Z LMHom X ) /\ ( Z |`s ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) ) e. LNoeM /\ ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) e. LNoeM ) -> Z e. LNoeM ) |
57 |
18 42 51 56
|
syl3anc |
|- ( ph -> Z e. LNoeM ) |