Metamath Proof Explorer

Theorem lcfrlem19

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 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lcfrlem19 ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) )

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 1 2 3 4 5 6 7 8 9 10 11 12 lcfrlem17 ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝑉 ∖ { 0 } ) )
14 1 2 3 4 6 9 13 dochnel ⊢ ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
15 1 3 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∧ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ) → 𝑈 ∈ LMod )
17 10 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
18 11 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
19 4 5 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
20 15 17 18 19 syl3anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
21 20 snssd ⊢ ( 𝜑 → { ( 𝑋 + 𝑌 ) } ⊆ 𝑉 )
22 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
23 1 3 4 22 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { ( 𝑋 + 𝑌 ) } ⊆ 𝑉 ) → ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑈 ) )
24 9 21 23 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑈 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∧ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ) → ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑈 ) )
26 simpr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∧ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ) → ( 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∧ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) )
27 5 22 lssvacl ⊢ ( ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∧ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
28 16 25 26 27 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∧ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
29 14 28 mtand ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∧ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) )
30 ianor ⊢ ( ¬ ( 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∧ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ↔ ( ¬ 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) )
31 29 30 sylib ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) )