Metamath Proof Explorer

Theorem pwssplit3

Description: Splitting for structure powers, part 3: restriction is a module homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses pwssplit1.y 
|- Y = ( W ^s U )
pwssplit1.z 
|- Z = ( W ^s V )
pwssplit1.b 
|- B = ( Base ` Y )
pwssplit1.c 
|- C = ( Base ` Z )
pwssplit1.f 
|- F = ( x e. B |-> ( x |` V ) )
Assertion pwssplit3 
|- ( ( W e. LMod /\ U e. X /\ V C_ U ) -> F e. ( Y LMHom Z ) )

Proof

Step Hyp Ref Expression
1 pwssplit1.y 
 |-  Y = ( W ^s U )
2 pwssplit1.z 
 |-  Z = ( W ^s V )
3 pwssplit1.b 
 |-  B = ( Base ` Y )
4 pwssplit1.c 
 |-  C = ( Base ` Z )
5 pwssplit1.f 
 |-  F = ( x e. B |-> ( x |` V ) )
6 eqid 
 |-  ( .s ` Y ) = ( .s ` Y )
7 eqid 
 |-  ( .s ` Z ) = ( .s ` Z )
8 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
9 eqid 
 |-  ( Scalar ` Z ) = ( Scalar ` Z )
10 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
11 simp1 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> W e. LMod )
12 simp2 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> U e. X )
13 1 pwslmod 
 |-  ( ( W e. LMod /\ U e. X ) -> Y e. LMod )
14 11 12 13 syl2anc 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> Y e. LMod )
15 simp3 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> V C_ U )
16 12 15 ssexd 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> V e. _V )
17 2 pwslmod 
 |-  ( ( W e. LMod /\ V e. _V ) -> Z e. LMod )
18 11 16 17 syl2anc 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> Z e. LMod )
19 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
20 2 19 pwssca 
 |-  ( ( W e. LMod /\ V e. _V ) -> ( Scalar ` W ) = ( Scalar ` Z ) )
21 11 16 20 syl2anc 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> ( Scalar ` W ) = ( Scalar ` Z ) )
22 1 19 pwssca 
 |-  ( ( W e. LMod /\ U e. X ) -> ( Scalar ` W ) = ( Scalar ` Y ) )
23 11 12 22 syl2anc 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> ( Scalar ` W ) = ( Scalar ` Y ) )
24 21 23 eqtr3d 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> ( Scalar ` Z ) = ( Scalar ` Y ) )
25 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
26 1 2 3 4 5 pwssplit2 
 |-  ( ( W e. Grp /\ U e. X /\ V C_ U ) -> F e. ( Y GrpHom Z ) )
27 25 26 syl3an1 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> F e. ( Y GrpHom Z ) )
28 snex 
 |-  { a } e. _V
29 xpexg 
 |-  ( ( U e. X /\ { a } e. _V ) -> ( U X. { a } ) e. _V )
30 12 28 29 sylancl 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> ( U X. { a } ) e. _V )
31 vex 
 |-  b e. _V
