Step |
Hyp |
Ref |
Expression |
1 |
|
lsatcvat2.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) |
2 |
|
lsatcvat2.p |
⊢ ⊕ = ( LSSum ‘ 𝑊 ) |
3 |
|
lsatcvat2.a |
⊢ 𝐴 = ( LSAtoms ‘ 𝑊 ) |
4 |
|
lsatcvat2.c |
⊢ 𝐶 = ( ⋖L ‘ 𝑊 ) |
5 |
|
lsatcvat2.w |
⊢ ( 𝜑 → 𝑊 ∈ LVec ) |
6 |
|
lsatcvat2.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑆 ) |
7 |
|
lsatcvat2.q |
⊢ ( 𝜑 → 𝑄 ∈ 𝐴 ) |
8 |
|
lsatcvat2.r |
⊢ ( 𝜑 → 𝑅 ∈ 𝐴 ) |
9 |
|
lsatcvat2.n |
⊢ ( 𝜑 → 𝑄 ≠ 𝑅 ) |
10 |
|
lsatcvat2.l |
⊢ ( 𝜑 → 𝑈 𝐶 ( 𝑄 ⊕ 𝑅 ) ) |
11 |
|
eqid |
⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 ) |
12 |
11 2 1 3 4 5 6 7 8 10
|
lsatcv1 |
⊢ ( 𝜑 → ( 𝑈 = { ( 0g ‘ 𝑊 ) } ↔ 𝑄 = 𝑅 ) ) |
13 |
12
|
necon3bid |
⊢ ( 𝜑 → ( 𝑈 ≠ { ( 0g ‘ 𝑊 ) } ↔ 𝑄 ≠ 𝑅 ) ) |
14 |
9 13
|
mpbird |
⊢ ( 𝜑 → 𝑈 ≠ { ( 0g ‘ 𝑊 ) } ) |
15 |
|
lveclmod |
⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod ) |
16 |
5 15
|
syl |
⊢ ( 𝜑 → 𝑊 ∈ LMod ) |
17 |
1 3 16 7
|
lsatlssel |
⊢ ( 𝜑 → 𝑄 ∈ 𝑆 ) |
18 |
1 3 16 8
|
lsatlssel |
⊢ ( 𝜑 → 𝑅 ∈ 𝑆 ) |
19 |
1 2
|
lsmcl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑄 ∈ 𝑆 ∧ 𝑅 ∈ 𝑆 ) → ( 𝑄 ⊕ 𝑅 ) ∈ 𝑆 ) |
20 |
16 17 18 19
|
syl3anc |
⊢ ( 𝜑 → ( 𝑄 ⊕ 𝑅 ) ∈ 𝑆 ) |
21 |
1 4 5 6 20 10
|
lcvpss |
⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) ) |
22 |
11 1 2 3 5 6 7 8 14 21
|
lsatcvat |
⊢ ( 𝜑 → 𝑈 ∈ 𝐴 ) |