Metamath Proof Explorer


Theorem lclkrlem2t

Description: Lemma for lclkr . We eliminate all hypotheses with B here. (Contributed by NM, 18-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 ∧ 𝑊𝐻 ) )
lclkrlem2q.le ( 𝜑 → ( 𝐿𝐸 ) = ( ‘ { 𝑋 } ) )
lclkrlem2q.lg ( 𝜑 → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
lclkrlem2t.n ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
Assertion lclkrlem2t ( 𝜑 → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )

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 lclkrlem2q.le ( 𝜑 → ( 𝐿𝐸 ) = ( ‘ { 𝑋 } ) )
23 lclkrlem2q.lg ( 𝜑 → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
24 lclkrlem2t.n ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
25 11 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) ) → 𝑋𝑉 )
26 12 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) ) → 𝑌𝑉 )
27 13 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) ) → 𝐸𝐹 )
28 14 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) ) → 𝐺𝐹 )
29 21 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
30 22 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) ) → ( 𝐿𝐸 ) = ( ‘ { 𝑋 } ) )
31 23 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) ) → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
32 eqid ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
33 24 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
34 simpr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) ) → ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) )
35 1 2 3 4 5 6 7 8 9 10 25 26 27 28 15 16 17 18 19 20 29 30 31 32 33 34 lclkrlem2s ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g𝑈 ) ) → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
36 11 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) ) → 𝑋𝑉 )
37 12 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) ) → 𝑌𝑉 )
38 13 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) ) → 𝐸𝐹 )
39 14 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) ) → 𝐺𝐹 )
40 21 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
41 22 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) ) → ( 𝐿𝐸 ) = ( ‘ { 𝑋 } ) )
42 23 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) ) → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
43 24 adantr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
44 simpr ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) ) → ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) )
45 1 2 3 4 5 6 7 8 9 10 36 37 38 39 15 16 17 18 19 20 40 41 42 32 43 44 lclkrlem2q ( ( 𝜑 ∧ ( 𝑋 ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ≠ ( 0g𝑈 ) ) → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
46 35 45 pm2.61dane ( 𝜑 → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )