Metamath Proof Explorer

Theorem lcfrlem20

Description: Lemma for lcfr . (Contributed by NM, 11-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 lcfrlem17.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfrlem17.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfrlem17.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfrlem17.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 lcfrlem17.p ⊢ + = ( +g ‘ 𝑈 )
6 lcfrlem17.z ⊢ 0 = ( 0g ‘ 𝑈 )
7 lcfrlem17.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 lcfrlem17.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
9 lcfrlem17.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 lcfrlem17.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
11 lcfrlem17.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
12 lcfrlem17.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
13 lcfrlem20.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
14 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
15 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 10 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
17 11 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
18 4 7 14 15 16 17 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) )
19 18 ineq1d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) )
20 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
21 eqid ⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
22 1 3 9 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
23 1 2 3 4 5 6 7 8 9 10 11 12 lcfrlem17 ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝑉 ∖ { 0 } ) )
24 1 2 3 4 6 21 9 23 dochsnshp ⊢ ( 𝜑 → ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSHyp ‘ 𝑈 ) )
25 4 7 6 8 15 10 lsatlspsn ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )
26 4 7 6 8 15 11 lsatlspsn ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ 𝐴 )
27 4 5 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
28 15 16 17 27 syl3anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
29 28 snssd ⊢ ( 𝜑 → { ( 𝑋 + 𝑌 ) } ⊆ 𝑉 )
30 1 3 4 20 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { ( 𝑋 + 𝑌 ) } ⊆ 𝑉 ) → ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑈 ) )
31 9 29 30 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑈 ) )
32 4 20 7 15 31 16 ellspsn5b ⊢ ( 𝜑 → ( 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) )
33 13 32 mtbid ⊢ ( 𝜑 → ¬ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
34 20 14 21 8 22 24 25 26 12 33 lshpat ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ 𝐴 )
35 19 34 eqeltrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ 𝐴 )