Step |
Hyp |
Ref |
Expression |
1 |
|
lcdlssvscl.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
lcdlssvscl.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
lcdlssvscl.f |
⊢ 𝐹 = ( Scalar ‘ 𝑈 ) |
4 |
|
lcdlssvscl.r |
⊢ 𝑅 = ( Base ‘ 𝐹 ) |
5 |
|
lcdlssvscl.c |
⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
|
lcdlssvscl.v |
⊢ 𝑉 = ( Base ‘ 𝐶 ) |
7 |
|
lcdlssvscl.t |
⊢ · = ( ·𝑠 ‘ 𝐶 ) |
8 |
|
lcdlssvscl.s |
⊢ 𝑆 = ( LSubSp ‘ 𝐶 ) |
9 |
|
lcdlssvscl.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
10 |
|
lcdlssvscl.l |
⊢ ( 𝜑 → 𝐿 ∈ 𝑆 ) |
11 |
|
lcdlssvscl.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑅 ) |
12 |
|
lcdlssvscl.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐿 ) |
13 |
1 5 9
|
lcdlmod |
⊢ ( 𝜑 → 𝐶 ∈ LMod ) |
14 |
|
eqid |
⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 ) |
15 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) ) |
16 |
1 2 3 4 5 14 15 9
|
lcdsbase |
⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = 𝑅 ) |
17 |
11 16
|
eleqtrrd |
⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ) |
18 |
14 7 15 8
|
lssvscl |
⊢ ( ( ( 𝐶 ∈ LMod ∧ 𝐿 ∈ 𝑆 ) ∧ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ∧ 𝑌 ∈ 𝐿 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐿 ) |
19 |
13 10 17 12 18
|
syl22anc |
⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐿 ) |