Metamath Proof Explorer

Theorem 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 = ( 0g ‘ 𝑈 )
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 = ( 0g ‘ 𝑈 )
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 ⊢ ( 𝜑 → 𝑀 ≠ 𝑋 )