Metamath Proof Explorer

Theorem frlmsplit2

Description: Restriction is homomorphic on free modules. (Contributed by Stefan O'Rear, 3-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmsplit2.y 
|- Y = ( R freeLMod U )
frlmsplit2.z 
|- Z = ( R freeLMod V )
frlmsplit2.b 
|- B = ( Base ` Y )
frlmsplit2.c 
|- C = ( Base ` Z )
frlmsplit2.f 
|- F = ( x e. B |-> ( x |` V ) )
Assertion frlmsplit2 
|- ( ( R e. Ring /\ U e. X /\ V C_ U ) -> F e. ( Y LMHom Z ) )

Proof

Step Hyp Ref Expression
1 frlmsplit2.y 
 |-  Y = ( R freeLMod U )
2 frlmsplit2.z 
 |-  Z = ( R freeLMod V )
3 frlmsplit2.b 
 |-  B = ( Base ` Y )
4 frlmsplit2.c 
 |-  C = ( Base ` Z )
5 frlmsplit2.f 
 |-  F = ( x e. B |-> ( x |` V ) )
6 simp1 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> R e. Ring )
7 simp2 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> U e. X )
8 eqid 
 |-  ( LSubSp ` ( ( ringLMod ` R ) ^s U ) ) = ( LSubSp ` ( ( ringLMod ` R ) ^s U ) )
9 1 3 8 frlmlss 
 |-  ( ( R e. Ring /\ U e. X ) -> B e. ( LSubSp ` ( ( ringLMod ` R ) ^s U ) ) )
10 6 7 9 syl2anc 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> B e. ( LSubSp ` ( ( ringLMod ` R ) ^s U ) ) )
11 eqid 
 |-  ( Base ` ( ( ringLMod ` R ) ^s U ) ) = ( Base ` ( ( ringLMod ` R ) ^s U ) )
12 11 8 lssss 
 |-  ( B e. ( LSubSp ` ( ( ringLMod ` R ) ^s U ) ) -> B C_ ( Base ` ( ( ringLMod ` R ) ^s U ) ) )
13 resmpt 
 |-  ( B C_ ( Base ` ( ( ringLMod ` R ) ^s U ) ) -> ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) = ( x e. B |-> ( x |` V ) ) )
14 10 12 13 3syl 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) = ( x e. B |-> ( x |` V ) ) )
15 14 5 eqtr4di 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) = F )
16 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
17 eqid 
 |-  ( ( ringLMod ` R ) ^s U ) = ( ( ringLMod ` R ) ^s U )
18 eqid 
 |-  ( ( ringLMod ` R ) ^s V ) = ( ( ringLMod ` R ) ^s V )
19 eqid 
 |-  ( Base ` ( ( ringLMod ` R ) ^s V ) ) = ( Base ` ( ( ringLMod ` R ) ^s V ) )
20 eqid 
 |-  ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) = ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) )
21 17 18 11 19 20 pwssplit3 
 |-  ( ( ( ringLMod ` R ) e. LMod /\ U e. X /\ V C_ U ) -> ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) e. ( ( ( ringLMod ` R ) ^s U ) LMHom ( ( ringLMod ` R ) ^s V ) ) )
22 16 21 syl3an1 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) e. ( ( ( ringLMod ` R ) ^s U ) LMHom ( ( ringLMod ` R ) ^s V ) ) )
23 eqid 
 |-  ( ( ( ringLMod ` R ) ^s U ) |`s B ) = ( ( ( ringLMod ` R ) ^s U ) |`s B )
24 8 23 reslmhm 
 |-  ( ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) e. ( ( ( ringLMod ` R ) ^s U ) LMHom ( ( ringLMod ` R ) ^s V ) ) /\ B e. ( LSubSp ` ( ( ringLMod ` R ) ^s U ) ) ) -> ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) e. ( ( ( ( ringLMod ` R ) ^s U ) |`s B ) LMHom ( ( ringLMod ` R ) ^s V ) ) )
