This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑌 = ( 𝑅 freeLMod 𝑈 )
frlmsplit2.z ⊢ 𝑍 = ( 𝑅 freeLMod 𝑉 )
frlmsplit2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
frlmsplit2.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
frlmsplit2.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) )
Assertion frlmsplit2 ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 ∈ ( 𝑌 LMHom 𝑍 ) )

Proof

Step Hyp Ref Expression
1 frlmsplit2.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝑈 )
2 frlmsplit2.z ⊢ 𝑍 = ( 𝑅 freeLMod 𝑉 )
3 frlmsplit2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
4 frlmsplit2.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
5 frlmsplit2.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) )
6 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑅 ∈ Ring )
7 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑈 ∈ 𝑋 )
8 eqid ⊢ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) = ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) )
9 1 3 8 frlmlss ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ) → 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) )
10 6 7 9 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) )
11 eqid ⊢ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) )
12 11 8 lssss ⊢ ( 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) → 𝐵 ⊆ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) )
13 resmpt ⊢ ( 𝐵 ⊆ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) → ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) ) )
14 10 12 13 3syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) ) )
15 14 5 eqtr4di ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) = 𝐹 )
16 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
17 eqid ⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 )
18 eqid ⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 )
19 eqid ⊢ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) )
20 eqid ⊢ ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) = ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) )
21 17 18 11 19 20 pwssplit3 ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ∈ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) LMHom ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) )
22 16 21 syl3an1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ∈ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) LMHom ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) )
23 eqid ⊢ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 )
24 8 23 reslmhm ⊢ ( ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ∈ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) LMHom ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) ∧ 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ) → ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) ∈ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) LMHom ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) )
25 22 10 24 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) ∈ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) LMHom ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) )
26 16 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ringLMod ‘ 𝑅 ) ∈ LMod )
27 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ⊆ 𝑈 )
28 7 27 ssexd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ∈ V )
29 18 pwslmod ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝑉 ∈ V ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ∈ LMod )
30 26 28 29 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ∈ LMod )
31 eqid ⊢ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) = ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) )
32 2 4 31 frlmlss ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑉 ∈ V ) → 𝐶 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) )
33 6 28 32 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐶 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) )
34 14 rneqd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ran ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) = ran ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) ) )
35 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
36 1 35 3 frlmbasf ⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 : 𝑈 ⟶ ( Base ‘ 𝑅 ) )
37 7 36 sylan ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 : 𝑈 ⟶ ( Base ‘ 𝑅 ) )
38 simpl3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑉 ⊆ 𝑈 )
39 37 38 fssresd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ↾ 𝑉 ) : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
40 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
41 elmapg ⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ 𝑉 ∈ V ) → ( ( 𝑥 ↾ 𝑉 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑉 ) ↔ ( 𝑥 ↾ 𝑉 ) : 𝑉 ⟶ ( Base ‘ 𝑅 ) ) )
42 40 28 41 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑥 ↾ 𝑉 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑉 ) ↔ ( 𝑥 ↾ 𝑉 ) : 𝑉 ⟶ ( Base ‘ 𝑅 ) ) )
43 42 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ↾ 𝑉 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑉 ) ↔ ( 𝑥 ↾ 𝑉 ) : 𝑉 ⟶ ( Base ‘ 𝑅 ) ) )
44 39 43 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ↾ 𝑉 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑉 ) )
45 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
46 1 45 3 frlmbasfsupp ⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 finSupp ( 0g ‘ 𝑅 ) )
47 7 46 sylan ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 finSupp ( 0g ‘ 𝑅 ) )
48 fvexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → ( 0g ‘ 𝑅 ) ∈ V )
49 47 48 fsuppres ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ↾ 𝑉 ) finSupp ( 0g ‘ 𝑅 ) )
50 2 35 45 4 frlmelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑉 ∈ V ) → ( ( 𝑥 ↾ 𝑉 ) ∈ 𝐶 ↔ ( ( 𝑥 ↾ 𝑉 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑉 ) ∧ ( 𝑥 ↾ 𝑉 ) finSupp ( 0g ‘ 𝑅 ) ) ) )
51 6 28 50 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑥 ↾ 𝑉 ) ∈ 𝐶 ↔ ( ( 𝑥 ↾ 𝑉 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑉 ) ∧ ( 𝑥 ↾ 𝑉 ) finSupp ( 0g ‘ 𝑅 ) ) ) )
52 51 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ↾ 𝑉 ) ∈ 𝐶 ↔ ( ( 𝑥 ↾ 𝑉 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑉 ) ∧ ( 𝑥 ↾ 𝑉 ) finSupp ( 0g ‘ 𝑅 ) ) ) )
53 44 49 52 mpbir2and ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ↾ 𝑉 ) ∈ 𝐶 )
54 53 fmpttd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) ) : 𝐵 ⟶ 𝐶 )
55 54 frnd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ran ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) ) ⊆ 𝐶 )
56 34 55 eqsstrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ran ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) ⊆ 𝐶 )
57 eqid ⊢ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ↾s 𝐶 ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ↾s 𝐶 )
58 57 31 reslmhm2b ⊢ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ∈ LMod ∧ 𝐶 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) ∧ ran ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) ⊆ 𝐶 ) → ( ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) ∈ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) LMHom ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) ↔ ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) ∈ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) LMHom ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ↾s 𝐶 ) ) ) )
59 30 33 56 58 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) ∈ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) LMHom ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ) ↔ ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) ∈ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) LMHom ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ↾s 𝐶 ) ) ) )
60 25 59 mpbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ) ↦ ( 𝑥 ↾ 𝑉 ) ) ↾ 𝐵 ) ∈ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) LMHom ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ↾s 𝐶 ) ) )
61 15 60 eqeltrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 ∈ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) LMHom ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ↾s 𝐶 ) ) )
62 1 3 frlmpws ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ) → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) )
63 6 7 62 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) )
64 2 4 frlmpws ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑉 ∈ V ) → 𝑍 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ↾s 𝐶 ) )
65 6 28 64 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑍 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ↾s 𝐶 ) )
66 63 65 oveq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑌 LMHom 𝑍 ) = ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑈 ) ↾s 𝐵 ) LMHom ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝑉 ) ↾s 𝐶 ) ) )
67 61 66 eleqtrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 ∈ ( 𝑌 LMHom 𝑍 ) )