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 36104

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 36103	. . . . 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 6105	. . . 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 2656	. . 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 6103	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊))
8		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((LCDual‘𝐾)‘𝑤) = ((LCDual‘𝐾)‘𝑊))
9		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → ((mapd‘𝐾)‘𝑤) = ((mapd‘𝐾)‘𝑊))
10	9	sbceq1d 3407	. . . . . . . . . . . 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 3457	. . . . . . . . . . 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 3457	. . . . . . . . . 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 3409	. . . . . . . . 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 3457	. . . . . . . 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 3457	. . . . . . 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 3409	. . . . . 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 6113	. . . . . . 7 ⊢ ((DVecH‘𝐾)‘𝑊) ∈ V
18		fvex 6113	. . . . . . 7 ⊢ (Base‘𝑢) ∈ V
19		fvex 6113	. . . . . . 7 ⊢ (LSpan‘𝑢) ∈ V
20		hdmap1fval.u	. . . . . . . . . . 11 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
21	20	eqeq2i 2622	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 ↔ 𝑢 = ((DVecH‘𝐾)‘𝑊))
22	21	biimpri 217	. . . . . . . . 9 ⊢ (𝑢 = ((DVecH‘𝐾)‘𝑊) → 𝑢 = 𝑈)
23	22	3ad2ant1 1075	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑢 = 𝑈)
24		simp2 1055	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = (Base‘𝑢))
25	22	fveq2d 6107	. . . . . . . . . . 11 ⊢ (𝑢 = ((DVecH‘𝐾)‘𝑊) → (Base‘𝑢) = (Base‘𝑈))
26	25	3ad2ant1 1075	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → (Base‘𝑢) = (Base‘𝑈))
27	24, 26	eqtrd 2644	. . . . . . . . 9 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = (Base‘𝑈))
28		hdmap1fval.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑈)
29	27, 28	syl6eqr 2662	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = 𝑉)
30		simp3 1056	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = (LSpan‘𝑢))
31	23	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → (LSpan‘𝑢) = (LSpan‘𝑈))
32	30, 31	eqtrd 2644	. . . . . . . . 9 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = (LSpan‘𝑈))
33		hdmap1fval.n	. . . . . . . . 9 ⊢ 𝑁 = (LSpan‘𝑈)
34	32, 33	syl6eqr 2662	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = 𝑁)
35		fvex 6113	. . . . . . . . . 10 ⊢ ((LCDual‘𝐾)‘𝑊) ∈ V
36		fvex 6113	. . . . . . . . . 10 ⊢ (Base‘𝑐) ∈ V
37		fvex 6113	. . . . . . . . . 10 ⊢ (LSpan‘𝑐) ∈ V
38		id 22	. . . . . . . . . . . . 13 ⊢ (𝑐 = ((LCDual‘𝐾)‘𝑊) → 𝑐 = ((LCDual‘𝐾)‘𝑊))
39		hdmap1fval.c	. . . . . . . . . . . . 13 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
40	38, 39	syl6eqr 2662	. . . . . . . . . . . 12 ⊢ (𝑐 = ((LCDual‘𝐾)‘𝑊) → 𝑐 = 𝐶)
41	40	3ad2ant1 1075	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑐 = 𝐶)
42		simp2 1055	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑑 = (Base‘𝑐))
43	41	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (Base‘𝑐) = (Base‘𝐶))
44		hdmap1fval.d	. . . . . . . . . . . . 13 ⊢ 𝐷 = (Base‘𝐶)
45	43, 44	syl6eqr 2662	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (Base‘𝑐) = 𝐷)
46	42, 45	eqtrd 2644	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑑 = 𝐷)
47		simp3 1056	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑗 = (LSpan‘𝑐))
48	41	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (LSpan‘𝑐) = (LSpan‘𝐶))
49		hdmap1fval.j	. . . . . . . . . . . . 13 ⊢ 𝐽 = (LSpan‘𝐶)
50	48, 49	syl6eqr 2662	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (LSpan‘𝑐) = 𝐽)
51	47, 50	eqtrd 2644	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑗 = 𝐽)
52		fvex 6113	. . . . . . . . . . . . 13 ⊢ ((mapd‘𝐾)‘𝑊) ∈ V
53		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → 𝑚 = ((mapd‘𝐾)‘𝑊))
54		hdmap1fval.m	. . . . . . . . . . . . . . 15 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
55	53, 54	syl6eqr 2662	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → 𝑚 = 𝑀)
56		fveq1 6102	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑀 → (𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑀‘(𝑛‘{(2^nd ‘𝑥)})))
57	56	eqeq1d 2612	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑀 → ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ↔ (𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ})))
58		fveq1 6102	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑀 → (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑀‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})))
59	58	eqeq1d 2612	. . . . . . . . . . . . . . . . . . 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 743	. . . . . . . . . . . . . . . . . 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 6513	. . . . . . . . . . . . . . . . 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 4055	. . . . . . . . . . . . . . . 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 4673	. . . . . . . . . . . . . . 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 2673	. . . . . . . . . . . . . 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 3437	. . . . . . . . . . . 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 1055	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑑 = 𝐷)
68		xpeq2 5053	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝐷 → (𝑣 × 𝑑) = (𝑣 × 𝐷))
69	68	xpeq1d 5062	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝐷 → ((𝑣 × 𝑑) × 𝑣) = ((𝑣 × 𝐷) × 𝑣))
70	67, 69	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑣 × 𝑑) × 𝑣) = ((𝑣 × 𝐷) × 𝑣))
71		simp1 1054	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑐 = 𝐶)
72	71	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (0_g‘𝑐) = (0_g‘𝐶))
73		hdmap1fval.q	. . . . . . . . . . . . . . . 16 ⊢ 𝑄 = (0_g‘𝐶)
74	72, 73	syl6eqr 2662	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (0_g‘𝑐) = 𝑄)
75		simp3 1056	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽)
76	75	fveq1d 6105	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑗‘{ℎ}) = (𝐽‘{ℎ}))
77	76	eqeq2d 2620	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ↔ (𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ})))
78	71	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (-_g‘𝑐) = (-_g‘𝐶))
79		hdmap1fval.r	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑅 = (-_g‘𝐶)
80	78, 79	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (-_g‘𝑐) = 𝑅)
81	80	oveqd 6566	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ) = ((2^nd ‘(1^st ‘𝑥))𝑅ℎ))
82	81	sneqd 4137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → {((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)} = {((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})
83	75, 82	fveq12d 6109	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)}) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))
84	83	eqeq2d 2620	. . . . . . . . . . . . . . . . 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 743	. . . . . . . . . . . . . . . 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 6514	. . . . . . . . . . . . . . 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 4056	. . . . . . . . . . . . . 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 4663	. . . . . . . . . . . . 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 2673	. . . . . . . . . . . 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 271	. . . . . . . . . . 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 1318	. . . . . . . . . 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 3474	. . . . . . . . 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 1055	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑣 = 𝑉)
94	93	xpeq1d 5062	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑣 × 𝐷) = (𝑉 × 𝐷))
95	94, 93	xpeq12d 5064	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑣 × 𝐷) × 𝑣) = ((𝑉 × 𝐷) × 𝑉))
96		simp1 1054	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑢 = 𝑈)
97	96	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (0_g‘𝑢) = (0_g‘𝑈))
98		hdmap1fval.o	. . . . . . . . . . . . . 14 ⊢ 0 = (0_g‘𝑈)
99	97, 98	syl6eqr 2662	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (0_g‘𝑢) = 0 )
100	99	eqeq2d 2620	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((2^nd ‘𝑥) = (0_g‘𝑢) ↔ (2^nd ‘𝑥) = 0 ))
101		simp3 1056	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁)
102	101	fveq1d 6105	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑛‘{(2^nd ‘𝑥)}) = (𝑁‘{(2^nd ‘𝑥)}))
103	102	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑀‘(𝑁‘{(2^nd ‘𝑥)})))
104	103	eqeq1d 2612	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ})))
105	96	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (-_g‘𝑢) = (-_g‘𝑈))
106		hdmap1fval.s	. . . . . . . . . . . . . . . . . . . 20 ⊢ − = (-_g‘𝑈)
107	105, 106	syl6eqr 2662	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (-_g‘𝑢) = − )
108	107	oveqd 6566	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥)) = ((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥)))
109	108	sneqd 4137	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → {((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))} = {((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})
110	101, 109	fveq12d 6109	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))}) = (𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))}))
111	110	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑀‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})))
112	111	eqeq1d 2612	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑀‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})))
113	104, 112	anbi12d 743	. . . . . . . . . . . . 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 ‘𝑥))𝑅ℎ)}))))
114	113	riotabidv 6513	. . . . . . . . . . . 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 ‘𝑥))𝑅ℎ)}))))
115	100, 114	ifbieq2d 4061	. . . . . . . . . . 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 ‘𝑥))𝑅ℎ)})))))
116	95, 115	mpteq12dv 4663	. . . . . . . . . 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 ‘𝑥))𝑅ℎ)}))))))
117	116	eleq2d 2673	. . . . . . . . 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 ‘𝑥))𝑅ℎ)})))))))
118	92, 117	syl5bb 271	. . . . . . . 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 ‘𝑥))𝑅ℎ)})))))))
119	23, 29, 34, 118	syl3anc 1318	. . . . . . 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 ‘𝑥))𝑅ℎ)})))))))
120	17, 18, 19, 119	sbc3ie 3474	. . . . . 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 ‘𝑥))𝑅ℎ)}))))))
121	16, 120	syl6bb 275	. . . . 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 ‘𝑥))𝑅ℎ)})))))))
122	121	abbi1dv 2730	. . . 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 ‘𝑥))𝑅ℎ)}))))))
123		eqid 2610	. . . 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‘𝑐)ℎ)})))))})
124		fvex 6113	. . . . . . . 8 ⊢ (Base‘𝑈) ∈ V
125	28, 124	eqeltri 2684	. . . . . . 7 ⊢ 𝑉 ∈ V
126		fvex 6113	. . . . . . . 8 ⊢ (Base‘𝐶) ∈ V
127	44, 126	eqeltri 2684	. . . . . . 7 ⊢ 𝐷 ∈ V
128	125, 127	xpex 6860	. . . . . 6 ⊢ (𝑉 × 𝐷) ∈ V
129	128, 125	xpex 6860	. . . . 5 ⊢ ((𝑉 × 𝐷) × 𝑉) ∈ V
130	129	mptex 6390	. . . 4 ⊢ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))))) ∈ V
131	122, 123, 130	fvmpt 6191	. . 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 ‘𝑥))𝑅ℎ)}))))))
132	6, 131	sylan9eq 2664	. 2 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))))))
133	1, 132	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 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 {cab 2596 Vcvv 3173 [wsbc 3402 ifcif 4036 {csn 4125 ↦ cmpt 4643 × cxp 5036 ‘cfv 5804 ℩crio 6510 (class class class)co 6549 1^st c1st 7057 2^nd c2nd 7058 Basecbs 15695 0_gc0g 15923 -_gcsg 17247 LSpanclspn 18792 LHypclh 34288 DVecHcdvh 35385 LCDualclcd 35893 mapdcmpd 35931 HDMap1chdma1 36099

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-hdmap1 36101

This theorem is referenced by: hdmap1vallem 36105

W3C validator