This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dochexmidlem7

Description: Lemma for dochexmid . Contradict dochexmidlem6 . (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dochexmidlem1.h ⊢ H = LHyp ⁡ K
dochexmidlem1.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochexmidlem1.u ⊢ U = DVecH ⁡ K ⁡ W
dochexmidlem1.v ⊢ V = Base U
dochexmidlem1.s ⊢ S = LSubSp ⁡ U
dochexmidlem1.n ⊢ N = LSpan ⁡ U
dochexmidlem1.p ⊢ ⊕ ˙ = LSSum ⁡ U
dochexmidlem1.a ⊢ A = LSAtoms ⁡ U
dochexmidlem1.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochexmidlem1.x ⊢ φ → X ∈ S
dochexmidlem6.pp ⊢ φ → p ∈ A
dochexmidlem6.z ⊢ 0 ˙ = 0 U
dochexmidlem6.m ⊢ M = X ⊕ ˙ p
dochexmidlem6.xn ⊢ φ → X ≠ 0 ˙
dochexmidlem6.c ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
dochexmidlem6.pl ⊢ φ → ¬ p ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X
Assertion dochexmidlem7 ⊢ φ → M ≠ X

Proof

Step Hyp Ref Expression
1 dochexmidlem1.h ⊢ H = LHyp ⁡ K
2 dochexmidlem1.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochexmidlem1.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochexmidlem1.v ⊢ V = Base U
5 dochexmidlem1.s ⊢ S = LSubSp ⁡ U
6 dochexmidlem1.n ⊢ N = LSpan ⁡ U
7 dochexmidlem1.p ⊢ ⊕ ˙ = LSSum ⁡ U
8 dochexmidlem1.a ⊢ A = LSAtoms ⁡ U
9 dochexmidlem1.k ⊢ φ → K ∈ HL ∧ W ∈ H
10 dochexmidlem1.x ⊢ φ → X ∈ S
11 dochexmidlem6.pp ⊢ φ → p ∈ A
12 dochexmidlem6.z ⊢ 0 ˙ = 0 U
13 dochexmidlem6.m ⊢ M = X ⊕ ˙ p
14 dochexmidlem6.xn ⊢ φ → X ≠ 0 ˙
15 dochexmidlem6.c ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
16 dochexmidlem6.pl ⊢ φ → ¬ p ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X
17 1 3 9 dvhlmod ⊢ φ → U ∈ LMod
18 5 lsssssubg ⊢ U ∈ LMod → S ⊆ SubGrp ⁡ U
19 17 18 syl ⊢ φ → S ⊆ SubGrp ⁡ U
20 19 10 sseldd ⊢ φ → X ∈ SubGrp ⁡ U
21 5 8 17 11 lsatlssel ⊢ φ → p ∈ S
22 19 21 sseldd ⊢ φ → p ∈ SubGrp ⁡ U
23 7 lsmub2 ⊢ X ∈ SubGrp ⁡ U ∧ p ∈ SubGrp ⁡ U → p ⊆ X ⊕ ˙ p
24 20 22 23 syl2anc ⊢ φ → p ⊆ X ⊕ ˙ p
25 24 13 sseqtrrdi ⊢ φ → p ⊆ M
26 4 5 lssss ⊢ X ∈ S → X ⊆ V
27 10 26 syl ⊢ φ → X ⊆ V
28 1 3 4 5 2 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ S
29 9 27 28 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ∈ S
30 19 29 sseldd ⊢ φ → ⊥ ˙ ⁡ X ∈ SubGrp ⁡ U
31 7 lsmub1 ⊢ X ∈ SubGrp ⁡ U ∧ ⊥ ˙ ⁡ X ∈ SubGrp ⁡ U → X ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X
32 20 30 31 syl2anc ⊢ φ → X ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X
33 sstr2 ⊢ p ⊆ X → X ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X → p ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X
34 32 33 syl5com ⊢ φ → p ⊆ X → p ⊆ X ⊕ ˙ ⊥ ˙ ⁡ X
35 16 34 mtod ⊢ φ → ¬ p ⊆ X
36 sseq2 ⊢ M = X → p ⊆ M ↔ p ⊆ X
37 36 biimpcd ⊢ p ⊆ M → M = X → p ⊆ X
38 37 necon3bd ⊢ p ⊆ M → ¬ p ⊆ X → M ≠ X
39 25 35 38 sylc ⊢ φ → M ≠ X