Step |
Hyp |
Ref |
Expression |
1 |
|
dochexmidlem1.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
dochexmidlem1.o |
⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
dochexmidlem1.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
dochexmidlem1.v |
⊢ 𝑉 = ( Base ‘ 𝑈 ) |
5 |
|
dochexmidlem1.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑈 ) |
6 |
|
dochexmidlem1.n |
⊢ 𝑁 = ( LSpan ‘ 𝑈 ) |
7 |
|
dochexmidlem1.p |
⊢ ⊕ = ( LSSum ‘ 𝑈 ) |
8 |
|
dochexmidlem1.a |
⊢ 𝐴 = ( LSAtoms ‘ 𝑈 ) |
9 |
|
dochexmidlem1.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
10 |
|
dochexmidlem1.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑆 ) |
11 |
|
dochexmidlem1.pp |
⊢ ( 𝜑 → 𝑝 ∈ 𝐴 ) |
12 |
|
dochexmidlem1.qq |
⊢ ( 𝜑 → 𝑞 ∈ 𝐴 ) |
13 |
|
dochexmidlem1.rr |
⊢ ( 𝜑 → 𝑟 ∈ 𝐴 ) |
14 |
|
dochexmidlem1.ql |
⊢ ( 𝜑 → 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) ) |
15 |
|
dochexmidlem1.rl |
⊢ ( 𝜑 → 𝑟 ⊆ 𝑋 ) |
16 |
|
eqid |
⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 ) |
17 |
1 3 9
|
dvhlmod |
⊢ ( 𝜑 → 𝑈 ∈ LMod ) |
18 |
16 8 17 13
|
lsatn0 |
⊢ ( 𝜑 → 𝑟 ≠ { ( 0g ‘ 𝑈 ) } ) |
19 |
5 8 17 13
|
lsatlssel |
⊢ ( 𝜑 → 𝑟 ∈ 𝑆 ) |
20 |
16 5
|
lssle0 |
⊢ ( ( 𝑈 ∈ LMod ∧ 𝑟 ∈ 𝑆 ) → ( 𝑟 ⊆ { ( 0g ‘ 𝑈 ) } ↔ 𝑟 = { ( 0g ‘ 𝑈 ) } ) ) |
21 |
17 19 20
|
syl2anc |
⊢ ( 𝜑 → ( 𝑟 ⊆ { ( 0g ‘ 𝑈 ) } ↔ 𝑟 = { ( 0g ‘ 𝑈 ) } ) ) |
22 |
21
|
necon3bbid |
⊢ ( 𝜑 → ( ¬ 𝑟 ⊆ { ( 0g ‘ 𝑈 ) } ↔ 𝑟 ≠ { ( 0g ‘ 𝑈 ) } ) ) |
23 |
18 22
|
mpbird |
⊢ ( 𝜑 → ¬ 𝑟 ⊆ { ( 0g ‘ 𝑈 ) } ) |
24 |
1 3 5 16 2
|
dochnoncon |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) = { ( 0g ‘ 𝑈 ) } ) |
25 |
9 10 24
|
syl2anc |
⊢ ( 𝜑 → ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) = { ( 0g ‘ 𝑈 ) } ) |
26 |
25
|
sseq2d |
⊢ ( 𝜑 → ( 𝑟 ⊆ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ↔ 𝑟 ⊆ { ( 0g ‘ 𝑈 ) } ) ) |
27 |
23 26
|
mtbird |
⊢ ( 𝜑 → ¬ 𝑟 ⊆ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ) |
28 |
|
sseq1 |
⊢ ( 𝑞 = 𝑟 → ( 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) ↔ 𝑟 ⊆ ( ⊥ ‘ 𝑋 ) ) ) |
29 |
14 28
|
syl5ibcom |
⊢ ( 𝜑 → ( 𝑞 = 𝑟 → 𝑟 ⊆ ( ⊥ ‘ 𝑋 ) ) ) |
30 |
29 15
|
jctild |
⊢ ( 𝜑 → ( 𝑞 = 𝑟 → ( 𝑟 ⊆ 𝑋 ∧ 𝑟 ⊆ ( ⊥ ‘ 𝑋 ) ) ) ) |
31 |
|
ssin |
⊢ ( ( 𝑟 ⊆ 𝑋 ∧ 𝑟 ⊆ ( ⊥ ‘ 𝑋 ) ) ↔ 𝑟 ⊆ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ) |
32 |
30 31
|
syl6ib |
⊢ ( 𝜑 → ( 𝑞 = 𝑟 → 𝑟 ⊆ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ) ) |
33 |
32
|
necon3bd |
⊢ ( 𝜑 → ( ¬ 𝑟 ⊆ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) → 𝑞 ≠ 𝑟 ) ) |
34 |
27 33
|
mpd |
⊢ ( 𝜑 → 𝑞 ≠ 𝑟 ) |