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 lspsnel5 ( 𝜑 → ( 𝑋 ∈ ( ‘ { ( 𝑋 + 𝑌 ) } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) )
33 13 32 mtbid ( 𝜑 → ¬ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ‘ { ( 𝑋 + 𝑌 ) } ) )
34 20 14 21 8 22 24 25 26 12 33 lshpat ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ 𝐴 )
35 19 34 eqeltrd ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ 𝐴 )