Metamath Proof Explorer

Theorem hdmapfval

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

Ref Expression
Hypotheses hdmapval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapfval.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmapfval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapfval.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmapfval.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
hdmapfval.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmapfval.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
hdmapfval.j ⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapfval.i ⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
hdmapfval.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapfval.k ⊢ ( 𝜑 → ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) )
Assertion hdmapfval ( 𝜑 → 𝑆 = ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hdmapval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapfval.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3 hdmapfval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 hdmapfval.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 hdmapfval.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6 hdmapfval.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7 hdmapfval.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
8 hdmapfval.j ⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
9 hdmapfval.i ⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
10 hdmapfval.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11 hdmapfval.k ⊢ ( 𝜑 → ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) )
12 1 hdmapffval ⊢ ( 𝐾 ∈ 𝐴 → ( HDMap ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } ) )
13 12 fveq1d ⊢ ( 𝐾 ∈ 𝐴 → ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } ) ‘ 𝑊 ) )
14 10 13 eqtrid ⊢ ( 𝐾 ∈ 𝐴 → 𝑆 = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } ) ‘ 𝑊 ) )
15 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
16 15 reseq2d ⊢ ( 𝑤 = 𝑊 → ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) = ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) )
17 16 opeq2d ⊢ ( 𝑤 = 𝑊 → ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ⟩ = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ )
18 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
19 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) )
20 2fveq3 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
21 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) )
22 21 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) = ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) )
23 22 oteq2d ⊢ ( 𝑤 = 𝑊 → ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ = ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ )
24 23 fveq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) = ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) )
25 24 oteq2d ⊢ ( 𝑤 = 𝑊 → ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ = ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ )
26 25 fveq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) )
27 26 eqeq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ↔ 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) )
28 27 imbi2d ⊢ ( 𝑤 = 𝑊 → ( ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ↔ ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
29 28 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ↔ ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
30 20 29 riotaeqbidv ⊢ ( 𝑤 = 𝑊 → ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) = ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
31 30 mpteq2dv ⊢ ( 𝑤 = 𝑊 → ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) = ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )
32 31 eleq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
33 19 32 sbceqbid ⊢ ( 𝑤 = 𝑊 → ( [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
34 33 sbcbidv ⊢ ( 𝑤 = 𝑊 → ( [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
35 18 34 sbceqbid ⊢ ( 𝑤 = 𝑊 → ( [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
36 17 35 sbceqbid ⊢ ( 𝑤 = 𝑊 → ( [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
37 opex ⊢ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ V
38 fvex ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
39 fvex ⊢ ( Base ‘ 𝑢 ) ∈ V
40 simp1 ⊢ ( ( 𝑒 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∧ 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → 𝑒 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ )
41 40 2 eqtr4di ⊢ ( ( 𝑒 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∧ 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → 𝑒 = 𝐸 )
42 simp2 ⊢ ( ( 𝑒 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∧ 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
43 42 3 eqtr4di ⊢ ( ( 𝑒 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∧ 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → 𝑢 = 𝑈 )
44 simp3 ⊢ ( ( 𝑒 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∧ 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → 𝑣 = ( Base ‘ 𝑢 ) )
45 43 fveq2d ⊢ ( ( 𝑒 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∧ 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( Base ‘ 𝑢 ) = ( Base ‘ 𝑈 ) )
46 44 45 eqtrd ⊢ ( ( 𝑒 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∧ 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → 𝑣 = ( Base ‘ 𝑈 ) )
47 46 4 eqtr4di ⊢ ( ( 𝑒 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∧ 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → 𝑣 = 𝑉 )
48 fvex ⊢ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
49 id ⊢ ( 𝑖 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) → 𝑖 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) )
50 49 9 eqtr4di ⊢ ( 𝑖 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) → 𝑖 = 𝐼 )
51 fveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) )
52 fveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) = ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) )
53 52 oteq2d ⊢ ( 𝑖 = 𝐼 → ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ = ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ )
54 53 fveq2d ⊢ ( 𝑖 = 𝐼 → ( 𝐼 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) )
55 51 54 eqtrd ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) )
56 55 eqeq2d ⊢ ( 𝑖 = 𝐼 → ( 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ↔ 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) )
57 56 imbi2d ⊢ ( 𝑖 = 𝐼 → ( ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ↔ ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
58 57 ralbidv ⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ↔ ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
59 58 riotabidv ⊢ ( 𝑖 = 𝐼 → ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) = ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
60 59 mpteq2dv ⊢ ( 𝑖 = 𝐼 → ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) = ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )
61 60 eleq2d ⊢ ( 𝑖 = 𝐼 → ( 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
62 50 61 syl ⊢ ( 𝑖 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) → ( 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
63 48 62 sbcie ⊢ ( [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )
64 simp3 ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → 𝑣 = 𝑉 )
65 6 fveq2i ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
66 7 65 eqtr2i ⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝐷
67 66 a1i ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝐷 )
68 simp2 ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → 𝑢 = 𝑈 )
69 68 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( LSpan ‘ 𝑢 ) = ( LSpan ‘ 𝑈 ) )
70 69 5 eqtr4di ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( LSpan ‘ 𝑢 ) = 𝑁 )
71 simp1 ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → 𝑒 = 𝐸 )
72 71 sneqd ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → { 𝑒 } = { 𝐸 } )
73 70 72 fveq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) = ( 𝑁 ‘ { 𝐸 } ) )
74 70 fveq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) = ( 𝑁 ‘ { 𝑡 } ) )
75 73 74 uneq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) = ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) )
76 75 eleq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) ↔ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) ) )
77 76 notbid ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) ↔ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) ) )
78 71 oteq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ = ⟨ 𝐸 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ )
79 71 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) = ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐸 ) )
80 8 fveq1i ⊢ ( 𝐽 ‘ 𝐸 ) = ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐸 )
81 79 80 eqtr4di ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) = ( 𝐽 ‘ 𝐸 ) )
82 81 oteq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ⟨ 𝐸 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ = ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ )
83 78 82 eqtrd ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ = ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ )
84 83 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) )
85 84 oteq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ = ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ )
86 85 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) )
87 86 eqeq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ↔ 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) )
88 77 87 imbi12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ↔ ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
89 64 88 raleqbidv ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ↔ ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
90 67 89 riotaeqbidv ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) = ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
91 64 90 mpteq12dv ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) = ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )
92 91 eleq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ 𝑎 ∈ ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
93 63 92 bitrid ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) → ( [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ 𝑎 ∈ ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
94 41 43 47 93 syl3anc ⊢ ( ( 𝑒 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∧ 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ) → ( [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ 𝑎 ∈ ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
95 37 38 39 94 sbc3ie ⊢ ( [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ 𝑎 ∈ ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )
96 36 95 bitrdi ⊢ ( 𝑤 = 𝑊 → ( [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ↔ 𝑎 ∈ ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ) )
97 96 eqabcdv ⊢ ( 𝑤 = 𝑊 → { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } = ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )
98 eqid ⊢ ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } )
99 97 98 4 mptfvmpt ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ) ⟩ / 𝑒 ] [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑤 ) / 𝑖 ] 𝑎 ∈ ( 𝑡 ∈ 𝑣 ↦ ( ℩ 𝑦 ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) ) ∀ 𝑧 ∈ 𝑣 ( ¬ 𝑧 ∈ ( ( ( LSpan ‘ 𝑢 ) ‘ { 𝑒 } ) ∪ ( ( LSpan ‘ 𝑢 ) ‘ { 𝑡 } ) ) → 𝑦 = ( 𝑖 ‘ ⟨ 𝑧 , ( 𝑖 ‘ ⟨ 𝑒 , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑤 ) ‘ 𝑒 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) } ) ‘ 𝑊 ) = ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )
100 14 99 sylan9eq ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → 𝑆 = ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )
101 11 100 syl ⊢ ( 𝜑 → 𝑆 = ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )