Theorem lclkrlem2a

Description: Lemma for lclkr . Use lshpat to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lclkrlem2a.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrlem2a.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrlem2a.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lclkrlem2a.z	⊢ 0 = ( 0g ‘ 𝑈 )
	lclkrlem2a.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	lclkrlem2a.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	lclkrlem2a.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
	lclkrlem2a.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lclkrlem2a.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
	lclkrlem2a.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
	lclkrlem2a.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
	lclkrlem2a.e	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ ( ⊥ ‘ { 𝑌 } ) )
	lclkrlem2a.d	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) )
Assertion	lclkrlem2a	⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lclkrlem2a.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lclkrlem2a.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lclkrlem2a.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lclkrlem2a.z	⊢ 0 = ( 0g ‘ 𝑈 )
6		lclkrlem2a.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
7		lclkrlem2a.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8		lclkrlem2a.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
9		lclkrlem2a.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lclkrlem2a.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
11		lclkrlem2a.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
12		lclkrlem2a.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
13		lclkrlem2a.e	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ ( ⊥ ‘ { 𝑌 } ) )
14		lclkrlem2a.d	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) )
15		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
16		eqid	⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
17	1 3 9	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
18	1 2 3 4 5 16 9 10	dochsnshp	⊢ ( 𝜑 → ( ⊥ ‘ { 𝐵 } ) ∈ ( LSHyp ‘ 𝑈 ) )
19	1 3 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
20	4 7 5 8 19 11	lsatlspsn	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )
21	4 7 5 8 19 12	lsatlspsn	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ 𝐴 )
22	11	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
23	22	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
24	1 3 2 4 7 9 23	dochocsp	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( ⊥ ‘ { 𝑋 } ) )
25	12	eldifad	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
26	25	snssd	⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
27	1 3 2 4 7 9 26	dochocsp	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( ⊥ ‘ { 𝑌 } ) )
28	24 27	eqeq12d	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( ⊥ ‘ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( ⊥ ‘ { 𝑋 } ) = ( ⊥ ‘ { 𝑌 } ) ) )
29		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
30	1 3 4 7 29	dihlsprn	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
31	9 22 30	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
32	1 3 4 7 29	dihlsprn	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
33	9 25 32	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
34	1 29 2 9 31 33	doch11	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( ⊥ ‘ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
35	28 34	bitr3d	⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) = ( ⊥ ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) ) )
36	35	necon3bid	⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ≠ ( ⊥ ‘ { 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
37	13 36	mpbid	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
38	10	eldifad	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
39	38	snssd	⊢ ( 𝜑 → { 𝐵 } ⊆ 𝑉 )
40	1 3 4 15 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐵 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝐵 } ) ∈ ( LSubSp ‘ 𝑈 ) )
41	9 39 40	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ { 𝐵 } ) ∈ ( LSubSp ‘ 𝑈 ) )
42	4 15 7 19 41 22	ellspsn5b	⊢ ( 𝜑 → ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ⊥ ‘ { 𝐵 } ) ) )
43	14 42	mtbid	⊢ ( 𝜑 → ¬ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ⊥ ‘ { 𝐵 } ) )
44	15 6 16 8 17 18 20 21 37 43	lshpat	⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { 𝐵 } ) ) ∈ 𝐴 )