25 22 10 24 syl2anc 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) e. ( ( ( ( ringLMod ` R ) ^s U ) |`s B ) LMHom ( ( ringLMod ` R ) ^s V ) ) )
26 16 3ad2ant1 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( ringLMod ` R ) e. LMod )
27 simp3 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> V C_ U )
28 7 27 ssexd 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> V e. _V )
29 18 pwslmod 
 |-  ( ( ( ringLMod ` R ) e. LMod /\ V e. _V ) -> ( ( ringLMod ` R ) ^s V ) e. LMod )
30 26 28 29 syl2anc 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( ( ringLMod ` R ) ^s V ) e. LMod )
31 eqid 
 |-  ( LSubSp ` ( ( ringLMod ` R ) ^s V ) ) = ( LSubSp ` ( ( ringLMod ` R ) ^s V ) )
32 2 4 31 frlmlss 
 |-  ( ( R e. Ring /\ V e. _V ) -> C e. ( LSubSp ` ( ( ringLMod ` R ) ^s V ) ) )
33 6 28 32 syl2anc 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> C e. ( LSubSp ` ( ( ringLMod ` R ) ^s V ) ) )
34 14 rneqd 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ran ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) = ran ( x e. B |-> ( x |` V ) ) )
35 eqid 
 |-  ( Base ` R ) = ( Base ` R )
36 1 35 3 frlmbasf 
 |-  ( ( U e. X /\ x e. B ) -> x : U --> ( Base ` R ) )
37 7 36 sylan 
 |-  ( ( ( R e. Ring /\ U e. X /\ V C_ U ) /\ x e. B ) -> x : U --> ( Base ` R ) )
38 simpl3 
 |-  ( ( ( R e. Ring /\ U e. X /\ V C_ U ) /\ x e. B ) -> V C_ U )
39 37 38 fssresd 
 |-  ( ( ( R e. Ring /\ U e. X /\ V C_ U ) /\ x e. B ) -> ( x |` V ) : V --> ( Base ` R ) )
40 fvex 
 |-  ( Base ` R ) e. _V
41 elmapg 
 |-  ( ( ( Base ` R ) e. _V /\ V e. _V ) -> ( ( x |` V ) e. ( ( Base ` R ) ^m V ) <-> ( x |` V ) : V --> ( Base ` R ) ) )
42 40 28 41 sylancr 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( ( x |` V ) e. ( ( Base ` R ) ^m V ) <-> ( x |` V ) : V --> ( Base ` R ) ) )
43 42 adantr 
 |-  ( ( ( R e. Ring /\ U e. X /\ V C_ U ) /\ x e. B ) -> ( ( x |` V ) e. ( ( Base ` R ) ^m V ) <-> ( x |` V ) : V --> ( Base ` R ) ) )
44 39 43 mpbird 
 |-  ( ( ( R e. Ring /\ U e. X /\ V C_ U ) /\ x e. B ) -> ( x |` V ) e. ( ( Base ` R ) ^m V ) )
45 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
46 1 45 3 frlmbasfsupp 
 |-  ( ( U e. X /\ x e. B ) -> x finSupp ( 0g ` R ) )
47 7 46 sylan 
 |-  ( ( ( R e. Ring /\ U e. X /\ V C_ U ) /\ x e. B ) -> x finSupp ( 0g ` R ) )
48 fvexd 
 |-  ( ( ( R e. Ring /\ U e. X /\ V C_ U ) /\ x e. B ) -> ( 0g ` R ) e. _V )
49 47 48 fsuppres 
 |-  ( ( ( R e. Ring /\ U e. X /\ V C_ U ) /\ x e. B ) -> ( x |` V ) finSupp ( 0g ` R ) )
50 2 35 45 4 frlmelbas 
 |-  ( ( R e. Ring /\ V e. _V ) -> ( ( x |` V ) e. C <-> ( ( x |` V ) e. ( ( Base ` R ) ^m V ) /\ ( x |` V ) finSupp ( 0g ` R ) ) ) )
