Step |
Hyp |
Ref |
Expression |
1 |
|
lfl0.d |
⊢ 𝐷 = ( Scalar ‘ 𝑊 ) |
2 |
|
lfl0.o |
⊢ 0 = ( 0g ‘ 𝐷 ) |
3 |
|
lfl0.z |
⊢ 𝑍 = ( 0g ‘ 𝑊 ) |
4 |
|
lfl0.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
5 |
|
simpl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝑊 ∈ LMod ) |
6 |
|
simpr |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 ∈ 𝐹 ) |
7 |
|
eqid |
⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) |
8 |
|
eqid |
⊢ ( 1r ‘ 𝐷 ) = ( 1r ‘ 𝐷 ) |
9 |
1 7 8
|
lmod1cl |
⊢ ( 𝑊 ∈ LMod → ( 1r ‘ 𝐷 ) ∈ ( Base ‘ 𝐷 ) ) |
10 |
9
|
adantr |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 1r ‘ 𝐷 ) ∈ ( Base ‘ 𝐷 ) ) |
11 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
12 |
11 3
|
lmod0vcl |
⊢ ( 𝑊 ∈ LMod → 𝑍 ∈ ( Base ‘ 𝑊 ) ) |
13 |
12
|
adantr |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝑍 ∈ ( Base ‘ 𝑊 ) ) |
14 |
|
eqid |
⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) |
15 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) |
16 |
|
eqid |
⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 ) |
17 |
|
eqid |
⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 ) |
18 |
11 14 1 15 7 16 17 4
|
lfli |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( ( 1r ‘ 𝐷 ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑍 ∈ ( Base ‘ 𝑊 ) ∧ 𝑍 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝐺 ‘ ( ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ( +g ‘ 𝑊 ) 𝑍 ) ) = ( ( ( 1r ‘ 𝐷 ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ) |
19 |
5 6 10 13 13 18
|
syl113anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ‘ ( ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ( +g ‘ 𝑊 ) 𝑍 ) ) = ( ( ( 1r ‘ 𝐷 ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ) |
20 |
11 1 15 7
|
lmodvscl |
⊢ ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ 𝐷 ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑍 ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ ( Base ‘ 𝑊 ) ) |
21 |
5 10 13 20
|
syl3anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ ( Base ‘ 𝑊 ) ) |
22 |
11 14 3
|
lmod0vrid |
⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ( +g ‘ 𝑊 ) 𝑍 ) = ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) |
23 |
21 22
|
syldan |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ( +g ‘ 𝑊 ) 𝑍 ) = ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) |
24 |
11 1 15 8
|
lmodvs1 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) = 𝑍 ) |
25 |
13 24
|
syldan |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) = 𝑍 ) |
26 |
23 25
|
eqtrd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ( +g ‘ 𝑊 ) 𝑍 ) = 𝑍 ) |
27 |
26
|
fveq2d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ‘ ( ( ( 1r ‘ 𝐷 ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ( +g ‘ 𝑊 ) 𝑍 ) ) = ( 𝐺 ‘ 𝑍 ) ) |
28 |
1
|
lmodring |
⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Ring ) |
29 |
28
|
adantr |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐷 ∈ Ring ) |
30 |
1 7 11 4
|
lflcl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑍 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐺 ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) ) |
31 |
13 30
|
mpd3an3 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) ) |
32 |
7 17 8
|
ringlidm |
⊢ ( ( 𝐷 ∈ Ring ∧ ( 𝐺 ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 1r ‘ 𝐷 ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) = ( 𝐺 ‘ 𝑍 ) ) |
33 |
29 31 32
|
syl2anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 1r ‘ 𝐷 ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) = ( 𝐺 ‘ 𝑍 ) ) |
34 |
33
|
oveq1d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( ( 1r ‘ 𝐷 ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) = ( ( 𝐺 ‘ 𝑍 ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ) |
35 |
19 27 34
|
3eqtr3d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ‘ 𝑍 ) = ( ( 𝐺 ‘ 𝑍 ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ) |
36 |
35
|
oveq1d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐺 ‘ 𝑍 ) ( -g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) = ( ( ( 𝐺 ‘ 𝑍 ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ( -g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ) |
37 |
|
ringgrp |
⊢ ( 𝐷 ∈ Ring → 𝐷 ∈ Grp ) |
38 |
29 37
|
syl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐷 ∈ Grp ) |
39 |
|
eqid |
⊢ ( -g ‘ 𝐷 ) = ( -g ‘ 𝐷 ) |
40 |
7 2 39
|
grpsubid |
⊢ ( ( 𝐷 ∈ Grp ∧ ( 𝐺 ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝐺 ‘ 𝑍 ) ( -g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) = 0 ) |
41 |
38 31 40
|
syl2anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐺 ‘ 𝑍 ) ( -g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) = 0 ) |
42 |
7 16 39
|
grppncan |
⊢ ( ( 𝐷 ∈ Grp ∧ ( 𝐺 ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺 ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝐺 ‘ 𝑍 ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ( -g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) = ( 𝐺 ‘ 𝑍 ) ) |
43 |
38 31 31 42
|
syl3anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( ( 𝐺 ‘ 𝑍 ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) ( -g ‘ 𝐷 ) ( 𝐺 ‘ 𝑍 ) ) = ( 𝐺 ‘ 𝑍 ) ) |
44 |
36 41 43
|
3eqtr3rd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ‘ 𝑍 ) = 0 ) |