Metamath Proof Explorer

Theorem lclkrlem2x

Description: Lemma for lclkr . Eliminate by cases the hypotheses of lclkrlem2u , lclkrlem2u and lclkrlem2w . (Contributed by NM, 18-Jan-2015)

Ref Expression
Hypotheses lclkrlem2x.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lclkrlem2x.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lclkrlem2x.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2x.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2x.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2x.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lclkrlem2x.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lclkrlem2x.p ⊢ + = ( +g ‘ 𝐷 )
lclkrlem2x.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lclkrlem2x.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lclkrlem2x.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lclkrlem2x.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
lclkrlem2x.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lclkrlem2x.le ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
lclkrlem2x.lg ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
Assertion lclkrlem2x ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2x.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
2 lclkrlem2x.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 lclkrlem2x.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 lclkrlem2x.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 lclkrlem2x.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
6 lclkrlem2x.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7 lclkrlem2x.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
8 lclkrlem2x.p ⊢ + = ( +g ‘ 𝐷 )
9 lclkrlem2x.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 lclkrlem2x.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11 lclkrlem2x.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
12 lclkrlem2x.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
13 lclkrlem2x.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
14 lclkrlem2x.le ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
15 lclkrlem2x.lg ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
16 df-ne ⊢ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ↔ ¬ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) )
17 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
18 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
19 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑈 ) ) = ( .r ‘ ( Scalar ‘ 𝑈 ) )
20 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) )
21 eqid ⊢ ( invr ‘ ( Scalar ‘ 𝑈 ) ) = ( invr ‘ ( Scalar ‘ 𝑈 ) )
22 eqid ⊢ ( -g ‘ 𝑈 ) = ( -g ‘ 𝑈 )
23 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → 𝑋 ∈ 𝑉 )
24 11 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → 𝑌 ∈ 𝑉 )
25 12 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → 𝐸 ∈ 𝐹 )
26 13 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → 𝐺 ∈ 𝐹 )
27 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
28 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
29 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
30 14 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
31 15 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
32 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) )
33 5 17 18 19 20 21 22 6 7 8 23 24 25 26 27 1 2 3 4 28 29 30 31 32 lclkrlem2u ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
34 16 33 sylan2br ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
35 df-ne ⊢ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ↔ ¬ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) )
36 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → 𝑋 ∈ 𝑉 )
37 11 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → 𝑌 ∈ 𝑉 )
38 12 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → 𝐸 ∈ 𝐹 )
39 13 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → 𝐺 ∈ 𝐹 )
40 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
41 14 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
42 15 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
43 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) )
44 5 17 18 19 20 21 22 6 7 8 36 37 38 39 27 1 2 3 4 28 40 41 42 43 lclkrlem2t ⊢ ( ( 𝜑 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
45 35 44 sylan2br ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
46 10 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) ) → 𝑋 ∈ 𝑉 )
47 11 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) ) → 𝑌 ∈ 𝑉 )
48 12 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) ) → 𝐸 ∈ 𝐹 )
49 13 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) ) → 𝐺 ∈ 𝐹 )
50 9 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
51 14 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) ) → ( 𝐿 ‘ 𝐸 ) = ( ⊥ ‘ { 𝑋 } ) )
52 15 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑌 } ) )
53 simprl ⊢ ( ( 𝜑 ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) )
54 simprr ⊢ ( ( 𝜑 ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) )
55 5 17 18 19 20 21 22 6 7 8 46 47 48 49 27 1 2 3 4 28 50 51 52 53 54 lclkrlem2w ⊢ ( ( 𝜑 ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
56 34 45 55 pm2.61dda ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )