Metamath Proof Explorer

Theorem lclkrlem2o

Description: Lemma for lclkr . When B is nonzero, the vectors X and Y can't both belong to the hyperplane generated by B . (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses lclkrlem2m.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2m.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
lclkrlem2m.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
lclkrlem2m.q ⊢ × = ( .r ‘ 𝑆 )
lclkrlem2m.z ⊢ 0 = ( 0g ‘ 𝑆 )
lclkrlem2m.i ⊢ 𝐼 = ( invr ‘ 𝑆 )
lclkrlem2m.m ⊢ − = ( -g ‘ 𝑈 )
lclkrlem2m.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lclkrlem2m.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lclkrlem2m.p ⊢ + = ( +g ‘ 𝐷 )
lclkrlem2m.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lclkrlem2m.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lclkrlem2m.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
lclkrlem2m.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lclkrlem2n.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lclkrlem2n.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lclkrlem2o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lclkrlem2o.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2o.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2o.a ⊢ ⊕ = ( LSSum ‘ 𝑈 )
lclkrlem2o.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lclkrlem2o.b ⊢ 𝐵 = ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
lclkrlem2o.n ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
lclkrlem2o.bn ⊢ ( 𝜑 → 𝐵 ≠ ( 0g ‘ 𝑈 ) )
Assertion lclkrlem2o ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
2 lclkrlem2m.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
3 lclkrlem2m.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4 lclkrlem2m.q ⊢ × = ( .r ‘ 𝑆 )
5 lclkrlem2m.z ⊢ 0 = ( 0g ‘ 𝑆 )
6 lclkrlem2m.i ⊢ 𝐼 = ( invr ‘ 𝑆 )
7 lclkrlem2m.m ⊢ − = ( -g ‘ 𝑈 )
8 lclkrlem2m.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9 lclkrlem2m.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
10 lclkrlem2m.p ⊢ + = ( +g ‘ 𝐷 )
11 lclkrlem2m.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12 lclkrlem2m.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
13 lclkrlem2m.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
14 lclkrlem2m.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
15 lclkrlem2n.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
16 lclkrlem2n.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
17 lclkrlem2o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
18 lclkrlem2o.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
19 lclkrlem2o.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
20 lclkrlem2o.a ⊢ ⊕ = ( LSSum ‘ 𝑈 )
21 lclkrlem2o.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
22 lclkrlem2o.b ⊢ 𝐵 = ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
23 lclkrlem2o.n ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
24 lclkrlem2o.bn ⊢ ( 𝜑 → 𝐵 ≠ ( 0g ‘ 𝑈 ) )
25 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
26 17 19 21 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
27 1 2 3 4 5 6 7 8 9 10 11 12 13 14 26 22 23 lclkrlem2m ⊢ ( 𝜑 → ( 𝐵 ∈ 𝑉 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 0 ) )
28 27 simpld ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
29 eldifsn ⊢ ( 𝐵 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ≠ ( 0g ‘ 𝑈 ) ) )
30 28 24 29 sylanbrc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
31 17 18 19 1 25 21 30 dochnel ⊢ ( 𝜑 → ¬ 𝐵 ∈ ( ⊥ ‘ { 𝐵 } ) )
32 17 19 21 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
33 32 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) ) → 𝑈 ∈ LMod )
34 28 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ 𝑉 )
35 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
36 17 19 1 35 18 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐵 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝐵 } ) ∈ ( LSubSp ‘ 𝑈 ) )
37 21 34 36 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { 𝐵 } ) ∈ ( LSubSp ‘ 𝑈 ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) ) → ( ⊥ ‘ { 𝐵 } ) ∈ ( LSubSp ‘ 𝑈 ) )
39 simprl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) ) → 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) )
40 3 lmodring ⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Ring )
41 32 40 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
42 8 9 10 32 13 14 ldualvaddcl ⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
43 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
44 3 43 1 8 lflcl ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
45 32 42 11 44 syl3anc ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
46 3 lvecdrng ⊢ ( 𝑈 ∈ LVec → 𝑆 ∈ DivRing )
47 26 46 syl ⊢ ( 𝜑 → 𝑆 ∈ DivRing )
48 3 43 1 8 lflcl ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
49 32 42 12 48 syl3anc ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
50 43 5 6 drnginvrcl ⊢ ( ( 𝑆 ∈ DivRing ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 ) → ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) )
51 47 49 23 50 syl3anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) )
52 43 4 ringcl ⊢ ( ( 𝑆 ∈ Ring ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) )
53 41 45 51 52 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) ) → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) )
55 simprr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) ) → 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) )
56 3 2 43 35 lssvscl ⊢ ( ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ { 𝐵 } ) ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) ) → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ ( ⊥ ‘ { 𝐵 } ) )
57 33 38 54 55 56 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) ) → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ ( ⊥ ‘ { 𝐵 } ) )
58 7 35 lssvsubcl ⊢ ( ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ { 𝐵 } ) ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ ( ⊥ ‘ { 𝐵 } ) ) ) → ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ∈ ( ⊥ ‘ { 𝐵 } ) )
59 33 38 39 57 58 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) ) → ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ∈ ( ⊥ ‘ { 𝐵 } ) )
60 22 59 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) ) → 𝐵 ∈ ( ⊥ ‘ { 𝐵 } ) )
61 31 60 mtand ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) )
62 ianor ⊢ ( ¬ ( 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∧ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) ↔ ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) )
63 61 62 sylib ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ⊥ ‘ { 𝐵 } ) ) )