hdmap1fval - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hdmap1fval		Structured version Visualization version GIF version

Theorem hdmap1fval 40259

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
hdmap1fval	⊢ (𝜑 → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))))))

Distinct variable groups: 𝑥,ℎ,𝐶 𝐷,ℎ,𝑥 ℎ,𝐽,𝑥 ℎ,𝑀,𝑥 ℎ,𝑁,𝑥 𝑈,ℎ,𝑥 ℎ,𝑉,𝑥 Allowed substitution hints: 𝜑(𝑥,ℎ) 𝐴(𝑥,ℎ) 𝑄(𝑥,ℎ) 𝑅(𝑥,ℎ) 𝐻(𝑥,ℎ) 𝐼(𝑥,ℎ) 𝐾(𝑥,ℎ) − (𝑥,ℎ) 𝑊(𝑥,ℎ) 0 (𝑥,ℎ)

Proof of Theorem hdmap1fval Dummy variables 𝑤 𝑎 𝑐 𝑑 𝑗 𝑚 𝑛 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hdmap1fval.k	. 2 ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))
2		hdmap1fval.i	. . . 4 ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)
3		hdmap1val.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
4	3	hdmap1ffval 40258	. . . . 5 ⊢ (𝐾 ∈ 𝐴 → (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‘𝑐)ℎ)})))))}))
5	4	fveq1d 6844	. . . 4 ⊢ (𝐾 ∈ 𝐴 → ((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‘𝑐)ℎ)})))))})‘𝑊))
6	2, 5	eqtrid 2788	. . 3 ⊢ (𝐾 ∈ 𝐴 → 𝐼 = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((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‘𝑐)ℎ)})))))})‘𝑊))
7		fveq2 6842	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊))
8		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((LCDual‘𝐾)‘𝑤) = ((LCDual‘𝐾)‘𝑊))
9		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → ((mapd‘𝐾)‘𝑤) = ((mapd‘𝐾)‘𝑊))
10	9	sbceq1d 3744	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → ([((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‘𝑐)ℎ)})))))))
11	10	sbcbidv 3798	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → ([(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‘𝑐)ℎ)})))))))
12	11	sbcbidv 3798	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ([(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‘𝑐)ℎ)})))))))
13	8, 12	sbceqbid 3746	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ([((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‘𝑐)ℎ)})))))))
14	13	sbcbidv 3798	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ([(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‘𝑐)ℎ)})))))))
15	14	sbcbidv 3798	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ([(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‘𝑐)ℎ)})))))))
16	7, 15	sbceqbid 3746	. . . . . 6 ⊢ (𝑤 = 𝑊 → ([((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‘𝑐)ℎ)})))))))
17		fvex 6855	. . . . . . 7 ⊢ ((DVecH‘𝐾)‘𝑊) ∈ V
18		fvex 6855	. . . . . . 7 ⊢ (Base‘𝑢) ∈ V
19		fvex 6855	. . . . . . 7 ⊢ (LSpan‘𝑢) ∈ V
20		hdmap1fval.u	. . . . . . . . . . 11 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
21	20	eqeq2i 2749	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 ↔ 𝑢 = ((DVecH‘𝐾)‘𝑊))
22	21	biimpri 227	. . . . . . . . 9 ⊢ (𝑢 = ((DVecH‘𝐾)‘𝑊) → 𝑢 = 𝑈)
23	22	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑢 = 𝑈)
24		simp2 1137	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = (Base‘𝑢))
25	22	fveq2d 6846	. . . . . . . . . . 11 ⊢ (𝑢 = ((DVecH‘𝐾)‘𝑊) → (Base‘𝑢) = (Base‘𝑈))
26	25	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → (Base‘𝑢) = (Base‘𝑈))
27	24, 26	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = (Base‘𝑈))
28		hdmap1fval.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑈)
29	27, 28	eqtr4di 2794	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = 𝑉)
30		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = (LSpan‘𝑢))
31	23	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → (LSpan‘𝑢) = (LSpan‘𝑈))
32	30, 31	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = (LSpan‘𝑈))
33		hdmap1fval.n	. . . . . . . . 9 ⊢ 𝑁 = (LSpan‘𝑈)
34	32, 33	eqtr4di 2794	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = 𝑁)
35		fvex 6855	. . . . . . . . . 10 ⊢ ((LCDual‘𝐾)‘𝑊) ∈ V
36		fvex 6855	. . . . . . . . . 10 ⊢ (Base‘𝑐) ∈ V
37		fvex 6855	. . . . . . . . . 10 ⊢ (LSpan‘𝑐) ∈ V
38		id 22	. . . . . . . . . . . . 13 ⊢ (𝑐 = ((LCDual‘𝐾)‘𝑊) → 𝑐 = ((LCDual‘𝐾)‘𝑊))
39		hdmap1fval.c	. . . . . . . . . . . . 13 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
40	38, 39	eqtr4di 2794	. . . . . . . . . . . 12 ⊢ (𝑐 = ((LCDual‘𝐾)‘𝑊) → 𝑐 = 𝐶)
41	40	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑐 = 𝐶)
42		simp2 1137	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑑 = (Base‘𝑐))
43	41	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (Base‘𝑐) = (Base‘𝐶))
44		hdmap1fval.d	. . . . . . . . . . . . 13 ⊢ 𝐷 = (Base‘𝐶)
45	43, 44	eqtr4di 2794	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (Base‘𝑐) = 𝐷)
46	42, 45	eqtrd 2776	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑑 = 𝐷)
47		simp3 1138	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑗 = (LSpan‘𝑐))
48	41	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (LSpan‘𝑐) = (LSpan‘𝐶))
49		hdmap1fval.j	. . . . . . . . . . . . 13 ⊢ 𝐽 = (LSpan‘𝐶)
50	48, 49	eqtr4di 2794	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (LSpan‘𝑐) = 𝐽)
51	47, 50	eqtrd 2776	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑗 = 𝐽)
52		fvex 6855	. . . . . . . . . . . . 13 ⊢ ((mapd‘𝐾)‘𝑊) ∈ V
53		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → 𝑚 = ((mapd‘𝐾)‘𝑊))
54		hdmap1fval.m	. . . . . . . . . . . . . . 15 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
55	53, 54	eqtr4di 2794	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → 𝑚 = 𝑀)
56		fveq1 6841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑀 → (𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑀‘(𝑛‘{(2^nd ‘𝑥)})))
57	56	eqeq1d 2738	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑀 → ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ↔ (𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ})))
58		fveq1 6841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑀 → (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑀‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})))
59	58	eqeq1d 2738	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑀 → ((𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)}) ↔ (𝑀‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)})))
60	57, 59	anbi12d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑀 → (((𝑚‘(𝑛‘{(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‘𝑐)ℎ)}))))
61	60	riotabidv 7315	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑀 → (℩ℎ ∈ 𝑑 ((𝑚‘(𝑛‘{(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‘𝑐)ℎ)}))))
62	61	ifeq2d 4506	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → 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‘𝑐)ℎ)})))))
63	62	mpteq2dv 5207	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ 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‘𝑐)ℎ)}))))))
64	63	eleq2d 2823	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑀 → (𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ 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‘𝑐)ℎ)})))))))
65	55, 64	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑚 = ((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‘𝑐)ℎ)})))))))
66	52, 65	sbcie 3782	. . . . . . . . . . . 12 ⊢ ([((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‘𝑐)ℎ)}))))))
67		simp2 1137	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑑 = 𝐷)
68		xpeq2 5654	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝐷 → (𝑣 × 𝑑) = (𝑣 × 𝐷))
69	68	xpeq1d 5662	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝐷 → ((𝑣 × 𝑑) × 𝑣) = ((𝑣 × 𝐷) × 𝑣))
70	67, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑣 × 𝑑) × 𝑣) = ((𝑣 × 𝐷) × 𝑣))
71		simp1 1136	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑐 = 𝐶)
72	71	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (0_g‘𝑐) = (0_g‘𝐶))
73		hdmap1fval.q	. . . . . . . . . . . . . . . 16 ⊢ 𝑄 = (0_g‘𝐶)
74	72, 73	eqtr4di 2794	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (0_g‘𝑐) = 𝑄)
75		simp3 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽)
76	75	fveq1d 6844	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑗‘{ℎ}) = (𝐽‘{ℎ}))
77	76	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ↔ (𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ})))
78	71	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (-_g‘𝑐) = (-_g‘𝐶))
79		hdmap1fval.r	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑅 = (-_g‘𝐶)
80	78, 79	eqtr4di 2794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (-_g‘𝑐) = 𝑅)
81	80	oveqd 7374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ) = ((2^nd ‘(1^st ‘𝑥))𝑅ℎ))
82	81	sneqd 4598	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → {((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)} = {((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})
83	75, 82	fveq12d 6849	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)}) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))
84	83	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑀‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)}) ↔ (𝑀‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})))
85	77, 84	anbi12d 631	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (((𝑀‘(𝑛‘{(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 ‘𝑥))𝑅ℎ)}))))
86	67, 85	riotaeqbidv 7316	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (℩ℎ ∈ 𝑑 ((𝑀‘(𝑛‘{(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 ‘𝑥))𝑅ℎ)}))))
87	74, 86	ifeq12d 4507	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 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 ‘𝑥))𝑅ℎ)})))))
88	70, 87	mpteq12dv 5196	. . . . . . . . . . . . 13 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ 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 ‘𝑥))𝑅ℎ)}))))))
89	88	eleq2d 2823	. . . . . . . . . . . 12 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝑑) × 𝑣) ↦ 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	66, 89	bitrid 282	. . . . . . . . . . 11 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ([((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 ‘𝑥))𝑅ℎ)})))))))
91	41, 46, 51, 90	syl3anc 1371	. . . . . . . . . 10 ⊢ ((𝑐 = ((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 ‘𝑥))𝑅ℎ)})))))))
92	35, 36, 37, 91	sbc3ie 3825	. . . . . . . . 9 ⊢ ([((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 ‘𝑥))𝑅ℎ)}))))))
93		simp2 1137	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑣 = 𝑉)
94	93	xpeq1d 5662	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑣 × 𝐷) = (𝑉 × 𝐷))
95	94, 93	xpeq12d 5664	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑣 × 𝐷) × 𝑣) = ((𝑉 × 𝐷) × 𝑉))
96		simp1 1136	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑢 = 𝑈)
97	96	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (0_g‘𝑢) = (0_g‘𝑈))
98		hdmap1fval.o	. . . . . . . . . . . . . 14 ⊢ 0 = (0_g‘𝑈)
99	97, 98	eqtr4di 2794	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (0_g‘𝑢) = 0 )
100	99	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((2^nd ‘𝑥) = (0_g‘𝑢) ↔ (2^nd ‘𝑥) = 0 ))
101		simp3 1138	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁)
102	101	fveq1d 6844	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑛‘{(2^nd ‘𝑥)}) = (𝑁‘{(2^nd ‘𝑥)}))
103	102	fveqeq2d 6850	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ})))
104	96	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (-_g‘𝑢) = (-_g‘𝑈))
105		hdmap1fval.s	. . . . . . . . . . . . . . . . . . 19 ⊢ − = (-_g‘𝑈)
106	104, 105	eqtr4di 2794	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (-_g‘𝑢) = − )
107	106	oveqd 7374	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥)) = ((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥)))
108	107	sneqd 4598	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → {((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))} = {((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})
109	101, 108	fveq12d 6849	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))}) = (𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))}))
110	109	fveqeq2d 6850	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑀‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})))
111	103, 110	anbi12d 631	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (((𝑀‘(𝑛‘{(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 7315	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (℩ℎ ∈ 𝐷 ((𝑀‘(𝑛‘{(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	100, 112	ifbieq2d 4512	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 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	95, 113	mpteq12dv 5196	. . . . . . . . . 10 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑥 ∈ ((𝑣 × 𝐷) × 𝑣) ↦ 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 2823	. . . . . . . . 9 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑎 ∈ (𝑥 ∈ ((𝑣 × 𝐷) × 𝑣) ↦ 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	92, 115	bitrid 282	. . . . . . . 8 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ([((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	23, 29, 34, 116	syl3anc 1371	. . . . . . 7 ⊢ ((𝑢 = ((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	17, 18, 19, 117	sbc3ie 3825	. . . . . 6 ⊢ ([((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	16, 118	bitrdi 286	. . . . 5 ⊢ (𝑤 = 𝑊 → ([((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	abbi1dv 2872	. . . 4 ⊢ (𝑤 = 𝑊 → {𝑎 ∣ [((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 2736	. . . 4 ⊢ (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((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	28	fvexi 6856	. . . . . . 7 ⊢ 𝑉 ∈ V
123	44	fvexi 6856	. . . . . . 7 ⊢ 𝐷 ∈ V
124	122, 123	xpex 7687	. . . . . 6 ⊢ (𝑉 × 𝐷) ∈ V
125	124, 122	xpex 7687	. . . . 5 ⊢ ((𝑉 × 𝐷) × 𝑉) ∈ V
126	125	mptex 7173	. . . 4 ⊢ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))))) ∈ V
127	120, 121, 126	fvmpt 6948	. . 3 ⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [((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	6, 127	sylan9eq 2796	. 2 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))))))
129	1, 128	syl 17	1 ⊢ (𝜑 → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 {cab 2713 [wsbc 3739 ifcif 4486 {csn 4586 ↦ cmpt 5188 × cxp 5631 ‘cfv 6496 ℩crio 7312 (class class class)co 7357 1^st c1st 7919 2^nd c2nd 7920 Basecbs 17083 0_gc0g 17321 -_gcsg 18750 LSpanclspn 20432 LHypclh 38447 DVecHcdvh 39541 LCDualclcd 40049 mapdcmpd 40087 HDMap1chdma1 40254

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-hdmap1 40256

This theorem is referenced by: hdmap1vallem 40260

W3C validator