Step |
Hyp |
Ref |
Expression |
1 |
|
lflmul.d |
⊢ 𝐷 = ( Scalar ‘ 𝑊 ) |
2 |
|
lflmul.k |
⊢ 𝐾 = ( Base ‘ 𝐷 ) |
3 |
|
lflmul.t |
⊢ × = ( .r ‘ 𝐷 ) |
4 |
|
lflmul.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
5 |
|
lflmul.s |
⊢ · = ( ·𝑠 ‘ 𝑊 ) |
6 |
|
lflmul.f |
⊢ 𝐹 = ( LFnl ‘ 𝑊 ) |
7 |
|
simp1 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → 𝑊 ∈ LMod ) |
8 |
|
simp2 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → 𝐺 ∈ 𝐹 ) |
9 |
|
simp3l |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → 𝑅 ∈ 𝐾 ) |
10 |
|
simp3r |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → 𝑋 ∈ 𝑉 ) |
11 |
|
eqid |
⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 ) |
12 |
4 11
|
lmod0vcl |
⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝑊 ) ∈ 𝑉 ) |
13 |
12
|
3ad2ant1 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 0g ‘ 𝑊 ) ∈ 𝑉 ) |
14 |
|
eqid |
⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) |
15 |
|
eqid |
⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 ) |
16 |
4 14 1 5 2 15 3 6
|
lfli |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) ) ) |
17 |
7 8 9 10 13 16
|
syl113anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) ) ) |
18 |
4 1 5 2
|
lmodvscl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑅 · 𝑋 ) ∈ 𝑉 ) |
19 |
7 9 10 18
|
syl3anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑅 · 𝑋 ) ∈ 𝑉 ) |
20 |
4 14 11
|
lmod0vrid |
⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 · 𝑋 ) ∈ 𝑉 ) → ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 𝑅 · 𝑋 ) ) |
21 |
7 19 20
|
syl2anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 𝑅 · 𝑋 ) ) |
22 |
21
|
fveq2d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ) = ( 𝐺 ‘ ( 𝑅 · 𝑋 ) ) ) |
23 |
|
eqid |
⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 ) |
24 |
1 23 11 6
|
lfl0 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝐷 ) ) |
25 |
24
|
3adant3 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝐷 ) ) |
26 |
25
|
oveq2d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 0g ‘ 𝐷 ) ) ) |
27 |
1
|
lmodfgrp |
⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Grp ) |
28 |
27
|
3ad2ant1 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → 𝐷 ∈ Grp ) |
29 |
1 2 4 6
|
lflcl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ 𝐾 ) |
30 |
29
|
3adant3l |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑋 ) ∈ 𝐾 ) |
31 |
1 2 3
|
lmodmcl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑋 ) ∈ 𝐾 ) → ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐾 ) |
32 |
7 9 30 31
|
syl3anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐾 ) |
33 |
2 15 23
|
grprid |
⊢ ( ( 𝐷 ∈ Grp ∧ ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐾 ) → ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 0g ‘ 𝐷 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ) |
34 |
28 32 33
|
syl2anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 0g ‘ 𝐷 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ) |
35 |
26 34
|
eqtrd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ) |
36 |
17 22 35
|
3eqtr3d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑅 · 𝑋 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ) |