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 42821

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 42820	. . . . 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 6879	. . . 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 2808	. . 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 6877	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊))
8		fveq2 6877	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((LCDual‘𝐾)‘𝑤) = ((LCDual‘𝐾)‘𝑊))
9		fveq2 6877	. . . . . . . . . . . . 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 3794	. . . . . . . . . . 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 3794	. . . . . . . . . 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 3794	. . . . . . . 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 3794	. . . . . . 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 6890	. . . . . . 7 ⊢ ((DVecH‘𝐾)‘𝑊) ∈ V
18		fvex 6890	. . . . . . 7 ⊢ (Base‘𝑢) ∈ V
19		fvex 6890	. . . . . . 7 ⊢ (LSpan‘𝑢) ∈ V
20		hdmap1fval.u	. . . . . . . . . . 11 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
21	20	eqeq2i 2774	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 ↔ 𝑢 = ((DVecH‘𝐾)‘𝑊))
22	21	biimpri 231	. . . . . . . . 9 ⊢ (𝑢 = ((DVecH‘𝐾)‘𝑊) → 𝑢 = 𝑈)
23	22	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑢 = 𝑈)
24		simp2 1155	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = (Base‘𝑢))
25	22	fveq2d 6881	. . . . . . . . . . 11 ⊢ (𝑢 = ((DVecH‘𝐾)‘𝑊) → (Base‘𝑢) = (Base‘𝑈))
26	25	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → (Base‘𝑢) = (Base‘𝑈))
27	24, 26	eqtrd 2796	. . . . . . . . 9 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = (Base‘𝑈))
28		hdmap1fval.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑈)
29	27, 28	eqtr4di 2814	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑣 = 𝑉)
30		simp3 1156	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = (LSpan‘𝑢))
31	23	fveq2d 6881	. . . . . . . . . 10 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → (LSpan‘𝑢) = (LSpan‘𝑈))
32	30, 31	eqtrd 2796	. . . . . . . . 9 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = (LSpan‘𝑈))
33		hdmap1fval.n	. . . . . . . . 9 ⊢ 𝑁 = (LSpan‘𝑈)
34	32, 33	eqtr4di 2814	. . . . . . . 8 ⊢ ((𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢) ∧ 𝑛 = (LSpan‘𝑢)) → 𝑛 = 𝑁)
35		fvex 6890	. . . . . . . . . 10 ⊢ ((LCDual‘𝐾)‘𝑊) ∈ V
36		fvex 6890	. . . . . . . . . 10 ⊢ (Base‘𝑐) ∈ V
37		fvex 6890	. . . . . . . . . 10 ⊢ (LSpan‘𝑐) ∈ V
38		id 23	. . . . . . . . . . . . 13 ⊢ (𝑐 = ((LCDual‘𝐾)‘𝑊) → 𝑐 = ((LCDual‘𝐾)‘𝑊))
39		hdmap1fval.c	. . . . . . . . . . . . 13 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
40	38, 39	eqtr4di 2814	. . . . . . . . . . . 12 ⊢ (𝑐 = ((LCDual‘𝐾)‘𝑊) → 𝑐 = 𝐶)
41	40	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑐 = 𝐶)
42		simp2 1155	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑑 = (Base‘𝑐))
43	41	fveq2d 6881	. . . . . . . . . . . . 13 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (Base‘𝑐) = (Base‘𝐶))
44		hdmap1fval.d	. . . . . . . . . . . . 13 ⊢ 𝐷 = (Base‘𝐶)
45	43, 44	eqtr4di 2814	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (Base‘𝑐) = 𝐷)
46	42, 45	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑑 = 𝐷)
47		simp3 1156	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑗 = (LSpan‘𝑐))
48	41	fveq2d 6881	. . . . . . . . . . . . 13 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (LSpan‘𝑐) = (LSpan‘𝐶))
49		hdmap1fval.j	. . . . . . . . . . . . 13 ⊢ 𝐽 = (LSpan‘𝐶)
50	48, 49	eqtr4di 2814	. . . . . . . . . . . 12 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → (LSpan‘𝑐) = 𝐽)
51	47, 50	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝑐 = ((LCDual‘𝐾)‘𝑊) ∧ 𝑑 = (Base‘𝑐) ∧ 𝑗 = (LSpan‘𝑐)) → 𝑗 = 𝐽)
52		fvex 6890	. . . . . . . . . . . . 13 ⊢ ((mapd‘𝐾)‘𝑊) ∈ V
53		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → 𝑚 = ((mapd‘𝐾)‘𝑊))
54		hdmap1fval.m	. . . . . . . . . . . . . . 15 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
55	53, 54	eqtr4di 2814	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((mapd‘𝐾)‘𝑊) → 𝑚 = 𝑀)
56		fveq1 6876	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑀 → (𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑀‘(𝑛‘{(2^nd ‘𝑥)})))
57	56	eqeq1d 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑀 → ((𝑚‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ↔ (𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ})))
58		fveq1 6876	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑀 → (𝑚‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})) = (𝑀‘(𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))})))
59	58	eqeq1d 2763	. . . . . . . . . . . . . . . . . . 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 644	. . . . . . . . . . . . . . . . . 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 7371	. . . . . . . . . . . . . . . . 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 4503	. . . . . . . . . . . . . . . 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 5199	. . . . . . . . . . . . . . 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 2847	. . . . . . . . . . . . . 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 18	. . . . . . . . . . . . 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 3780	. . . . . . . . . . . 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 1155	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑑 = 𝐷)
68		xpeq2 5672	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝐷 → (𝑣 × 𝑑) = (𝑣 × 𝐷))
69	68	xpeq1d 5680	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝐷 → ((𝑣 × 𝑑) × 𝑣) = ((𝑣 × 𝐷) × 𝑣))
70	67, 69	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑣 × 𝑑) × 𝑣) = ((𝑣 × 𝐷) × 𝑣))
71		simp1 1154	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑐 = 𝐶)
72	71	fveq2d 6881	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (0_g‘𝑐) = (0_g‘𝐶))
73		hdmap1fval.q	. . . . . . . . . . . . . . . 16 ⊢ 𝑄 = (0_g‘𝐶)
74	72, 73	eqtr4di 2814	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (0_g‘𝑐) = 𝑄)
75		simp3 1156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽)
76	75	fveq1d 6879	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑗‘{ℎ}) = (𝐽‘{ℎ}))
77	76	eqeq2d 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝑗‘{ℎ}) ↔ (𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ})))
78	71	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (-_g‘𝑐) = (-_g‘𝐶))
79		hdmap1fval.r	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑅 = (-_g‘𝐶)
80	78, 79	eqtr4di 2814	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (-_g‘𝑐) = 𝑅)
81	80	oveqd 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → ((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ) = ((2^nd ‘(1^st ‘𝑥))𝑅ℎ))
82	81	sneqd 4596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → {((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)} = {((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})
83	75, 82	fveq12d 6884	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ∧ 𝑗 = 𝐽) → (𝑗‘{((2^nd ‘(1^st ‘𝑥))(-_g‘𝑐)ℎ)}) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))
84	83	eqeq2d 2772	. . . . . . . . . . . . . . . . 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 644	. . . . . . . . . . . . . . . 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 7372	. . . . . . . . . . . . . . 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 4504	. . . . . . . . . . . . . 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 5192	. . . . . . . . . . . . 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 2847	. . . . . . . . . . . 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 286	. . . . . . . . . . 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 1398	. . . . . . . . . 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 3816	. . . . . . . . 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 1155	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑣 = 𝑉)
94	93	xpeq1d 5680	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑣 × 𝐷) = (𝑉 × 𝐷))
95	94, 93	xpeq12d 5682	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑣 × 𝐷) × 𝑣) = ((𝑉 × 𝐷) × 𝑉))
96		simp1 1154	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑢 = 𝑈)
97	96	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (0_g‘𝑢) = (0_g‘𝑈))
98		hdmap1fval.o	. . . . . . . . . . . . . 14 ⊢ 0 = (0_g‘𝑈)
99	97, 98	eqtr4di 2814	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (0_g‘𝑢) = 0 )
100	99	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((2^nd ‘𝑥) = (0_g‘𝑢) ↔ (2^nd ‘𝑥) = 0 ))
101		simp3 1156	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁)
102	101	fveq1d 6879	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑛‘{(2^nd ‘𝑥)}) = (𝑁‘{(2^nd ‘𝑥)}))
103	102	fveqeq2d 6885	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((𝑀‘(𝑛‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ})))
104	96	fveq2d 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (-_g‘𝑢) = (-_g‘𝑈))
105		hdmap1fval.s	. . . . . . . . . . . . . . . . . . 19 ⊢ − = (-_g‘𝑈)
106	104, 105	eqtr4di 2814	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (-_g‘𝑢) = − )
107	106	oveqd 7429	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → ((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥)) = ((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥)))
108	107	sneqd 4596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → {((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))} = {((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})
109	101, 108	fveq12d 6884	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ∧ 𝑛 = 𝑁) → (𝑛‘{((1^st ‘(1^st ‘𝑥))(-_g‘𝑢)(2^nd ‘𝑥))}) = (𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))}))
110	109	fveqeq2d 6885	. . . . . . . . . . . . . 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 644	. . . . . . . . . . . . 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 7371	. . . . . . . . . . . 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 4509	. . . . . . . . . . 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 5192	. . . . . . . . . 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 2847	. . . . . . . . 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 286	. . . . . . . 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 1398	. . . . . . 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 3816	. . . . . 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 290	. . . . 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	eqabcdv 2895	. . . 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 2761	. . . 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 6891	. . . . . . 7 ⊢ 𝑉 ∈ V
123	44	fvexi 6891	. . . . . . 7 ⊢ 𝐷 ∈ V
124	122, 123	xpex 7756	. . . . . 6 ⊢ (𝑉 × 𝐷) ∈ V
125	124, 122	xpex 7756	. . . . 5 ⊢ ((𝑉 × 𝐷) × 𝑉) ∈ V
126	125	mptex 7221	. . . 4 ⊢ (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))))) ∈ V
127	120, 121, 126	fvmpt 6985	. . 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 2816	. 2 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))))))
129	1, 128	syl 18	1 ⊢ (𝜑 → 𝐼 = (𝑥 ∈ ((𝑉 × 𝐷) × 𝑉) ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)}))))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 {cab 2739 [wsbc 3739 ifcif 4482 {csn 4584 ↦ cmpt 5186 × cxp 5649 ‘cfv 6531 ℩crio 7368 (class class class)co 7412 1^st c1st 7988 2^nd c2nd 7989 Basecbs 17367 0_gc0g 17590 -_gcsg 19126 LSpanclspn 21226 LHypclh 41009 DVecHcdvh 42103 LCDualclcd 42611 mapdcmpd 42649 HDMap1chdma1 42816

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-hdmap1 42818

This theorem is used by: hdmap1vallem 42822

W3C validator