hdmapfval - Mathbox for Norm Megill

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

Theorem hdmapfval 38957

Description: Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)

**Hypotheses**
Ref	Expression
hdmapval.h	⊢ 𝐻 = (LHyp‘𝐾)
hdmapfval.e	⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
hdmapfval.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
hdmapfval.v	⊢ 𝑉 = (Base‘𝑈)
hdmapfval.n	⊢ 𝑁 = (LSpan‘𝑈)
hdmapfval.c	⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
hdmapfval.d	⊢ 𝐷 = (Base‘𝐶)
hdmapfval.j	⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)
hdmapfval.i	⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)
hdmapfval.s	⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
hdmapfval.k	⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))

**Assertion**
Ref	Expression
hdmapfval	⊢ (𝜑 → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))

Distinct variable groups: 𝑦,𝑡,𝑧,𝐾 𝑦,𝐷 𝑡,𝐸,𝑦,𝑧 𝑡,𝐼,𝑦,𝑧 𝑡,𝑈,𝑦,𝑧 𝑡,𝑉,𝑦,𝑧 𝑡,𝑊,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑦,𝑧,𝑡) 𝐴(𝑦,𝑧,𝑡) 𝐶(𝑦,𝑧,𝑡) 𝐷(𝑧,𝑡) 𝑆(𝑦,𝑧,𝑡) 𝐻(𝑦,𝑧,𝑡) 𝐽(𝑦,𝑧,𝑡) 𝑁(𝑦,𝑧,𝑡)

