Theorem dochexmidlem4

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	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	dochexmidlem4.pp	⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
	dochexmidlem4.qq	⊢ ( 𝜑 → 𝑞 ∈ 𝐴 )
	dochexmidlem4.z	⊢ 0 = ( 0g ‘ 𝑈 )
	dochexmidlem4.m	⊢ 𝑀 = ( 𝑋 ⊕ 𝑝 )
	dochexmidlem4.xn	⊢ ( 𝜑 → 𝑋 ≠ { 0 } )
	dochexmidlem4.pl	⊢ ( 𝜑 → 𝑞 ⊆ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) )
Assertion	dochexmidlem4	⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )

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		dochexmidlem4.pp	⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
12		dochexmidlem4.qq	⊢ ( 𝜑 → 𝑞 ∈ 𝐴 )
13		dochexmidlem4.z	⊢ 0 = ( 0g ‘ 𝑈 )
14		dochexmidlem4.m	⊢ 𝑀 = ( 𝑋 ⊕ 𝑝 )
15		dochexmidlem4.xn	⊢ ( 𝜑 → 𝑋 ≠ { 0 } )
16		dochexmidlem4.pl	⊢ ( 𝜑 → 𝑞 ⊆ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) )
17	1 3 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
18	5 8 17 11	lsatlssel	⊢ ( 𝜑 → 𝑝 ∈ 𝑆 )
19		inss2	⊢ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ⊆ 𝑀
20	16 19	sstrdi	⊢ ( 𝜑 → 𝑞 ⊆ 𝑀 )
21	20 14	sseqtrdi	⊢ ( 𝜑 → 𝑞 ⊆ ( 𝑋 ⊕ 𝑝 ) )
22	13 5 7 8 17 10 18 12 15 21	lsmsat	⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) )
23	9	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
24	10	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) ) → 𝑋 ∈ 𝑆 )
25	11	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) ) → 𝑝 ∈ 𝐴 )
26	12	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) ) → 𝑞 ∈ 𝐴 )
27		simp2	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) ) → 𝑟 ∈ 𝐴 )
28		inss1	⊢ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑀 ) ⊆ ( ⊥ ‘ 𝑋 )
29	16 28	sstrdi	⊢ ( 𝜑 → 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) )
30	29	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) )
31		simp3l	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) ) → 𝑟 ⊆ 𝑋 )
32		simp3r	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) ) → 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) )
33	1 2 3 4 5 6 7 8 23 24 25 26 27 30 31 32	dochexmidlem3	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐴 ∧ ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) ) → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
34	33	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝐴 ( 𝑟 ⊆ 𝑋 ∧ 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) ) → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) )
35	22 34	mpd	⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )