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