Proof of Theorem hdmapfval Dummy variables 𝑤 𝑒 𝑎 𝑖 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hdmapfval.k	. 2 ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))
2		hdmapfval.s	. . . 4 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
3		hdmapval.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
4	3	hdmapffval 38956	. . . . 5 ⊢ (𝐾 ∈ 𝐴 → (HDMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
5	4	fveq1d 6667	. . . 4 ⊢ (𝐾 ∈ 𝐴 → ((HDMap‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊))
6	2, 5	syl5eq 2868	. . 3 ⊢ (𝐾 ∈ 𝐴 → 𝑆 = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊))
7		fveq2 6665	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊))
8	7	reseq2d 5848	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ( I ↾ ((LTrn‘𝐾)‘𝑤)) = ( I ↾ ((LTrn‘𝐾)‘𝑊)))
9	8	opeq2d 4804	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩)
10		fveq2 6665	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊))
11		fveq2 6665	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((HDMap1‘𝐾)‘𝑤) = ((HDMap1‘𝐾)‘𝑊))
12		2fveq3 6670	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → (Base‘((LCDual‘𝐾)‘𝑤)) = (Base‘((LCDual‘𝐾)‘𝑊)))
13		fveq2 6665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑊 → ((HVMap‘𝐾)‘𝑤) = ((HVMap‘𝐾)‘𝑊))
14	13	fveq1d 6667	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑊 → (((HVMap‘𝐾)‘𝑤)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝑒))
15	14	oteq2d 4810	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑊 → ⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩ = ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩)
16	15	fveq2d 6669	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑊 → (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩) = (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩))
17	16	oteq2d 4810	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑊 → ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)
18	17	fveq2d 6669	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑊 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
19	18	eqeq2d 2832	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑊 → (𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))
20	19	imbi2d 343	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑊 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
21	20	ralbidv 3197	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
22	12, 21	riotaeqbidv 7111	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))) = (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
23	22	mpteq2dv 5155	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
24	23	eleq2d 2898	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
25	11, 24	sbceqbid 3779	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ([((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
26	25	sbcbidv 3827	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ([(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
27	10, 26	sbceqbid 3779	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ([((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
28	9, 27	sbceqbid 3779	. . . . . 6 ⊢ (𝑤 = 𝑊 → ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ / 𝑒][((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
29		opex 5349	. . . . . . 7 ⊢ ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∈ V
30		fvex 6678	. . . . . . 7 ⊢ ((DVecH‘𝐾)‘𝑊) ∈ V
31		fvex 6678	. . . . . . 7 ⊢ (Base‘𝑢) ∈ V
32		simp1 1132	. . . . . . . . 9 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩)
33		hdmapfval.e	. . . . . . . . 9 ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
34	32, 33	syl6eqr 2874	. . . . . . . 8 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = 𝐸)
35		simp2 1133	. . . . . . . . 9 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = ((DVecH‘𝐾)‘𝑊))
36		hdmapfval.u	. . . . . . . . 9 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
37	35, 36	syl6eqr 2874	. . . . . . . 8 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = 𝑈)
38		simp3 1134	. . . . . . . . . 10 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑢))
39	37	fveq2d 6669	. . . . . . . . . 10 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → (Base‘𝑢) = (Base‘𝑈))
40	38, 39	eqtrd 2856	. . . . . . . . 9 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑈))
41		hdmapfval.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑈)
42	40, 41	syl6eqr 2874	. . . . . . . 8 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = 𝑉)
43		fvex 6678	. . . . . . . . . 10 ⊢ ((HDMap1‘𝐾)‘𝑊) ∈ V
44		id 22	. . . . . . . . . . . 12 ⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = ((HDMap1‘𝐾)‘𝑊))
45		hdmapfval.i	. . . . . . . . . . . 12 ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)
46	44, 45	syl6eqr 2874	. . . . . . . . . . 11 ⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = 𝐼)
47		fveq1 6664	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝐼 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
48		fveq1 6664	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝐼 → (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩) = (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩))
49	48	oteq2d 4810	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝐼 → ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)
50	49	fveq2d 6669	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝐼 → (𝐼‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
51	47, 50	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝐼 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
52	51	eqeq2d 2832	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝐼 → (𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))
53	52	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝐼 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
54	53	ralbidv 3197	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝐼 → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
55	54	riotabidv 7110	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝐼 → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))) = (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
56	55	mpteq2dv 5155	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝐼 → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
57	56	eleq2d 2898	. . . . . . . . . . 11 ⊢ (𝑖 = 𝐼 → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
58	46, 57	syl 17	. . . . . . . . . 10 ⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
59	43, 58	sbcie 3812	. . . . . . . . 9 ⊢ ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
60		simp3 1134	. . . . . . . . . . 11 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑣 = 𝑉)
61		hdmapfval.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (Base‘𝐶)
62		hdmapfval.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
63	62	fveq2i 6668	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐶) = (Base‘((LCDual‘𝐾)‘𝑊))
64	61, 63	eqtr2i 2845	. . . . . . . . . . . . 13 ⊢ (Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷
65	64	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷)
66		simp2 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑢 = 𝑈)
67	66	fveq2d 6669	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (LSpan‘𝑢) = (LSpan‘𝑈))
68		hdmapfval.n	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑁 = (LSpan‘𝑈)
69	67, 68	syl6eqr 2874	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (LSpan‘𝑢) = 𝑁)
70		simp1 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑒 = 𝐸)
71	70	sneqd 4573	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → {𝑒} = {𝐸})
72	69, 71	fveq12d 6672	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑒}) = (𝑁‘{𝐸}))
73	69	fveq1d 6667	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑡}) = (𝑁‘{𝑡}))
74	72, 73	uneq12d 4140	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) = ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})))
75	74	eleq2d 2898	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡}))))
76	75	notbid 320	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡}))))
77	70	oteq1d 4809	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩)
78	70	fveq2d 6669	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝐸))
79		hdmapfval.j	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)
80	79	fveq1i 6666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽‘𝐸) = (((HVMap‘𝐾)‘𝑊)‘𝐸)
81	78, 80	syl6eqr 2874	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (𝐽‘𝐸))
82	81	oteq2d 4810	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ⟨𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (𝐽‘𝐸), 𝑧⟩)
83	77, 82	eqtrd 2856	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (𝐽‘𝐸), 𝑧⟩)
84	83	fveq2d 6669	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩) = (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))
85	84	oteq2d 4810	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)
86	85	fveq2d 6669	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))
87	86	eqeq2d 2832	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))
88	76, 87	imbi12d 347	. . . . . . . . . . . . 13 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))
89	60, 88	raleqbidv 3402	. . . . . . . . . . . 12 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))
90	65, 89	riotaeqbidv 7111	. . . . . . . . . . 11 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))) = (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))
91	60, 90	mpteq12dv 5144	. . . . . . . . . 10 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
92	91	eleq2d 2898	. . . . . . . . 9 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))))
93	59, 92	syl5bb 285	. . . . . . . 8 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))))
94	34, 37, 42, 93	syl3anc 1367	. . . . . . 7 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))))
95	29, 30, 31, 94	sbc3ie 3852	. . . . . 6 ⊢ ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ / 𝑒][((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
96	28, 95	syl6bb 289	. . . . 5 ⊢ (𝑤 = 𝑊 → ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))))
97	96	abbi1dv 2952	. . . 4 ⊢ (𝑤 = 𝑊 → {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))} = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
98		eqid 2821	. . . 4 ⊢ (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})
99	97, 98, 41	mptfvmpt 6984	. . 3 ⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊) = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
100	6, 99	sylan9eq 2876	. 2 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
101	1, 100	syl 17	1 ⊢ (𝜑 → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 {cab 2799 ∀wral 3138 [wsbc 3772 ∪ cun 3934 {csn 4561 ⟨cop 4567 ⟨cotp 4569 ↦ cmpt 5139 I cid 5454 ↾ cres 5552 ‘cfv 6350 ℩crio 7107 Basecbs 16477 LSpanclspn 19737 LHypclh 37114 LTrncltrn 37231 DVecHcdvh 38208 LCDualclcd 38716 HVMapchvm 38886 HDMap1chdma1 38921 HDMapchdma 38922

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pr 5322

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-ot 4570 df-uni 4833 df-iun 4914 df-br 5060 df-opab 5122 df-mpt 5140 df-id 5455 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-riota 7108 df-hdmap 38924

This theorem is referenced by: hdmapval 38958 hdmapfnN 38959

W3C validator