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