# Metamath Proof Explorer

## Theorem hdmap1vallem

Description: Value of preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmap1val.h 𝐻 = ( LHyp ‘ 𝐾 )
hdmap1fval.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmap1fval.v 𝑉 = ( Base ‘ 𝑈 )
hdmap1fval.s = ( -g𝑈 )
hdmap1fval.o 0 = ( 0g𝑈 )
hdmap1fval.n 𝑁 = ( LSpan ‘ 𝑈 )
hdmap1fval.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmap1fval.d 𝐷 = ( Base ‘ 𝐶 )
hdmap1fval.r 𝑅 = ( -g𝐶 )
hdmap1fval.q 𝑄 = ( 0g𝐶 )
hdmap1fval.j 𝐽 = ( LSpan ‘ 𝐶 )
hdmap1fval.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
hdmap1fval.i 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
hdmap1fval.k ( 𝜑 → ( 𝐾𝐴𝑊𝐻 ) )
hdmap1val.t ( 𝜑𝑇 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) )
Assertion hdmap1vallem ( 𝜑 → ( 𝐼𝑇 ) = if ( ( 2nd𝑇 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) ) ) )

### Proof

Step Hyp Ref Expression
1 hdmap1val.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmap1fval.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmap1fval.v 𝑉 = ( Base ‘ 𝑈 )
4 hdmap1fval.s = ( -g𝑈 )
5 hdmap1fval.o 0 = ( 0g𝑈 )
6 hdmap1fval.n 𝑁 = ( LSpan ‘ 𝑈 )
7 hdmap1fval.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8 hdmap1fval.d 𝐷 = ( Base ‘ 𝐶 )
9 hdmap1fval.r 𝑅 = ( -g𝐶 )
10 hdmap1fval.q 𝑄 = ( 0g𝐶 )
11 hdmap1fval.j 𝐽 = ( LSpan ‘ 𝐶 )
12 hdmap1fval.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
13 hdmap1fval.i 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
14 hdmap1fval.k ( 𝜑 → ( 𝐾𝐴𝑊𝐻 ) )
15 hdmap1val.t ( 𝜑𝑇 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 hdmap1fval ( 𝜑𝐼 = ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2nd𝑥 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) ) ) )
17 16 fveq1d ( 𝜑 → ( 𝐼𝑇 ) = ( ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2nd𝑥 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) ) ) ‘ 𝑇 ) )
18 10 fvexi 𝑄 ∈ V
19 riotaex ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) ) ∈ V
20 18 19 ifex if ( ( 2nd𝑇 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) ) ) ∈ V
21 fveqeq2 ( 𝑥 = 𝑇 → ( ( 2nd𝑥 ) = 0 ↔ ( 2nd𝑇 ) = 0 ) )
22 fveq2 ( 𝑥 = 𝑇 → ( 2nd𝑥 ) = ( 2nd𝑇 ) )
23 22 sneqd ( 𝑥 = 𝑇 → { ( 2nd𝑥 ) } = { ( 2nd𝑇 ) } )
24 23 fveq2d ( 𝑥 = 𝑇 → ( 𝑁 ‘ { ( 2nd𝑥 ) } ) = ( 𝑁 ‘ { ( 2nd𝑇 ) } ) )
25 24 fveqeq2d ( 𝑥 = 𝑇 → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ) )
26 2fveq3 ( 𝑥 = 𝑇 → ( 1st ‘ ( 1st𝑥 ) ) = ( 1st ‘ ( 1st𝑇 ) ) )
27 26 22 oveq12d ( 𝑥 = 𝑇 → ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) = ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) )
28 27 sneqd ( 𝑥 = 𝑇 → { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } = { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } )
29 28 fveq2d ( 𝑥 = 𝑇 → ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) = ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) )
30 29 fveq2d ( 𝑥 = 𝑇 → ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) )
31 2fveq3 ( 𝑥 = 𝑇 → ( 2nd ‘ ( 1st𝑥 ) ) = ( 2nd ‘ ( 1st𝑇 ) ) )
32 31 oveq1d ( 𝑥 = 𝑇 → ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) = ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) )
33 32 sneqd ( 𝑥 = 𝑇 → { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } = { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } )
34 33 fveq2d ( 𝑥 = 𝑇 → ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) )
35 30 34 eqeq12d ( 𝑥 = 𝑇 → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) )
36 25 35 anbi12d ( 𝑥 = 𝑇 → ( ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ↔ ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) ) )
37 36 riotabidv ( 𝑥 = 𝑇 → ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) = ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) ) )
38 21 37 ifbieq2d ( 𝑥 = 𝑇 → if ( ( 2nd𝑥 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) ) = if ( ( 2nd𝑇 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) ) ) )
39 eqid ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2nd𝑥 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) ) ) = ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2nd𝑥 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) ) )
40 38 39 fvmptg ( ( 𝑇 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ∧ if ( ( 2nd𝑇 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) ) ) ∈ V ) → ( ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2nd𝑥 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) ) ) ‘ 𝑇 ) = if ( ( 2nd𝑇 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) ) ) )
41 15 20 40 sylancl ( 𝜑 → ( ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2nd𝑥 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) ) ) ‘ 𝑇 ) = if ( ( 2nd𝑇 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) ) ) )
42 17 41 eqtrd ( 𝜑 → ( 𝐼𝑇 ) = if ( ( 2nd𝑇 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑇 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑇 ) ) ( 2nd𝑇 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑇 ) ) 𝑅 ) } ) ) ) ) )