# Metamath Proof Explorer

## Theorem hdmap1fval

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

Ref Expression
Hypotheses hdmap1val.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmap1fval.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmap1fval.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmap1fval.s
hdmap1fval.o
hdmap1fval.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
hdmap1fval.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmap1fval.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmap1fval.r ${⊢}{R}={-}_{{C}}$
hdmap1fval.q ${⊢}{Q}={0}_{{C}}$
hdmap1fval.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
hdmap1fval.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
hdmap1fval.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
hdmap1fval.k ${⊢}{\phi }\to \left({K}\in {A}\wedge {W}\in {H}\right)$
Assertion hdmap1fval

### Proof

Step Hyp Ref Expression
1 hdmap1val.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmap1fval.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hdmap1fval.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hdmap1fval.s
5 hdmap1fval.o
6 hdmap1fval.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
7 hdmap1fval.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
8 hdmap1fval.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
9 hdmap1fval.r ${⊢}{R}={-}_{{C}}$
10 hdmap1fval.q ${⊢}{Q}={0}_{{C}}$
11 hdmap1fval.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
12 hdmap1fval.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
13 hdmap1fval.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
14 hdmap1fval.k ${⊢}{\phi }\to \left({K}\in {A}\wedge {W}\in {H}\right)$
15 1 hdmap1ffval
16 15 fveq1d
17 13 16 syl5eq
18 fveq2 ${⊢}{w}={W}\to \mathrm{DVecH}\left({K}\right)\left({w}\right)=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
19 fveq2 ${⊢}{w}={W}\to \mathrm{LCDual}\left({K}\right)\left({w}\right)=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
20 fveq2 ${⊢}{w}={W}\to \mathrm{mapd}\left({K}\right)\left({w}\right)=\mathrm{mapd}\left({K}\right)\left({W}\right)$
21 20 sbceq1d
22 21 sbcbidv
23 22 sbcbidv
24 19 23 sbceqbid
25 24 sbcbidv
26 25 sbcbidv
27 18 26 sbceqbid
28 fvex ${⊢}\mathrm{DVecH}\left({K}\right)\left({W}\right)\in \mathrm{V}$
29 fvex ${⊢}{\mathrm{Base}}_{{u}}\in \mathrm{V}$
30 fvex ${⊢}\mathrm{LSpan}\left({u}\right)\in \mathrm{V}$
31 2 eqeq2i ${⊢}{u}={U}↔{u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
32 31 biimpri ${⊢}{u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\to {u}={U}$
33 32 3ad2ant1 ${⊢}\left({u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\wedge {n}=\mathrm{LSpan}\left({u}\right)\right)\to {u}={U}$
34 simp2 ${⊢}\left({u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\wedge {n}=\mathrm{LSpan}\left({u}\right)\right)\to {v}={\mathrm{Base}}_{{u}}$
35 32 fveq2d ${⊢}{u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\to {\mathrm{Base}}_{{u}}={\mathrm{Base}}_{{U}}$
36 35 3ad2ant1 ${⊢}\left({u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\wedge {n}=\mathrm{LSpan}\left({u}\right)\right)\to {\mathrm{Base}}_{{u}}={\mathrm{Base}}_{{U}}$
37 34 36 eqtrd ${⊢}\left({u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\wedge {n}=\mathrm{LSpan}\left({u}\right)\right)\to {v}={\mathrm{Base}}_{{U}}$
38 37 3 syl6eqr ${⊢}\left({u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\wedge {n}=\mathrm{LSpan}\left({u}\right)\right)\to {v}={V}$
39 simp3 ${⊢}\left({u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\wedge {n}=\mathrm{LSpan}\left({u}\right)\right)\to {n}=\mathrm{LSpan}\left({u}\right)$
40 33 fveq2d ${⊢}\left({u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\wedge {n}=\mathrm{LSpan}\left({u}\right)\right)\to \mathrm{LSpan}\left({u}\right)=\mathrm{LSpan}\left({U}\right)$
41 39 40 eqtrd ${⊢}\left({u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\wedge {n}=\mathrm{LSpan}\left({u}\right)\right)\to {n}=\mathrm{LSpan}\left({U}\right)$
42 41 6 syl6eqr ${⊢}\left({u}=\mathrm{DVecH}\left({K}\right)\left({W}\right)\wedge {v}={\mathrm{Base}}_{{u}}\wedge {n}=\mathrm{LSpan}\left({u}\right)\right)\to {n}={N}$
43 fvex ${⊢}\mathrm{LCDual}\left({K}\right)\left({W}\right)\in \mathrm{V}$
44 fvex ${⊢}{\mathrm{Base}}_{{c}}\in \mathrm{V}$
45 fvex ${⊢}\mathrm{LSpan}\left({c}\right)\in \mathrm{V}$
46 id ${⊢}{c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\to {c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
47 46 7 syl6eqr ${⊢}{c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\to {c}={C}$
48 47 3ad2ant1 ${⊢}\left({c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\wedge {d}={\mathrm{Base}}_{{c}}\wedge {j}=\mathrm{LSpan}\left({c}\right)\right)\to {c}={C}$
49 simp2 ${⊢}\left({c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\wedge {d}={\mathrm{Base}}_{{c}}\wedge {j}=\mathrm{LSpan}\left({c}\right)\right)\to {d}={\mathrm{Base}}_{{c}}$
50 48 fveq2d ${⊢}\left({c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\wedge {d}={\mathrm{Base}}_{{c}}\wedge {j}=\mathrm{LSpan}\left({c}\right)\right)\to {\mathrm{Base}}_{{c}}={\mathrm{Base}}_{{C}}$
51 50 8 syl6eqr ${⊢}\left({c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\wedge {d}={\mathrm{Base}}_{{c}}\wedge {j}=\mathrm{LSpan}\left({c}\right)\right)\to {\mathrm{Base}}_{{c}}={D}$
52 49 51 eqtrd ${⊢}\left({c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\wedge {d}={\mathrm{Base}}_{{c}}\wedge {j}=\mathrm{LSpan}\left({c}\right)\right)\to {d}={D}$
53 simp3 ${⊢}\left({c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\wedge {d}={\mathrm{Base}}_{{c}}\wedge {j}=\mathrm{LSpan}\left({c}\right)\right)\to {j}=\mathrm{LSpan}\left({c}\right)$
54 48 fveq2d ${⊢}\left({c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\wedge {d}={\mathrm{Base}}_{{c}}\wedge {j}=\mathrm{LSpan}\left({c}\right)\right)\to \mathrm{LSpan}\left({c}\right)=\mathrm{LSpan}\left({C}\right)$
55 54 11 syl6eqr ${⊢}\left({c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\wedge {d}={\mathrm{Base}}_{{c}}\wedge {j}=\mathrm{LSpan}\left({c}\right)\right)\to \mathrm{LSpan}\left({c}\right)={J}$
56 53 55 eqtrd ${⊢}\left({c}=\mathrm{LCDual}\left({K}\right)\left({W}\right)\wedge {d}={\mathrm{Base}}_{{c}}\wedge {j}=\mathrm{LSpan}\left({c}\right)\right)\to {j}={J}$
57 fvex ${⊢}\mathrm{mapd}\left({K}\right)\left({W}\right)\in \mathrm{V}$
58 id ${⊢}{m}=\mathrm{mapd}\left({K}\right)\left({W}\right)\to {m}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
59 58 12 syl6eqr ${⊢}{m}=\mathrm{mapd}\left({K}\right)\left({W}\right)\to {m}={M}$
60 fveq1 ${⊢}{m}={M}\to {m}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)$
61 60 eqeq1d ${⊢}{m}={M}\to \left({m}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)↔{M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\right)$
62 fveq1 ${⊢}{m}={M}\to {m}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)$
63 62 eqeq1d ${⊢}{m}={M}\to \left({m}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)↔{M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)$
64 61 63 anbi12d ${⊢}{m}={M}\to \left(\left({m}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {m}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)↔\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)$
65 64 riotabidv ${⊢}{m}={M}\to \left(\iota {h}\in {d}|\left({m}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {m}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)=\left(\iota {h}\in {d}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)$
66 65 ifeq2d ${⊢}{m}={M}\to if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({m}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {m}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)=if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)$
67 66 mpteq2dv ${⊢}{m}={M}\to \left({x}\in \left(\left({v}×{d}\right)×{v}\right)⟼if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({m}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {m}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)\right)=\left({x}\in \left(\left({v}×{d}\right)×{v}\right)⟼if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)\right)$
68 67 eleq2d ${⊢}{m}={M}\to \left({a}\in \left({x}\in \left(\left({v}×{d}\right)×{v}\right)⟼if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({m}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {m}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)\right)↔{a}\in \left({x}\in \left(\left({v}×{d}\right)×{v}\right)⟼if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)\right)\right)$
69 59 68 syl ${⊢}{m}=\mathrm{mapd}\left({K}\right)\left({W}\right)\to \left({a}\in \left({x}\in \left(\left({v}×{d}\right)×{v}\right)⟼if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({m}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {m}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)\right)↔{a}\in \left({x}\in \left(\left({v}×{d}\right)×{v}\right)⟼if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)\right)\right)$
70 57 69 sbcie
71 simp2 ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to {d}={D}$
72 xpeq2 ${⊢}{d}={D}\to {v}×{d}={v}×{D}$
73 72 xpeq1d ${⊢}{d}={D}\to \left({v}×{d}\right)×{v}=\left({v}×{D}\right)×{v}$
74 71 73 syl ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to \left({v}×{d}\right)×{v}=\left({v}×{D}\right)×{v}$
75 simp1 ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to {c}={C}$
76 75 fveq2d ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to {0}_{{c}}={0}_{{C}}$
77 76 10 syl6eqr ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to {0}_{{c}}={Q}$
78 simp3 ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to {j}={J}$
79 78 fveq1d ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to {j}\left(\left\{{h}\right\}\right)={J}\left(\left\{{h}\right\}\right)$
80 79 eqeq2d ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to \left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)↔{M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\right)$
81 75 fveq2d ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to {-}_{{c}}={-}_{{C}}$
82 81 9 syl6eqr ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to {-}_{{c}}={R}$
83 82 oveqd ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to {2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}={2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}$
84 83 sneqd ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to \left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}=\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}$
85 78 84 fveq12d ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to {j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)={J}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}\right)$
86 85 eqeq2d ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to \left({M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)↔{M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}\right)\right)$
87 80 86 anbi12d ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to \left(\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)↔\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}\right)\right)\right)$
88 71 87 riotaeqbidv ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to \left(\iota {h}\in {d}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)=\left(\iota {h}\in {D}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}\right)\right)\right)$
89 77 88 ifeq12d ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)=if\left({2}^{nd}\left({x}\right)={0}_{{u}},{Q},\left(\iota {h}\in {D}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}\right)\right)\right)\right)$
90 74 89 mpteq12dv ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to \left({x}\in \left(\left({v}×{d}\right)×{v}\right)⟼if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)\right)=\left({x}\in \left(\left({v}×{D}\right)×{v}\right)⟼if\left({2}^{nd}\left({x}\right)={0}_{{u}},{Q},\left(\iota {h}\in {D}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}\right)\right)\right)\right)\right)$
91 90 eleq2d ${⊢}\left({c}={C}\wedge {d}={D}\wedge {j}={J}\right)\to \left({a}\in \left({x}\in \left(\left({v}×{d}\right)×{v}\right)⟼if\left({2}^{nd}\left({x}\right)={0}_{{u}},{0}_{{c}},\left(\iota {h}\in {d}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={j}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){-}_{{c}}{h}\right\}\right)\right)\right)\right)\right)↔{a}\in \left({x}\in \left(\left({v}×{D}\right)×{v}\right)⟼if\left({2}^{nd}\left({x}\right)={0}_{{u}},{Q},\left(\iota {h}\in {D}|\left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\wedge {M}\left({n}\left(\left\{{1}^{st}\left({1}^{st}\left({x}\right)\right){-}_{{u}}{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}\right)\right)\right)\right)\right)\right)$
92 70 91 syl5bb
93 48 52 56 92 syl3anc
94 43 44 45 93 sbc3ie
95 simp2 ${⊢}\left({u}={U}\wedge {v}={V}\wedge {n}={N}\right)\to {v}={V}$
96 95 xpeq1d ${⊢}\left({u}={U}\wedge {v}={V}\wedge {n}={N}\right)\to {v}×{D}={V}×{D}$
97 96 95 xpeq12d ${⊢}\left({u}={U}\wedge {v}={V}\wedge {n}={N}\right)\to \left({v}×{D}\right)×{v}=\left({V}×{D}\right)×{V}$
98 simp1 ${⊢}\left({u}={U}\wedge {v}={V}\wedge {n}={N}\right)\to {u}={U}$
99 98 fveq2d ${⊢}\left({u}={U}\wedge {v}={V}\wedge {n}={N}\right)\to {0}_{{u}}={0}_{{U}}$
100 99 5 syl6eqr
101 100 eqeq2d
102 simp3 ${⊢}\left({u}={U}\wedge {v}={V}\wedge {n}={N}\right)\to {n}={N}$
103 102 fveq1d ${⊢}\left({u}={U}\wedge {v}={V}\wedge {n}={N}\right)\to {n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)={N}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)$
104 103 fveqeq2d ${⊢}\left({u}={U}\wedge {v}={V}\wedge {n}={N}\right)\to \left({M}\left({n}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)↔{M}\left({N}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\right)$
105 98 fveq2d ${⊢}\left({u}={U}\wedge {v}={V}\wedge {n}={N}\right)\to {-}_{{u}}={-}_{{U}}$
106 105 4 syl6eqr
107 106 oveqd
108 107 sneqd
109 102 108 fveq12d
110 109 fveqeq2d
111 104 110 anbi12d
112 111 riotabidv
113 101 112 ifbieq2d
114 97 113 mpteq12dv
115 114 eleq2d
116 94 115 syl5bb
117 33 38 42 116 syl3anc
118 28 29 30 117 sbc3ie
119 27 118 syl6bb
120 119 abbi1dv
121 eqid
122 3 fvexi ${⊢}{V}\in \mathrm{V}$
123 8 fvexi ${⊢}{D}\in \mathrm{V}$
124 122 123 xpex ${⊢}{V}×{D}\in \mathrm{V}$
125 124 122 xpex ${⊢}\left({V}×{D}\right)×{V}\in \mathrm{V}$
126 125 mptex
127 120 121 126 fvmpt
128 17 127 sylan9eq
129 14 128 syl