Metamath Proof Explorer

Theorem frlmsubgval

Description: Subtraction in a free module. (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypotheses frlmsubval.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
frlmsubval.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
frlmsubval.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
frlmsubval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
frlmsubval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
frlmsubval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
frlmsubval.a ⊢ − = ( -g ‘ 𝑅 )
frlmsubval.p ⊢ 𝑀 = ( -g ‘ 𝑌 )
Assertion frlmsubgval ( 𝜑 → ( 𝐹 𝑀 𝐺 ) = ( 𝐹 ∘f − 𝐺 ) )

Proof

Step Hyp Ref Expression
1 frlmsubval.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
2 frlmsubval.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 frlmsubval.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 frlmsubval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 frlmsubval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
6 frlmsubval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
7 frlmsubval.a ⊢ − = ( -g ‘ 𝑅 )
8 frlmsubval.p ⊢ 𝑀 = ( -g ‘ 𝑌 )
9 1 2 frlmpws ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
10 3 4 9 syl2anc ⊢ ( 𝜑 → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
11 10 fveq2d ⊢ ( 𝜑 → ( -g ‘ 𝑌 ) = ( -g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
12 8 11 syl5eq ⊢ ( 𝜑 → 𝑀 = ( -g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
13 12 oveqd ⊢ ( 𝜑 → ( 𝐹 𝑀 𝐺 ) = ( 𝐹 ( -g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) 𝐺 ) )
14 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
15 3 14 syl ⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ LMod )
16 eqid ⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
17 16 pwslmod ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ 𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod )
18 15 4 17 syl2anc ⊢ ( 𝜑 → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod )
19 eqid ⊢ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
20 1 2 19 frlmlss ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
21 3 4 20 syl2anc ⊢ ( 𝜑 → 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
22 19 lsssubg ⊢ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod ∧ 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) → 𝐵 ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
23 18 21 22 syl2anc ⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
24 eqid ⊢ ( -g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( -g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
25 eqid ⊢ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 )
26 eqid ⊢ ( -g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) = ( -g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
27 24 25 26 subgsub ⊢ ( ( 𝐵 ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ( -g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝐺 ) = ( 𝐹 ( -g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) 𝐺 ) )
28 23 5 6 27 syl3anc ⊢ ( 𝜑 → ( 𝐹 ( -g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝐺 ) = ( 𝐹 ( -g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) 𝐺 ) )
29 lmodgrp ⊢ ( ( ringLMod ‘ 𝑅 ) ∈ LMod → ( ringLMod ‘ 𝑅 ) ∈ Grp )
30 3 14 29 3syl ⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ Grp )
31 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
32 1 31 2 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝐹 ∈ 𝐵 ) → 𝐹 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
33 4 5 32 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
34 rlmbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
35 16 34 pwsbas ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ Grp ∧ 𝐼 ∈ 𝑊 ) → ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
36 30 4 35 syl2anc ⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
37 33 36 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
38 1 31 2 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
39 4 6 38 syl2anc ⊢ ( 𝜑 → 𝐺 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
40 39 36 eleqtrd ⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
41 eqid ⊢ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
42 rlmsub ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ ( ringLMod ‘ 𝑅 ) )
43 7 42 eqtri ⊢ − = ( -g ‘ ( ringLMod ‘ 𝑅 ) )
44 16 41 43 24 pwssub ⊢ ( ( ( ( ringLMod ‘ 𝑅 ) ∈ Grp ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝐹 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ∧ 𝐺 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) ) → ( 𝐹 ( -g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝐺 ) = ( 𝐹 ∘f − 𝐺 ) )
45 30 4 37 40 44 syl22anc ⊢ ( 𝜑 → ( 𝐹 ( -g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝐺 ) = ( 𝐹 ∘f − 𝐺 ) )
46 13 28 45 3eqtr2d ⊢ ( 𝜑 → ( 𝐹 𝑀 𝐺 ) = ( 𝐹 ∘f − 𝐺 ) )