Metamath Proof Explorer

Theorem lflsub

Description: Property of a linear functional. ( lnfnaddi analog.) (Contributed by NM, 18-Apr-2014)

Ref Expression
Hypotheses lflsub.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lflsub.m ⊢ 𝑀 = ( -g ‘ 𝐷 )
lflsub.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lflsub.a ⊢ − = ( -g ‘ 𝑊 )
lflsub.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
Assertion lflsub ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑋 − 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) 𝑀 ( 𝐺 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lflsub.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2 lflsub.m ⊢ 𝑀 = ( -g ‘ 𝐷 )
3 lflsub.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 lflsub.a ⊢ − = ( -g ‘ 𝑊 )
5 lflsub.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
7 simp3l ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑋 ∈ 𝑉 )
8 1 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Ring )
9 8 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐷 ∈ Ring )
10 ringgrp ⊢ ( 𝐷 ∈ Ring → 𝐷 ∈ Grp )
11 9 10 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐷 ∈ Grp )
12 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
13 eqid ⊢ ( 1r ‘ 𝐷 ) = ( 1r ‘ 𝐷 )
14 12 13 ringidcl ⊢ ( 𝐷 ∈ Ring → ( 1r ‘ 𝐷 ) ∈ ( Base ‘ 𝐷 ) )
15 9 14 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 1r ‘ 𝐷 ) ∈ ( Base ‘ 𝐷 ) )
16 eqid ⊢ ( invg ‘ 𝐷 ) = ( invg ‘ 𝐷 )
17 12 16 grpinvcl ⊢ ( ( 𝐷 ∈ Grp ∧ ( 1r ‘ 𝐷 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ∈ ( Base ‘ 𝐷 ) )
18 11 15 17 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ∈ ( Base ‘ 𝐷 ) )
19 simp3r ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑌 ∈ 𝑉 )
20 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
21 3 1 20 12 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑌 ∈ 𝑉 ) → ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
22 6 18 19 21 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
23 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
24 3 23 lmodcom ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = ( ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) )
25 6 7 22 24 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = ( ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) )
26 25 fveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ) = ( 𝐺 ‘ ( ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ) )
27 simp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐺 ∈ 𝐹 )
28 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
29 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
30 3 23 1 20 12 28 29 5 lfli ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ) = ( ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑌 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) )
31 6 27 18 19 7 30 syl113anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ) = ( ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑌 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) )
32 1 12 3 5 lflcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
33 32 3adant3l ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
34 12 29 13 16 9 33 ringnegl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑌 ) ) = ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) )
35 34 oveq1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑌 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) = ( ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) )
36 ringabl ⊢ ( 𝐷 ∈ Ring → 𝐷 ∈ Abel )
37 9 36 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝐷 ∈ Abel )
38 12 16 grpinvcl ⊢ ( ( 𝐷 ∈ Grp ∧ ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐷 ) )
39 11 33 38 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐷 ) )
40 1 12 3 5 lflcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
41 40 3adant3r ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
42 12 28 ablcom ⊢ ( ( 𝐷 ∈ Abel ∧ ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝐷 ) ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
43 37 39 41 42 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝐷 ) ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
44 35 43 eqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑌 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝐷 ) ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
45 26 31 44 3eqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ) = ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝐷 ) ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
46 3 23 4 1 20 16 13 lmodvsubval2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
47 6 7 19 46 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
48 47 fveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑋 − 𝑌 ) ) = ( 𝐺 ‘ ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐷 ) ‘ ( 1r ‘ 𝐷 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ) )
49 12 28 16 2 grpsubval ⊢ ( ( ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝐺 ‘ 𝑋 ) 𝑀 ( 𝐺 ‘ 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝐷 ) ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
50 41 33 49 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐺 ‘ 𝑋 ) 𝑀 ( 𝐺 ‘ 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( +g ‘ 𝐷 ) ( ( invg ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑌 ) ) ) )
51 45 48 50 3eqtr4d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑋 − 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) 𝑀 ( 𝐺 ‘ 𝑌 ) ) )