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 = ( 0_g ‘ 𝑈 )
	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 = ( 0_g ‘ 𝑈 )
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	biimpri	⊢ ( ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊊ 𝑉 )
31	30	adantl	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) ) → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊊ 𝑉 )
32	5 8 24 25 28 31	lpssat	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) )
33	32	ex	⊢ ( 𝜑 → ( ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) ) )
34	9	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
35	10	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → 𝑋 ∈ 𝑆 )
36		simp2	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → 𝑝 ∈ 𝐴 )
37		eqid	⊢ ( 𝑋 ⊕ 𝑝 ) = ( 𝑋 ⊕ 𝑝 )
38	12	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → 𝑋 ≠ { 0 } )
39	13	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
40		simp3	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )
41	1 2 3 4 5 6 7 8 34 35 36 11 37 38 39 40	dochexmidlem6	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 ⊕ 𝑝 ) = 𝑋 )
42	1 2 3 4 5 6 7 8 34 35 36 11 37 38 39 40	dochexmidlem7	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 ⊕ 𝑝 ) ≠ 𝑋 )
43	41 42	pm2.21ddne	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) )
44	43	3adant3l	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) )
45	44	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑉 ∧ ¬ 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) )
46	33 45	syld	⊢ ( 𝜑 → ( ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 ∧ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) )
47	23 46	mpand	⊢ ( 𝜑 → ( ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) )
48	47	necon1bd	⊢ ( 𝜑 → ( ¬ ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) )
49	14 48	mpi	⊢ ( 𝜑 → ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )

Metamath Proof Explorer

Theorem dochexmidlem8

Proof