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 39737

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 39736	. . . . 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 6758	. . . 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	syl5eq 2791	. . 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 6756	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊))
8		fveq2 6756	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((LCDual‘𝐾)‘𝑤) = ((LCDual‘𝐾)‘𝑊))
9		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → ((mapd‘𝐾)‘𝑤) = ((mapd‘𝐾)‘𝑊))
10	9	sbceq1d 3716	. . . . . . . . . . . 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 3770	. . . . . . . . . . 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 3770	. . . . . . . . . 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 3718	. . . . . . . . 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 3770	. . . . . . . 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 3770	. . . . . . 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 3718	. . . . . 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 6769	. . . . . . 7 ⊢ ((DVecH‘𝐾)‘𝑊) ∈ V
18		fvex 6769	. . . . . . 7 ⊢ (Base‘𝑢) ∈ V
19		fvex 6769	. . . . . . 7 ⊢ (LSpan‘𝑢) ∈ V
20		hdmap1fval.u	. . . . . . . . . . 11 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
21	20	eqeq2i 2751	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 ↔ 𝑢 = ((DVecH‘𝐾)‘𝑊))
22	21	biimpri 227	. . . . . . . . 9 ⊢ (𝑢 = ((DVecH‘𝐾)‘𝑊) → 𝑢 = 𝑈)
23	22	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑢 = 𝑈)
24		simp2 1135	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = (Base‘𝑢))
25	22	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑢 = ((DVecH‘𝐾)‘𝑊) → (Base‘𝑢) = (Base‘𝑈))
26	25	3ad2ant1 1131	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → (Base‘𝑢) = (Base‘𝑈))
27	24, 26	eqtrd 2778	. . . . . . . . 9 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = (Base‘𝑈))
28		hdmap1fval.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑈)
29	27, 28	eqtr4di 2797	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = 𝑉)
30		simp3 1136	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = (LSpan‘𝑢))
31	23	fveq2d 6760	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → (LSpan‘𝑢) = (LSpan‘𝑈))
32	30, 31	eqtrd 2778	. . . . . . . . 9 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = (LSpan‘𝑈))
33		hdmap1fval.n	. . . . . . . . 9 ⊢ 𝑁 = (LSpan‘𝑈)
34	32, 33	eqtr4di 2797	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = 𝑁)
35		fvex 6769	. . . . . . . . . 10 ⊢ ((LCDual‘𝐾)‘𝑊) ∈ V
36		fvex 6769	. . . . . . . . . 10 ⊢ (Base‘𝑐) ∈ V
37		fvex 6769	. . . . . . . . . 10 ⊢ (LSpan‘𝑐) ∈ V
38		id 22	. . . . . . . . . . . . 13 ⊢ (𝑐 = ((LCDual‘𝐾)‘𝑊) → 𝑐 = ((LCDual‘𝐾)‘𝑊))
39		hdmap1fval.c	. . . . . . . . . . . . 13 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
40	38, 39	eqtr4di 2797	. . . . . . . . . . . 12 ⊢ (𝑐 = ((LCDual‘𝐾)‘𝑊) → 𝑐 = 𝐶)
41	40	3ad2ant1 1131	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑐 = 𝐶)
42		simp2 1135	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑑 = (Base‘𝑐))
43	41	fveq2d 6760	. . . . . . . . . . . . 13 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (Base‘𝑐) = (Base‘𝐶))
44		hdmap1fval.d	. . . . . . . . . . . . 13 ⊢ 𝐷 = (Base‘𝐶)
45	43, 44	eqtr4di 2797	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (Base‘𝑐) = 𝐷)
46	42, 45	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑑 = 𝐷)
47		simp3 1136	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑗 = (LSpan‘𝑐))
48	41	fveq2d 6760	. . . . . . . . . . . . 13 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (LSpan‘𝑐) = (LSpan‘𝐶))
49		hdmap1fval.j	. . . . . . . . . . . . 13 ⊢ 𝐽 = (LSpan‘𝐶)
50	48, 49	eqtr4di 2797	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (LSpan‘𝑐) = 𝐽)
51	47, 50	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑗 = 𝐽)
52		fvex 6769	. . . . . . . . . . . . 13 ⊢ ((mapd‘𝐾)‘𝑊) ∈ V
53		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → 𝑚 = ((mapd‘𝐾)‘𝑊))
54		hdmap1fval.m	. . . . . . . . . . . . . . 15 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
55	53, 54	eqtr4di 2797	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → 𝑚 = 𝑀)
56		fveq1 6755	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑀 → (𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑀‘(𝑛‘{(2^nd ‘𝑥)})))
57	56	eqeq1d 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑀 → ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ↔ (𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ})))
58		fveq1 6755	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑀 → (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑀‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})))
59	58	eqeq1d 2740	. . . . . . . . . . . . . . . . . . 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 630	. . . . . . . . . . . . . . . . . 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 7214	. . . . . . . . . . . . . . . . 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 4476	. . . . . . . . . . . . . . . 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 5172	. . . . . . . . . . . . . . 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 2824	. . . . . . . . . . . . . 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 3754	. . . . . . . . . . . 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 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑑 = 𝐷)
68		xpeq2 5601	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝐷 → (𝑣 × 𝑑) = (𝑣 × 𝐷))
69	68	xpeq1d 5609	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝐷 → ((𝑣 × 𝑑) × 𝑣) = ((𝑣 × 𝐷) × 𝑣))
70	67, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑣 × 𝑑) × 𝑣) = ((𝑣 × 𝐷) × 𝑣))
71		simp1 1134	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑐 = 𝐶)
72	71	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (0_g‘𝑐) = (0_g‘𝐶))
73		hdmap1fval.q	. . . . . . . . . . . . . . . 16 ⊢ 𝑄 = (0_g‘𝐶)
74	72, 73	eqtr4di 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (0_g‘𝑐) = 𝑄)
75		simp3 1136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽)
76	75	fveq1d 6758	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑗‘{ℎ}) = (𝐽‘{ℎ}))
77	76	eqeq2d 2749	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ↔ (𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ})))
78	71	fveq2d 6760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (-_g‘𝑐) = (-_g‘𝐶))
79		hdmap1fval.r	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑅 = (-_g‘𝐶)
80	78, 79	eqtr4di 2797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (-_g‘𝑐) = 𝑅)
81	80	oveqd 7272	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ) = ((2^nd ‘(1^st ‘𝑥))𝑅ℎ))
82	81	sneqd 4570	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → {((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)} = {((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})
83	75, 82	fveq12d 6763	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)}) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))
84	83	eqeq2d 2749	. . . . . . . . . . . . . . . . 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 630	. . . . . . . . . . . . . . . 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 7215	. . . . . . . . . . . . . . 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 4477	. . . . . . . . . . . . . 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 5161	. . . . . . . . . . . . 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 2824	. . . . . . . . . . . 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	syl5bb 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 1369	. . . . . . . . . 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 3798	. . . . . . . . 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 1135	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑣 = 𝑉)
94	93	xpeq1d 5609	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑣 × 𝐷) = (𝑉 × 𝐷))
95	94, 93	xpeq12d 5611	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑣 × 𝐷) × 𝑣) = ((𝑉 × 𝐷) × 𝑉))
96		simp1 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑢 = 𝑈)
97	96	fveq2d 6760	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (0_g‘𝑢) = (0_g‘𝑈))
98		hdmap1fval.o	. . . . . . . . . . . . . 14 ⊢ 0 = (0_g‘𝑈)
99	97, 98	eqtr4di 2797	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (0_g‘𝑢) = 0 )
100	99	eqeq2d 2749	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((2^nd ‘𝑥) = (0_g‘𝑢) ↔ (2^nd ‘𝑥) = 0 ))
101		simp3 1136	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁)
102	101	fveq1d 6758	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑛‘{(2^nd ‘𝑥)}) = (𝑁‘{(2^nd ‘𝑥)}))
103	102	fveqeq2d 6764	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ})))
104	96	fveq2d 6760	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (-_g‘𝑢) = (-_g‘𝑈))
105		hdmap1fval.s	. . . . . . . . . . . . . . . . . . 19 ⊢ − = (-_g‘𝑈)
106	104, 105	eqtr4di 2797	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (-_g‘𝑢) = − )
107	106	oveqd 7272	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥)) = ((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥)))
108	107	sneqd 4570	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → {((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))} = {((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})
109	101, 108	fveq12d 6763	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))}) = (𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))}))
110	109	fveqeq2d 6764	. . . . . . . . . . . . . 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 630	. . . . . . . . . . . . 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 7214	. . . . . . . . . . . 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 4482	. . . . . . . . . . 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 5161	. . . . . . . . . 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 2824	. . . . . . . . 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	syl5bb 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 1369	. . . . . . 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 3798	. . . . . 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 2877	. . . 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 2738	. . . 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 6770	. . . . . . 7 ⊢ 𝑉 ∈ V
123	44	fvexi 6770	. . . . . . 7 ⊢ 𝐷 ∈ V
124	122, 123	xpex 7581	. . . . . 6 ⊢ (𝑉 × 𝐷) ∈ V
125	124, 122	xpex 7581	. . . . 5 ⊢ ((𝑉 × 𝐷) × 𝑉) ∈ V
126	125	mptex 7081	. . . 4 ⊢ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))))) ∈ V
127	120, 121, 126	fvmpt 6857	. . 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 2799	. 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 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 {cab 2715 [wsbc 3711 ifcif 4456 {csn 4558 ↦ cmpt 5153 × cxp 5578 ‘cfv 6418 ℩crio 7211 (class class class)co 7255 1^st c1st 7802 2^nd c2nd 7803 Basecbs 16840 0_gc0g 17067 -_gcsg 18494 LSpanclspn 20148 LHypclh 37925 DVecHcdvh 39019 LCDualclcd 39527 mapdcmpd 39565 HDMap1chdma1 39732

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-hdmap1 39734

This theorem is referenced by: hdmap1vallem 39738

W3C validator