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