51 6 28 50 syl2anc 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( ( x |` V ) e. C <-> ( ( x |` V ) e. ( ( Base ` R ) ^m V ) /\ ( x |` V ) finSupp ( 0g ` R ) ) ) )
52 51 adantr 
 |-  ( ( ( R e. Ring /\ U e. X /\ V C_ U ) /\ x e. B ) -> ( ( x |` V ) e. C <-> ( ( x |` V ) e. ( ( Base ` R ) ^m V ) /\ ( x |` V ) finSupp ( 0g ` R ) ) ) )
53 44 49 52 mpbir2and 
 |-  ( ( ( R e. Ring /\ U e. X /\ V C_ U ) /\ x e. B ) -> ( x |` V ) e. C )
54 53 fmpttd 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( x e. B |-> ( x |` V ) ) : B --> C )
55 54 frnd 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ran ( x e. B |-> ( x |` V ) ) C_ C )
56 34 55 eqsstrd 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ran ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) C_ C )
57 eqid 
 |-  ( ( ( ringLMod ` R ) ^s V ) |`s C ) = ( ( ( ringLMod ` R ) ^s V ) |`s C )
58 57 31 reslmhm2b 
 |-  ( ( ( ( ringLMod ` R ) ^s V ) e. LMod /\ C e. ( LSubSp ` ( ( ringLMod ` R ) ^s V ) ) /\ ran ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) C_ C ) -> ( ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) e. ( ( ( ( ringLMod ` R ) ^s U ) |`s B ) LMHom ( ( ringLMod ` R ) ^s V ) ) <-> ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) e. ( ( ( ( ringLMod ` R ) ^s U ) |`s B ) LMHom ( ( ( ringLMod ` R ) ^s V ) |`s C ) ) ) )
59 30 33 56 58 syl3anc 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) e. ( ( ( ( ringLMod ` R ) ^s U ) |`s B ) LMHom ( ( ringLMod ` R ) ^s V ) ) <-> ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) e. ( ( ( ( ringLMod ` R ) ^s U ) |`s B ) LMHom ( ( ( ringLMod ` R ) ^s V ) |`s C ) ) ) )
60 25 59 mpbid 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( ( x e. ( Base ` ( ( ringLMod ` R ) ^s U ) ) |-> ( x |` V ) ) |` B ) e. ( ( ( ( ringLMod ` R ) ^s U ) |`s B ) LMHom ( ( ( ringLMod ` R ) ^s V ) |`s C ) ) )
61 15 60 eqeltrrd 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> F e. ( ( ( ( ringLMod ` R ) ^s U ) |`s B ) LMHom ( ( ( ringLMod ` R ) ^s V ) |`s C ) ) )
62 1 3 frlmpws 
 |-  ( ( R e. Ring /\ U e. X ) -> Y = ( ( ( ringLMod ` R ) ^s U ) |`s B ) )
63 6 7 62 syl2anc 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> Y = ( ( ( ringLMod ` R ) ^s U ) |`s B ) )
64 2 4 frlmpws 
 |-  ( ( R e. Ring /\ V e. _V ) -> Z = ( ( ( ringLMod ` R ) ^s V ) |`s C ) )
65 6 28 64 syl2anc 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> Z = ( ( ( ringLMod ` R ) ^s V ) |`s C ) )
66 63 65 oveq12d 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> ( Y LMHom Z ) = ( ( ( ( ringLMod ` R ) ^s U ) |`s B ) LMHom ( ( ( ringLMod ` R ) ^s V ) |`s C ) ) )
67 61 66 eleqtrrd 
 |-  ( ( R e. Ring /\ U e. X /\ V C_ U ) -> F e. ( Y LMHom Z ) )