Step |
Hyp |
Ref |
Expression |
1 |
|
lss0v.x |
⊢ 𝑋 = ( 𝑊 ↾s 𝑈 ) |
2 |
|
lss0v.o |
⊢ 0 = ( 0g ‘ 𝑊 ) |
3 |
|
lss0v.z |
⊢ 𝑍 = ( 0g ‘ 𝑋 ) |
4 |
|
lss0v.l |
⊢ 𝐿 = ( LSubSp ‘ 𝑊 ) |
5 |
|
0ss |
⊢ ∅ ⊆ 𝑈 |
6 |
|
eqid |
⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 ) |
7 |
|
eqid |
⊢ ( LSpan ‘ 𝑋 ) = ( LSpan ‘ 𝑋 ) |
8 |
1 6 7 4
|
lsslsp |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ ∅ ⊆ 𝑈 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) ) |
9 |
5 8
|
mp3an3 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) ) |
10 |
2 6
|
lsp0 |
⊢ ( 𝑊 ∈ LMod → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } ) |
11 |
10
|
adantr |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } ) |
12 |
1 4
|
lsslmod |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → 𝑋 ∈ LMod ) |
13 |
3 7
|
lsp0 |
⊢ ( 𝑋 ∈ LMod → ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) = { 𝑍 } ) |
14 |
12 13
|
syl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ( ( LSpan ‘ 𝑋 ) ‘ ∅ ) = { 𝑍 } ) |
15 |
9 11 14
|
3eqtr3rd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → { 𝑍 } = { 0 } ) |
16 |
15
|
unieqd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ∪ { 𝑍 } = ∪ { 0 } ) |
17 |
3
|
fvexi |
⊢ 𝑍 ∈ V |
18 |
17
|
unisn |
⊢ ∪ { 𝑍 } = 𝑍 |
19 |
2
|
fvexi |
⊢ 0 ∈ V |
20 |
19
|
unisn |
⊢ ∪ { 0 } = 0 |
21 |
16 18 20
|
3eqtr3g |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → 𝑍 = 0 ) |