Metamath Proof Explorer

Theorem dochexmidlem8

Description: Lemma for dochexmid . The contradiction of dochexmidlem6 and dochexmidlem7 shows that there can be no atom p that is not in X + ( ._|_X ) , which is therefore the whole atom space. (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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
dochexmidlem8.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochexmidlem8.xn ⊢ ( 𝜑 → 𝑋 ≠ { 0 } )
dochexmidlem8.c ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
Assertion dochexmidlem8 ( 𝜑 → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )

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 dochexmidlem8.z ⊢ 0 = ( 0g ‘ 𝑈 )
12 dochexmidlem8.xn ⊢ ( 𝜑 → 𝑋 ≠ { 0 } )
13 dochexmidlem8.c ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
14 nonconne ⊢ ¬ ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 )
15 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 4 5 lssss ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ⊆ 𝑉 )
17 10 16 syl ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
18 1 3 4 5 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )
19 9 17 18 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )
20 5 7 lsmcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑆 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝑆 ) → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ∈ 𝑆 )
21 15 10 19 20 syl3anc ⊢ ( 𝜑 → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ∈ 𝑆 )
22 4 5 lssss ⊢ ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ∈ 𝑆 → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 )
23 21 22 syl ⊢ ( 𝜑 → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 )
24 15 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) ) → 𝑈 ∈ LMod )
25 21 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) ) → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ∈ 𝑆 )
26 4 5 lss1 ⊢ ( 𝑈 ∈ LMod → 𝑉 ∈ 𝑆 )
27 15 26 syl ⊢ ( 𝜑 → 𝑉 ∈ 𝑆 )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) ) → 𝑉 ∈ 𝑆 )
29 df-pss ⊢ ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊊ 𝑉 ↔ ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) )
30 29 bilanri ⊢ ( ( 𝜑 ∧ ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) ) → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊊ 𝑉 )
31 5 8 24 25 28 30 lpssat ⊢ ( ( 𝜑 ∧ ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) )
32 31 ex ⊢ ( 𝜑 → ( ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) ) )
33 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
34 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → 𝑋 ∈ 𝑆 )
35 simp2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → 𝑝 ∈ 𝐴 )
36 eqid ⊢ ( 𝑋 ⊕ 𝑝 ) = ( 𝑋 ⊕ 𝑝 )
37 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → 𝑋 ≠ { 0 } )
38 13 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
39 simp3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
40 1 2 3 4 5 6 7 8 33 34 35 11 36 37 38 39 dochexmidlem6 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 ⊕ 𝑝 ) = 𝑋 )
41 1 2 3 4 5 6 7 8 33 34 35 11 36 37 38 39 dochexmidlem7 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 ⊕ 𝑝 ) ≠ 𝑋 )
42 40 41 pm2.21ddne ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) )
43 42 3adant3l ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) )
44 43 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) )
45 32 44 syld ⊢ ( 𝜑 → ( ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) )
46 23 45 mpand ⊢ ( 𝜑 → ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) )
47 46 necon1bd ⊢ ( 𝜑 → ( ¬ ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) )
48 14 47 mpi ⊢ ( 𝜑 → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )