Metamath Proof Explorer


Theorem mapdrvallem3

Description: Lemma for mapdrval . (Contributed by NM, 2-Feb-2015)

Ref Expression
Hypotheses mapdrval.h 𝐻 = ( LHyp ‘ 𝐾 )
mapdrval.o 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapdrval.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdrval.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdrval.s 𝑆 = ( LSubSp ‘ 𝑈 )
mapdrval.f 𝐹 = ( LFnl ‘ 𝑈 )
mapdrval.l 𝐿 = ( LKer ‘ 𝑈 )
mapdrval.d 𝐷 = ( LDual ‘ 𝑈 )
mapdrval.t 𝑇 = ( LSubSp ‘ 𝐷 )
mapdrval.c 𝐶 = { 𝑔𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑔 ) ) ) = ( 𝐿𝑔 ) }
mapdrval.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
mapdrval.r ( 𝜑𝑅𝑇 )
mapdrval.e ( 𝜑𝑅𝐶 )
mapdrval.q 𝑄 = 𝑅 ( 𝑂 ‘ ( 𝐿 ) )
mapdrval.v 𝑉 = ( Base ‘ 𝑈 )
mapdrvallem2.a 𝐴 = ( LSAtoms ‘ 𝑈 )
mapdrvallem2.n 𝑁 = ( LSpan ‘ 𝑈 )
mapdrvallem2.z 0 = ( 0g𝑈 )
mapdrvallem2.y 𝑌 = ( 0g𝐷 )
Assertion mapdrvallem3 ( 𝜑 → { 𝑓𝐶 ∣ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 } = 𝑅 )

Proof

Step Hyp Ref Expression
1 mapdrval.h 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdrval.o 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdrval.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
4 mapdrval.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 mapdrval.s 𝑆 = ( LSubSp ‘ 𝑈 )
6 mapdrval.f 𝐹 = ( LFnl ‘ 𝑈 )
7 mapdrval.l 𝐿 = ( LKer ‘ 𝑈 )
8 mapdrval.d 𝐷 = ( LDual ‘ 𝑈 )
9 mapdrval.t 𝑇 = ( LSubSp ‘ 𝐷 )
10 mapdrval.c 𝐶 = { 𝑔𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑔 ) ) ) = ( 𝐿𝑔 ) }
11 mapdrval.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 mapdrval.r ( 𝜑𝑅𝑇 )
13 mapdrval.e ( 𝜑𝑅𝐶 )
14 mapdrval.q 𝑄 = 𝑅 ( 𝑂 ‘ ( 𝐿 ) )
15 mapdrval.v 𝑉 = ( Base ‘ 𝑈 )
16 mapdrvallem2.a 𝐴 = ( LSAtoms ‘ 𝑈 )
17 mapdrvallem2.n 𝑁 = ( LSpan ‘ 𝑈 )
18 mapdrvallem2.z 0 = ( 0g𝑈 )
19 mapdrvallem2.y 𝑌 = ( 0g𝐷 )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 mapdrvallem2 ( 𝜑 → { 𝑓𝐶 ∣ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 } ⊆ 𝑅 )
21 2fveq3 ( = 𝑓 → ( 𝑂 ‘ ( 𝐿 ) ) = ( 𝑂 ‘ ( 𝐿𝑓 ) ) )
22 21 ssiun2s ( 𝑓𝑅 → ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑅 ( 𝑂 ‘ ( 𝐿 ) ) )
23 22 adantl ( ( 𝜑𝑓𝑅 ) → ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑅 ( 𝑂 ‘ ( 𝐿 ) ) )
24 23 14 sseqtrrdi ( ( 𝜑𝑓𝑅 ) → ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 )
25 13 24 ssrabdv ( 𝜑𝑅 ⊆ { 𝑓𝐶 ∣ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 } )
26 20 25 eqssd ( 𝜑 → { 𝑓𝐶 ∣ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 } = 𝑅 )