This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } )