dochexmidlem7

Description: Lemma for dochexmid . Contradict dochexmidlem6 . (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	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	dochexmidlem6.pp	⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
	dochexmidlem6.z	⊢ 0 = ( 0_g ‘ 𝑈 )
	dochexmidlem6.m	⊢ 𝑀 = ( 𝑋 ⊕ 𝑝 )
	dochexmidlem6.xn	⊢ ( 𝜑 → 𝑋 ≠ { 0 } )
	dochexmidlem6.c	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
	dochexmidlem6.pl	⊢ ( 𝜑 → ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
Assertion	dochexmidlem7	⊢ ( 𝜑 → 𝑀 ≠ 𝑋 )

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		dochexmidlem6.pp	⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
12		dochexmidlem6.z	⊢ 0 = ( 0_g ‘ 𝑈 )
13		dochexmidlem6.m	⊢ 𝑀 = ( 𝑋 ⊕ 𝑝 )
14		dochexmidlem6.xn	⊢ ( 𝜑 → 𝑋 ≠ { 0 } )
15		dochexmidlem6.c	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
16		dochexmidlem6.pl	⊢ ( 𝜑 → ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
17	1 3 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
18	5	lsssssubg	⊢ ( 𝑈 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
19	17 18	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
20	19 10	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ( SubGrp ‘ 𝑈 ) )
21	5 8 17 11	lsatlssel	⊢ ( 𝜑 → 𝑝 ∈ 𝑆 )
22	19 21	sseldd	⊢ ( 𝜑 → 𝑝 ∈ ( SubGrp ‘ 𝑈 ) )
23	7	lsmub2	⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑈 ) ∧ 𝑝 ∈ ( SubGrp ‘ 𝑈 ) ) → 𝑝 ⊆ ( 𝑋 ⊕ 𝑝 ) )
24	20 22 23	syl2anc	⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑋 ⊕ 𝑝 ) )
25	24 13	sseqtrrdi	⊢ ( 𝜑 → 𝑝 ⊆ 𝑀 )
26	4 5	lssss	⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ⊆ 𝑉 )
27	10 26	syl	⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
28	1 3 4 5 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )
29	9 27 28	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )
30	19 29	sseldd	⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝑈 ) )
31	7	lsmub1	⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝑈 ) ) → 𝑋 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
32	20 30 31	syl2anc	⊢ ( 𝜑 → 𝑋 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
33		sstr2	⊢ ( 𝑝 ⊆ 𝑋 → ( 𝑋 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) )
34	32 33	syl5com	⊢ ( 𝜑 → ( 𝑝 ⊆ 𝑋 → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) )
35	16 34	mtod	⊢ ( 𝜑 → ¬ 𝑝 ⊆ 𝑋 )
36		sseq2	⊢ ( 𝑀 = 𝑋 → ( 𝑝 ⊆ 𝑀 ↔ 𝑝 ⊆ 𝑋 ) )
37	36	biimpcd	⊢ ( 𝑝 ⊆ 𝑀 → ( 𝑀 = 𝑋 → 𝑝 ⊆ 𝑋 ) )
38	37	necon3bd	⊢ ( 𝑝 ⊆ 𝑀 → ( ¬ 𝑝 ⊆ 𝑋 → 𝑀 ≠ 𝑋 ) )
39	25 35 38	sylc	⊢ ( 𝜑 → 𝑀 ≠ 𝑋 )

Metamath Proof Explorer

Theorem dochexmidlem7

Proof