32 offres 
 |-  ( ( ( U X. { a } ) e. _V /\ b e. _V ) -> ( ( ( U X. { a } ) oF ( .s ` W ) b ) |` V ) = ( ( ( U X. { a } ) |` V ) oF ( .s ` W ) ( b |` V ) ) )
33 30 31 32 sylancl 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> ( ( ( U X. { a } ) oF ( .s ` W ) b ) |` V ) = ( ( ( U X. { a } ) |` V ) oF ( .s ` W ) ( b |` V ) ) )
34 33 adantr 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( ( ( U X. { a } ) oF ( .s ` W ) b ) |` V ) = ( ( ( U X. { a } ) |` V ) oF ( .s ` W ) ( b |` V ) ) )
35 xpssres 
 |-  ( V C_ U -> ( ( U X. { a } ) |` V ) = ( V X. { a } ) )
36 35 3ad2ant3 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> ( ( U X. { a } ) |` V ) = ( V X. { a } ) )
37 36 adantr 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( ( U X. { a } ) |` V ) = ( V X. { a } ) )
38 37 oveq1d 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( ( ( U X. { a } ) |` V ) oF ( .s ` W ) ( b |` V ) ) = ( ( V X. { a } ) oF ( .s ` W ) ( b |` V ) ) )
39 34 38 eqtrd 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( ( ( U X. { a } ) oF ( .s ` W ) b ) |` V ) = ( ( V X. { a } ) oF ( .s ` W ) ( b |` V ) ) )
40 eqid 
 |-  ( .s ` W ) = ( .s ` W )
41 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
42 simpl1 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> W e. LMod )
43 simpl2 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> U e. X )
44 23 fveq2d 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` Y ) ) )
45 44 eleq2d 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> ( a e. ( Base ` ( Scalar ` W ) ) <-> a e. ( Base ` ( Scalar ` Y ) ) ) )
46 45 biimpar 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ a e. ( Base ` ( Scalar ` Y ) ) ) -> a e. ( Base ` ( Scalar ` W ) ) )
47 46 adantrr 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> a e. ( Base ` ( Scalar ` W ) ) )
48 simprr 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> b e. B )
49 1 3 40 6 19 41 42 43 47 48 pwsvscafval 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( a ( .s ` Y ) b ) = ( ( U X. { a } ) oF ( .s ` W ) b ) )
50 49 reseq1d 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( ( a ( .s ` Y ) b ) |` V ) = ( ( ( U X. { a } ) oF ( .s ` W ) b ) |` V ) )
51 5 fvtresfn 
 |-  ( b e. B -> ( F ` b ) = ( b |` V ) )
52 51 ad2antll 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( F ` b ) = ( b |` V ) )
53 52 oveq2d 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( ( V X. { a } ) oF ( .s ` W ) ( F ` b ) ) = ( ( V X. { a } ) oF ( .s ` W ) ( b |` V ) ) )
54 39 50 53 3eqtr4d 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( ( a ( .s ` Y ) b ) |` V ) = ( ( V X. { a } ) oF ( .s ` W ) ( F ` b ) ) )
55 3 8 6 10 lmodvscl 
 |-  ( ( Y e. LMod /\ a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) -> ( a ( .s ` Y ) b ) e. B )
56 55 3expb 
 |-  ( ( Y e. LMod /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( a ( .s ` Y ) b ) e. B )
57 14 56 sylan 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( a ( .s ` Y ) b ) e. B )
58 5 fvtresfn 
 |-  ( ( a ( .s ` Y ) b ) e. B -> ( F ` ( a ( .s ` Y ) b ) ) = ( ( a ( .s ` Y ) b ) |` V ) )
59 57 58 syl 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( F ` ( a ( .s ` Y ) b ) ) = ( ( a ( .s ` Y ) b ) |` V ) )
60 16 adantr 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> V e. _V )
61 1 2 3 4 5 pwssplit0 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> F : B --> C )
62 61 ffvelrnda 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ b e. B ) -> ( F ` b ) e. C )
63 62 adantrl 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( F ` b ) e. C )
64 2 4 40 7 19 41 42 60 47 63 pwsvscafval 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( a ( .s ` Z ) ( F ` b ) ) = ( ( V X. { a } ) oF ( .s ` W ) ( F ` b ) ) )
65 54 59 64 3eqtr4d 
 |-  ( ( ( W e. LMod /\ U e. X /\ V C_ U ) /\ ( a e. ( Base ` ( Scalar ` Y ) ) /\ b e. B ) ) -> ( F ` ( a ( .s ` Y ) b ) ) = ( a ( .s ` Z ) ( F ` b ) ) )
66 3 6 7 8 9 10 14 18 24 27 65 islmhmd 
 |-  ( ( W e. LMod /\ U e. X /\ V C_ U ) -> F e. ( Y LMHom Z ) )