hdmap1fval

Description: Preliminary map from vectors to functionals in the closed kernel dual space. TODO: change span J to the convention L for this section. (Contributed by NM, 15-May-2015)

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

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 = ( 0_g ‘ 𝑈 )
6		hdmap1fval.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7		hdmap1fval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8		hdmap1fval.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
9		hdmap1fval.r	⊢ 𝑅 = ( -_g ‘ 𝐶 )
10		hdmap1fval.q	⊢ 𝑄 = ( 0_g ‘ 𝐶 )
11		hdmap1fval.j	⊢ 𝐽 = ( LSpan ‘ 𝐶 )
12		hdmap1fval.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
13		hdmap1fval.i	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
14		hdmap1fval.k	⊢ ( 𝜑 → ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) )
15	1	hdmap1ffval	⊢ ( 𝐾 ∈ 𝐴 → ( HDMap1 ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) )
16	15	fveq1d	⊢ ( 𝐾 ∈ 𝐴 → ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) ‘ 𝑊 ) )
17	13 16	eqtrid	⊢ ( 𝐾 ∈ 𝐴 → 𝐼 = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) ‘ 𝑊 ) )
18		fveq2	⊢ ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
19		fveq2	⊢ ( 𝑤 = 𝑊 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
20		fveq2	⊢ ( 𝑤 = 𝑊 → ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) )
21	20	sbceq1d	⊢ ( 𝑤 = 𝑊 → ( [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) )
22	21	sbcbidv	⊢ ( 𝑤 = 𝑊 → ( [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) )
23	22	sbcbidv	⊢ ( 𝑤 = 𝑊 → ( [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) )
24	19 23	sbceqbid	⊢ ( 𝑤 = 𝑊 → ( [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) )
25	24	sbcbidv	⊢ ( 𝑤 = 𝑊 → ( [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) )
26	25	sbcbidv	⊢ ( 𝑤 = 𝑊 → ( [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) )
27	18 26	sbceqbid	⊢ ( 𝑤 = 𝑊 → ( [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) )
28		fvex	⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
29		fvex	⊢ ( Base ‘ 𝑢 ) ∈ V
30		fvex	⊢ ( LSpan ‘ 𝑢 ) ∈ V
31	2	eqeq2i	⊢ ( 𝑢 = 𝑈 ↔ 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
32	31	biimpri	⊢ ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) → 𝑢 = 𝑈 )
33	32	3ad2ant1	⊢ ( ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ∧ 𝑛 = ( LSpan ‘ 𝑢 ) ) → 𝑢 = 𝑈 )
34		simp2	⊢ ( ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ∧ 𝑛 = ( LSpan ‘ 𝑢 ) ) → 𝑣 = ( Base ‘ 𝑢 ) )
35	32	fveq2d	⊢ ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) → ( Base ‘ 𝑢 ) = ( Base ‘ 𝑈 ) )
36	35	3ad2ant1	⊢ ( ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ∧ 𝑛 = ( LSpan ‘ 𝑢 ) ) → ( Base ‘ 𝑢 ) = ( Base ‘ 𝑈 ) )
37	34 36	eqtrd	⊢ ( ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ∧ 𝑛 = ( LSpan ‘ 𝑢 ) ) → 𝑣 = ( Base ‘ 𝑈 ) )
38	37 3	eqtr4di	⊢ ( ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ∧ 𝑛 = ( LSpan ‘ 𝑢 ) ) → 𝑣 = 𝑉 )
39		simp3	⊢ ( ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ∧ 𝑛 = ( LSpan ‘ 𝑢 ) ) → 𝑛 = ( LSpan ‘ 𝑢 ) )
40	33	fveq2d	⊢ ( ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ∧ 𝑛 = ( LSpan ‘ 𝑢 ) ) → ( LSpan ‘ 𝑢 ) = ( LSpan ‘ 𝑈 ) )
41	39 40	eqtrd	⊢ ( ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ∧ 𝑛 = ( LSpan ‘ 𝑢 ) ) → 𝑛 = ( LSpan ‘ 𝑈 ) )
42	41 6	eqtr4di	⊢ ( ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ∧ 𝑛 = ( LSpan ‘ 𝑢 ) ) → 𝑛 = 𝑁 )
43		fvex	⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
44		fvex	⊢ ( Base ‘ 𝑐 ) ∈ V
45		fvex	⊢ ( LSpan ‘ 𝑐 ) ∈ V
46		id	⊢ ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) → 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
47	46 7	eqtr4di	⊢ ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) → 𝑐 = 𝐶 )
48	47	3ad2ant1	⊢ ( ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑑 = ( Base ‘ 𝑐 ) ∧ 𝑗 = ( LSpan ‘ 𝑐 ) ) → 𝑐 = 𝐶 )
49		simp2	⊢ ( ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑑 = ( Base ‘ 𝑐 ) ∧ 𝑗 = ( LSpan ‘ 𝑐 ) ) → 𝑑 = ( Base ‘ 𝑐 ) )
50	48	fveq2d	⊢ ( ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑑 = ( Base ‘ 𝑐 ) ∧ 𝑗 = ( LSpan ‘ 𝑐 ) ) → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
51	50 8	eqtr4di	⊢ ( ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑑 = ( Base ‘ 𝑐 ) ∧ 𝑗 = ( LSpan ‘ 𝑐 ) ) → ( Base ‘ 𝑐 ) = 𝐷 )
52	49 51	eqtrd	⊢ ( ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑑 = ( Base ‘ 𝑐 ) ∧ 𝑗 = ( LSpan ‘ 𝑐 ) ) → 𝑑 = 𝐷 )
53		simp3	⊢ ( ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑑 = ( Base ‘ 𝑐 ) ∧ 𝑗 = ( LSpan ‘ 𝑐 ) ) → 𝑗 = ( LSpan ‘ 𝑐 ) )
54	48	fveq2d	⊢ ( ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑑 = ( Base ‘ 𝑐 ) ∧ 𝑗 = ( LSpan ‘ 𝑐 ) ) → ( LSpan ‘ 𝑐 ) = ( LSpan ‘ 𝐶 ) )
55	54 11	eqtr4di	⊢ ( ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑑 = ( Base ‘ 𝑐 ) ∧ 𝑗 = ( LSpan ‘ 𝑐 ) ) → ( LSpan ‘ 𝑐 ) = 𝐽 )
56	53 55	eqtrd	⊢ ( ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑑 = ( Base ‘ 𝑐 ) ∧ 𝑗 = ( LSpan ‘ 𝑐 ) ) → 𝑗 = 𝐽 )
57		fvex	⊢ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
58		id	⊢ ( 𝑚 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) → 𝑚 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) )
59	58 12	eqtr4di	⊢ ( 𝑚 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) → 𝑚 = 𝑀 )
60		fveq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) )
61	60	eqeq1d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ↔ ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ) )
62		fveq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) )
63	62	eqeq1d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ↔ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) )
64	61 63	anbi12d	⊢ ( 𝑚 = 𝑀 → ( ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ↔ ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) )
65	64	riotabidv	⊢ ( 𝑚 = 𝑀 → ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) = ( ℩ ℎ ∈ 𝑑 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) )
66	65	ifeq2d	⊢ ( 𝑚 = 𝑀 → if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) = if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) )
67	66	mpteq2dv	⊢ ( 𝑚 = 𝑀 → ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) = ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) )
68	67	eleq2d	⊢ ( 𝑚 = 𝑀 → ( 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) )
69	59 68	syl	⊢ ( 𝑚 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) → ( 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ) )
70	57 69	sbcie	⊢ ( [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) )
71		simp2	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → 𝑑 = 𝐷 )
72		xpeq2	⊢ ( 𝑑 = 𝐷 → ( 𝑣 × 𝑑 ) = ( 𝑣 × 𝐷 ) )
73	72	xpeq1d	⊢ ( 𝑑 = 𝐷 → ( ( 𝑣 × 𝑑 ) × 𝑣 ) = ( ( 𝑣 × 𝐷 ) × 𝑣 ) )
74	71 73	syl	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( ( 𝑣 × 𝑑 ) × 𝑣 ) = ( ( 𝑣 × 𝐷 ) × 𝑣 ) )
75		simp1	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → 𝑐 = 𝐶 )
76	75	fveq2d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( 0_g ‘ 𝑐 ) = ( 0_g ‘ 𝐶 ) )
77	76 10	eqtr4di	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( 0_g ‘ 𝑐 ) = 𝑄 )
78		simp3	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → 𝑗 = 𝐽 )
79	78	fveq1d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( 𝑗 ‘ { ℎ } ) = ( 𝐽 ‘ { ℎ } ) )
80	79	eqeq2d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ↔ ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ) )
81	75	fveq2d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( -_g ‘ 𝑐 ) = ( -_g ‘ 𝐶 ) )
82	81 9	eqtr4di	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( -_g ‘ 𝑐 ) = 𝑅 )
83	82	oveqd	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) )
84	83	sneqd	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } = { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } )
85	78 84	fveq12d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) )
86	85	eqeq2d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ↔ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) )
87	80 86	anbi12d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ↔ ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) )
88	71 87	riotaeqbidv	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( ℩ ℎ ∈ 𝑑 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) )
89	77 88	ifeq12d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) = if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) )
90	74 89	mpteq12dv	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) = ( 𝑥 ∈ ( ( 𝑣 × 𝐷 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) )
91	90	eleq2d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝐷 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ) )
92	70 91	bitrid	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽 ) → ( [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝐷 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ) )
93	48 52 56 92	syl3anc	⊢ ( ( 𝑐 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑑 = ( Base ‘ 𝑐 ) ∧ 𝑗 = ( LSpan ‘ 𝑐 ) ) → ( [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝐷 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ) )
94	43 44 45 93	sbc3ie	⊢ ( [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝐷 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) )
95		simp2	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → 𝑣 = 𝑉 )
96	95	xpeq1d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( 𝑣 × 𝐷 ) = ( 𝑉 × 𝐷 ) )
97	96 95	xpeq12d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( ( 𝑣 × 𝐷 ) × 𝑣 ) = ( ( 𝑉 × 𝐷 ) × 𝑉 ) )
98		simp1	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → 𝑢 = 𝑈 )
99	98	fveq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( 0_g ‘ 𝑢 ) = ( 0_g ‘ 𝑈 ) )
100	99 5	eqtr4di	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( 0_g ‘ 𝑢 ) = 0 )
101	100	eqeq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) ↔ ( 2^nd ‘ 𝑥 ) = 0 ) )
102		simp3	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → 𝑛 = 𝑁 )
103	102	fveq1d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) = ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) )
104	103	fveqeq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ) )
105	98	fveq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( -_g ‘ 𝑢 ) = ( -_g ‘ 𝑈 ) )
106	105 4	eqtr4di	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( -_g ‘ 𝑢 ) = − )
107	106	oveqd	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) )
108	107	sneqd	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } = { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } )
109	102 108	fveq12d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) = ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) )
110	109	fveqeq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) )
111	104 110	anbi12d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ↔ ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) )
112	111	riotabidv	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) )
113	101 112	ifbieq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) = if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) )
114	97 113	mpteq12dv	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( 𝑥 ∈ ( ( 𝑣 × 𝐷 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) = ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) )
115	114	eleq2d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝐷 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ) )
116	94 115	bitrid	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁 ) → ( [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ) )
117	33 38 42 116	syl3anc	⊢ ( ( 𝑢 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑣 = ( Base ‘ 𝑢 ) ∧ 𝑛 = ( LSpan ‘ 𝑢 ) ) → ( [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ) )
118	28 29 30 117	sbc3ie	⊢ ( [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) )
119	27 118	bitrdi	⊢ ( 𝑤 = 𝑊 → ( [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) ↔ 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ) )
120	119	eqabcdv	⊢ ( 𝑤 = 𝑊 → { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } = ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) )
121		eqid	⊢ ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } )
122	3	fvexi	⊢ 𝑉 ∈ V
123	8	fvexi	⊢ 𝐷 ∈ V
124	122 123	xpex	⊢ ( 𝑉 × 𝐷 ) ∈ V
125	124 122	xpex	⊢ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ∈ V
126	125	mptex	⊢ ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) ∈ V
127	120 121 126	fvmpt	⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ { 𝑎 ∣ [ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) / 𝑢 ] [ ( Base ‘ 𝑢 ) / 𝑣 ] [ ( LSpan ‘ 𝑢 ) / 𝑛 ] [ ( ( LCDual ‘ 𝐾 ) ‘ 𝑤 ) / 𝑐 ] [ ( Base ‘ 𝑐 ) / 𝑑 ] [ ( LSpan ‘ 𝑐 ) / 𝑗 ] [ ( ( mapd ‘ 𝐾 ) ‘ 𝑤 ) / 𝑚 ] 𝑎 ∈ ( 𝑥 ∈ ( ( 𝑣 × 𝑑 ) × 𝑣 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = ( 0_g ‘ 𝑢 ) , ( 0_g ‘ 𝑐 ) , ( ℩ ℎ ∈ 𝑑 ( ( 𝑚 ‘ ( 𝑛 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑗 ‘ { ℎ } ) ∧ ( 𝑚 ‘ ( 𝑛 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑢 ) ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑗 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( -_g ‘ 𝑐 ) ℎ ) } ) ) ) ) ) } ) ‘ 𝑊 ) = ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) )
128	17 127	sylan9eq	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) )
129	14 128	syl	⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ ( ( 𝑉 × 𝐷 ) × 𝑉 ) ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) ) )

Metamath Proof Explorer

Theorem hdmap1fval

Proof