# Metamath Proof Explorer

## Theorem dochexmidlem5

Description: Lemma for dochexmid . (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dochexmidlem1.h 𝐻 = ( LHyp ‘ 𝐾 )
dochexmidlem1.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochexmidlem1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochexmidlem1.v 𝑉 = ( Base ‘ 𝑈 )
dochexmidlem1.s 𝑆 = ( LSubSp ‘ 𝑈 )
dochexmidlem1.n 𝑁 = ( LSpan ‘ 𝑈 )
dochexmidlem1.p = ( LSSum ‘ 𝑈 )
dochexmidlem1.a 𝐴 = ( LSAtoms ‘ 𝑈 )
dochexmidlem1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dochexmidlem1.x ( 𝜑𝑋𝑆 )
dochexmidlem5.pp ( 𝜑𝑝𝐴 )
dochexmidlem5.z 0 = ( 0g𝑈 )
dochexmidlem5.m 𝑀 = ( 𝑋 𝑝 )
dochexmidlem5.xn ( 𝜑𝑋 ≠ { 0 } )
dochexmidlem5.pl ( 𝜑 → ¬ 𝑝 ⊆ ( 𝑋 ( 𝑋 ) ) )
Assertion dochexmidlem5 ( 𝜑 → ( ( 𝑋 ) ∩ 𝑀 ) = { 0 } )

### Proof

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 dochexmidlem5.pp ( 𝜑𝑝𝐴 )
12 dochexmidlem5.z 0 = ( 0g𝑈 )
13 dochexmidlem5.m 𝑀 = ( 𝑋 𝑝 )
14 dochexmidlem5.xn ( 𝜑𝑋 ≠ { 0 } )
15 dochexmidlem5.pl ( 𝜑 → ¬ 𝑝 ⊆ ( 𝑋 ( 𝑋 ) ) )
16 1 3 9 dvhlmod ( 𝜑𝑈 ∈ LMod )
17 16 adantr ( ( 𝜑 ∧ ( ( 𝑋 ) ∩ 𝑀 ) ≠ { 0 } ) → 𝑈 ∈ LMod )
18 4 5 lssss ( 𝑋𝑆𝑋𝑉 )
19 10 18 syl ( 𝜑𝑋𝑉 )
20 1 3 4 5 2 dochlss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) ∈ 𝑆 )
21 9 19 20 syl2anc ( 𝜑 → ( 𝑋 ) ∈ 𝑆 )
22 5 8 16 11 lsatlssel ( 𝜑𝑝𝑆 )
23 5 7 lsmcl ( ( 𝑈 ∈ LMod ∧ 𝑋𝑆𝑝𝑆 ) → ( 𝑋 𝑝 ) ∈ 𝑆 )
24 16 10 22 23 syl3anc ( 𝜑 → ( 𝑋 𝑝 ) ∈ 𝑆 )
25 13 24 eqeltrid ( 𝜑𝑀𝑆 )
26 5 lssincl ( ( 𝑈 ∈ LMod ∧ ( 𝑋 ) ∈ 𝑆𝑀𝑆 ) → ( ( 𝑋 ) ∩ 𝑀 ) ∈ 𝑆 )
27 16 21 25 26 syl3anc ( 𝜑 → ( ( 𝑋 ) ∩ 𝑀 ) ∈ 𝑆 )
28 27 adantr ( ( 𝜑 ∧ ( ( 𝑋 ) ∩ 𝑀 ) ≠ { 0 } ) → ( ( 𝑋 ) ∩ 𝑀 ) ∈ 𝑆 )
29 simpr ( ( 𝜑 ∧ ( ( 𝑋 ) ∩ 𝑀 ) ≠ { 0 } ) → ( ( 𝑋 ) ∩ 𝑀 ) ≠ { 0 } )
30 5 12 8 17 28 29 lssatomic ( ( 𝜑 ∧ ( ( 𝑋 ) ∩ 𝑀 ) ≠ { 0 } ) → ∃ 𝑞𝐴 𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) )
31 30 ex ( 𝜑 → ( ( ( 𝑋 ) ∩ 𝑀 ) ≠ { 0 } → ∃ 𝑞𝐴 𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) ) )
32 9 3ad2ant1 ( ( 𝜑𝑞𝐴𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
33 10 3ad2ant1 ( ( 𝜑𝑞𝐴𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) ) → 𝑋𝑆 )
34 11 3ad2ant1 ( ( 𝜑𝑞𝐴𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) ) → 𝑝𝐴 )
35 simp2 ( ( 𝜑𝑞𝐴𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) ) → 𝑞𝐴 )
36 14 3ad2ant1 ( ( 𝜑𝑞𝐴𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) ) → 𝑋 ≠ { 0 } )
37 simp3 ( ( 𝜑𝑞𝐴𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) ) → 𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) )
38 1 2 3 4 5 6 7 8 32 33 34 35 12 13 36 37 dochexmidlem4 ( ( 𝜑𝑞𝐴𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) ) → 𝑝 ⊆ ( 𝑋 ( 𝑋 ) ) )
39 38 rexlimdv3a ( 𝜑 → ( ∃ 𝑞𝐴 𝑞 ⊆ ( ( 𝑋 ) ∩ 𝑀 ) → 𝑝 ⊆ ( 𝑋 ( 𝑋 ) ) ) )
40 31 39 syld ( 𝜑 → ( ( ( 𝑋 ) ∩ 𝑀 ) ≠ { 0 } → 𝑝 ⊆ ( 𝑋 ( 𝑋 ) ) ) )
41 40 necon1bd ( 𝜑 → ( ¬ 𝑝 ⊆ ( 𝑋 ( 𝑋 ) ) → ( ( 𝑋 ) ∩ 𝑀 ) = { 0 } ) )
42 15 41 mpd ( 𝜑 → ( ( 𝑋 ) ∩ 𝑀 ) = { 0 } )