Metamath Proof Explorer


Theorem lclkrlem2u

Description: Lemma for lclkr . lclkrlem2t with X and Y swapped. (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 ( 𝜑 → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
lclkrlem2u.n ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ 0 )
Assertion lclkrlem2u ( 𝜑 → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )

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 lclkrlem2u.n ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ≠ 0 )
25 17 19 21 dvhlmod ( 𝜑𝑈 ∈ LMod )
26 8 9 10 25 13 14 ldualvaddcom ( 𝜑 → ( 𝐸 + 𝐺 ) = ( 𝐺 + 𝐸 ) )
27 26 fveq1d ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = ( ( 𝐺 + 𝐸 ) ‘ 𝑋 ) )
28 27 24 eqnetrrd ( 𝜑 → ( ( 𝐺 + 𝐸 ) ‘ 𝑋 ) ≠ 0 )
29 1 2 3 4 5 6 7 8 9 10 12 11 14 13 15 16 17 18 19 20 21 23 22 28 lclkrlem2t ( 𝜑 → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐺 + 𝐸 ) ) ) ) = ( 𝐿 ‘ ( 𝐺 + 𝐸 ) ) )
30 26 fveq2d ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = ( 𝐿 ‘ ( 𝐺 + 𝐸 ) ) )
31 30 fveq2d ( 𝜑 → ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) = ( ‘ ( 𝐿 ‘ ( 𝐺 + 𝐸 ) ) ) )
32 31 fveq2d ( 𝜑 → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐺 + 𝐸 ) ) ) ) )
33 29 32 30 3eqtr4d ( 𝜑 → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )