Step |
Hyp |
Ref |
Expression |
1 |
|
snlindsntor.b |
⊢ 𝐵 = ( Base ‘ 𝑀 ) |
2 |
|
snlindsntor.r |
⊢ 𝑅 = ( Scalar ‘ 𝑀 ) |
3 |
|
snlindsntor.s |
⊢ 𝑆 = ( Base ‘ 𝑅 ) |
4 |
|
snlindsntor.0 |
⊢ 0 = ( 0g ‘ 𝑅 ) |
5 |
|
snlindsntor.z |
⊢ 𝑍 = ( 0g ‘ 𝑀 ) |
6 |
|
snlindsntor.t |
⊢ · = ( ·𝑠 ‘ 𝑀 ) |
7 |
|
eqidd |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → { 〈 𝑋 , 𝑠 〉 } = { 〈 𝑋 , 𝑠 〉 } ) |
8 |
|
fsng |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ) → ( { 〈 𝑋 , 𝑠 〉 } : { 𝑋 } ⟶ { 𝑠 } ↔ { 〈 𝑋 , 𝑠 〉 } = { 〈 𝑋 , 𝑠 〉 } ) ) |
9 |
8
|
adantll |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( { 〈 𝑋 , 𝑠 〉 } : { 𝑋 } ⟶ { 𝑠 } ↔ { 〈 𝑋 , 𝑠 〉 } = { 〈 𝑋 , 𝑠 〉 } ) ) |
10 |
7 9
|
mpbird |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → { 〈 𝑋 , 𝑠 〉 } : { 𝑋 } ⟶ { 𝑠 } ) |
11 |
|
snssi |
⊢ ( 𝑠 ∈ 𝑆 → { 𝑠 } ⊆ 𝑆 ) |
12 |
11
|
adantl |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → { 𝑠 } ⊆ 𝑆 ) |
13 |
10 12
|
fssd |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → { 〈 𝑋 , 𝑠 〉 } : { 𝑋 } ⟶ 𝑆 ) |
14 |
3
|
fvexi |
⊢ 𝑆 ∈ V |
15 |
|
snex |
⊢ { 𝑋 } ∈ V |
16 |
14 15
|
pm3.2i |
⊢ ( 𝑆 ∈ V ∧ { 𝑋 } ∈ V ) |
17 |
|
elmapg |
⊢ ( ( 𝑆 ∈ V ∧ { 𝑋 } ∈ V ) → ( { 〈 𝑋 , 𝑠 〉 } ∈ ( 𝑆 ↑m { 𝑋 } ) ↔ { 〈 𝑋 , 𝑠 〉 } : { 𝑋 } ⟶ 𝑆 ) ) |
18 |
16 17
|
mp1i |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( { 〈 𝑋 , 𝑠 〉 } ∈ ( 𝑆 ↑m { 𝑋 } ) ↔ { 〈 𝑋 , 𝑠 〉 } : { 𝑋 } ⟶ 𝑆 ) ) |
19 |
13 18
|
mpbird |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → { 〈 𝑋 , 𝑠 〉 } ∈ ( 𝑆 ↑m { 𝑋 } ) ) |
20 |
|
oveq1 |
⊢ ( 𝑓 = { 〈 𝑋 , 𝑠 〉 } → ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = ( { 〈 𝑋 , 𝑠 〉 } ( linC ‘ 𝑀 ) { 𝑋 } ) ) |
21 |
20
|
eqeq1d |
⊢ ( 𝑓 = { 〈 𝑋 , 𝑠 〉 } → ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ↔ ( { 〈 𝑋 , 𝑠 〉 } ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ) ) |
22 |
|
fveq1 |
⊢ ( 𝑓 = { 〈 𝑋 , 𝑠 〉 } → ( 𝑓 ‘ 𝑋 ) = ( { 〈 𝑋 , 𝑠 〉 } ‘ 𝑋 ) ) |
23 |
22
|
eqeq1d |
⊢ ( 𝑓 = { 〈 𝑋 , 𝑠 〉 } → ( ( 𝑓 ‘ 𝑋 ) = 0 ↔ ( { 〈 𝑋 , 𝑠 〉 } ‘ 𝑋 ) = 0 ) ) |
24 |
21 23
|
imbi12d |
⊢ ( 𝑓 = { 〈 𝑋 , 𝑠 〉 } → ( ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ↔ ( ( { 〈 𝑋 , 𝑠 〉 } ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( { 〈 𝑋 , 𝑠 〉 } ‘ 𝑋 ) = 0 ) ) ) |
25 |
1 2 3 6
|
lincvalsng |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ) → ( { 〈 𝑋 , 𝑠 〉 } ( linC ‘ 𝑀 ) { 𝑋 } ) = ( 𝑠 · 𝑋 ) ) |
26 |
25
|
3expa |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( { 〈 𝑋 , 𝑠 〉 } ( linC ‘ 𝑀 ) { 𝑋 } ) = ( 𝑠 · 𝑋 ) ) |
27 |
26
|
eqeq1d |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( ( { 〈 𝑋 , 𝑠 〉 } ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 ↔ ( 𝑠 · 𝑋 ) = 𝑍 ) ) |
28 |
|
fvsng |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑠 ∈ 𝑆 ) → ( { 〈 𝑋 , 𝑠 〉 } ‘ 𝑋 ) = 𝑠 ) |
29 |
28
|
adantll |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( { 〈 𝑋 , 𝑠 〉 } ‘ 𝑋 ) = 𝑠 ) |
30 |
29
|
eqeq1d |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( ( { 〈 𝑋 , 𝑠 〉 } ‘ 𝑋 ) = 0 ↔ 𝑠 = 0 ) ) |
31 |
27 30
|
imbi12d |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( ( ( { 〈 𝑋 , 𝑠 〉 } ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( { 〈 𝑋 , 𝑠 〉 } ‘ 𝑋 ) = 0 ) ↔ ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ) |
32 |
24 31
|
sylan9bbr |
⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑓 = { 〈 𝑋 , 𝑠 〉 } ) → ( ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) ↔ ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ) |
33 |
19 32
|
rspcdv |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) → ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ) |
34 |
33
|
ralrimdva |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑓 ∈ ( 𝑆 ↑m { 𝑋 } ) ( ( 𝑓 ( linC ‘ 𝑀 ) { 𝑋 } ) = 𝑍 → ( 𝑓 ‘ 𝑋 ) = 0 ) → ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 · 𝑋 ) = 𝑍 → 𝑠 = 0 ) ) ) |