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