Step |
Hyp |
Ref |
Expression |
1 |
|
lincvalsn.b |
⊢ 𝐵 = ( Base ‘ 𝑀 ) |
2 |
|
lincvalsn.s |
⊢ 𝑆 = ( Scalar ‘ 𝑀 ) |
3 |
|
lincvalsn.r |
⊢ 𝑅 = ( Base ‘ 𝑆 ) |
4 |
|
lincvalsn.t |
⊢ · = ( ·𝑠 ‘ 𝑀 ) |
5 |
|
simp1 |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑀 ∈ LMod ) |
6 |
|
simp2 |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑉 ∈ 𝐵 ) |
7 |
2
|
fveq2i |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) |
8 |
3 7
|
eqtri |
⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) ) |
9 |
8
|
eleq2i |
⊢ ( 𝑌 ∈ 𝑅 ↔ 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) |
10 |
9
|
biimpi |
⊢ ( 𝑌 ∈ 𝑅 → 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) |
11 |
10
|
3ad2ant3 |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) |
12 |
|
fvexd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ) |
13 |
|
eqid |
⊢ { 〈 𝑉 , 𝑌 〉 } = { 〈 𝑉 , 𝑌 〉 } |
14 |
13
|
mapsnop |
⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ) → { 〈 𝑉 , 𝑌 〉 } ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m { 𝑉 } ) ) |
15 |
6 11 12 14
|
syl3anc |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → { 〈 𝑉 , 𝑌 〉 } ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m { 𝑉 } ) ) |
16 |
|
snelpwi |
⊢ ( 𝑉 ∈ ( Base ‘ 𝑀 ) → { 𝑉 } ∈ 𝒫 ( Base ‘ 𝑀 ) ) |
17 |
16 1
|
eleq2s |
⊢ ( 𝑉 ∈ 𝐵 → { 𝑉 } ∈ 𝒫 ( Base ‘ 𝑀 ) ) |
18 |
17
|
3ad2ant2 |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → { 𝑉 } ∈ 𝒫 ( Base ‘ 𝑀 ) ) |
19 |
|
lincval |
⊢ ( ( 𝑀 ∈ LMod ∧ { 〈 𝑉 , 𝑌 〉 } ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m { 𝑉 } ) ∧ { 𝑉 } ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( { 〈 𝑉 , 𝑌 〉 } ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 } ↦ ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ) |
20 |
5 15 18 19
|
syl3anc |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { 〈 𝑉 , 𝑌 〉 } ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 } ↦ ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ) |
21 |
|
lmodgrp |
⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp ) |
22 |
|
grpmnd |
⊢ ( 𝑀 ∈ Grp → 𝑀 ∈ Mnd ) |
23 |
21 22
|
syl |
⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Mnd ) |
24 |
23
|
3ad2ant1 |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑀 ∈ Mnd ) |
25 |
|
fvsng |
⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑉 ) = 𝑌 ) |
26 |
25
|
3adant1 |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑉 ) = 𝑌 ) |
27 |
26
|
oveq1d |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ) |
28 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 ) |
29 |
1 2 28 3
|
lmodvscl |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝑅 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 ) |
30 |
29
|
3com23 |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 ) |
31 |
27 30
|
eqeltrd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 ) |
32 |
|
fveq2 |
⊢ ( 𝑣 = 𝑉 → ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑣 ) = ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑉 ) ) |
33 |
|
id |
⊢ ( 𝑣 = 𝑉 → 𝑣 = 𝑉 ) |
34 |
32 33
|
oveq12d |
⊢ ( 𝑣 = 𝑉 → ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ) |
35 |
1 34
|
gsumsn |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝐵 ∧ ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 } ↦ ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ) |
36 |
24 6 31 35
|
syl3anc |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 } ↦ ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ) |
37 |
4
|
eqcomi |
⊢ ( ·𝑠 ‘ 𝑀 ) = · |
38 |
37
|
a1i |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ·𝑠 ‘ 𝑀 ) = · ) |
39 |
|
eqidd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑉 = 𝑉 ) |
40 |
38 26 39
|
oveq123d |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( ( { 〈 𝑉 , 𝑌 〉 } ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 𝑌 · 𝑉 ) ) |
41 |
20 36 40
|
3eqtrd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( { 〈 𝑉 , 𝑌 〉 } ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 𝑌 · 𝑉 ) ) |