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

Metamath Proof Explorer

Theorem dochexmidlem1

Description: Lemma for dochexmid . Holland's proof implicitly requires q =/= r , which we prove here. (Contributed by NM, 14-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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
dochexmidlem1.pp ⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
dochexmidlem1.qq ⊢ ( 𝜑 → 𝑞 ∈ 𝐴 )
dochexmidlem1.rr ⊢ ( 𝜑 → 𝑟 ∈ 𝐴 )
dochexmidlem1.ql ⊢ ( 𝜑 → 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) )
dochexmidlem1.rl ⊢ ( 𝜑 → 𝑟 ⊆ 𝑋 )
Assertion dochexmidlem1 ( 𝜑 → 𝑞 ≠ 𝑟 )

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 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 imbitrdi ⊢ ( 𝜑 → ( 𝑞 = 𝑟 → 𝑟 ⊆ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ) )
33 32 necon3bd ⊢ ( 𝜑 → ( ¬ 𝑟 ⊆ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) → 𝑞 ≠ 𝑟 ) )
34 27 33 mpd ⊢ ( 𝜑 → 𝑞 ≠ 𝑟 )