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	⊢ ( 𝜑 → 𝑞 ≠ 𝑟 )