# Metamath Proof Explorer

## Theorem dih1dimatlem

Description: Lemma for dih1dimat . (Contributed by NM, 10-Apr-2014)

Ref Expression
Hypotheses dih1dimat.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dih1dimat.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dih1dimat.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dih1dimat.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
dih1dimat.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dih1dimat.l
dih1dimat.c ${⊢}{C}=\mathrm{Atoms}\left({K}\right)$
dih1dimat.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
dih1dimat.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dih1dimat.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
dih1dimat.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
dih1dimat.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
dih1dimat.d ${⊢}{F}=\mathrm{Scalar}\left({U}\right)$
dih1dimat.j ${⊢}{J}={inv}_{r}\left({F}\right)$
dih1dimat.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dih1dimat.m
dih1dimat.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
dih1dimat.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
dih1dimat.z
dih1dimat.g ${⊢}{G}=\left(\iota {h}\in {T}|{h}\left({P}\right)={J}\left({s}\right)\left({f}\right)\left({P}\right)\right)$
Assertion dih1dimatlem ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {D}\in {A}\right)\to {D}\in \mathrm{ran}{I}$

### Proof

Step Hyp Ref Expression
1 dih1dimat.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dih1dimat.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dih1dimat.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
4 dih1dimat.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
5 dih1dimat.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
6 dih1dimat.l
7 dih1dimat.c ${⊢}{C}=\mathrm{Atoms}\left({K}\right)$
8 dih1dimat.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
9 dih1dimat.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
10 dih1dimat.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
11 dih1dimat.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
12 dih1dimat.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
13 dih1dimat.d ${⊢}{F}=\mathrm{Scalar}\left({U}\right)$
14 dih1dimat.j ${⊢}{J}={inv}_{r}\left({F}\right)$
15 dih1dimat.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
16 dih1dimat.m
17 dih1dimat.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
18 dih1dimat.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
19 dih1dimat.z
20 dih1dimat.g ${⊢}{G}=\left(\iota {h}\in {T}|{h}\left({P}\right)={J}\left({s}\right)\left({f}\right)\left({P}\right)\right)$
21 id ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
22 1 2 21 dvhlvec ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {U}\in \mathrm{LVec}$
23 15 18 19 4 islsat
24 22 23 syl
25 24 biimpa
26 eldifi
27 1 9 11 2 15 dvhvbase ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {V}={T}×{E}$
28 27 eleq2d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({v}\in {V}↔{v}\in \left({T}×{E}\right)\right)$
29 26 28 syl5ib
30 29 imp
31 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}={O}\right)\to {s}={O}$
32 31 opeq2d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}={O}\right)\to ⟨{f},{s}⟩=⟨{f},{O}⟩$
33 32 sneqd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}={O}\right)\to \left\{⟨{f},{s}⟩\right\}=\left\{⟨{f},{O}⟩\right\}$
34 33 fveq2d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}={O}\right)\to {N}\left(\left\{⟨{f},{s}⟩\right\}\right)={N}\left(\left\{⟨{f},{O}⟩\right\}\right)$
35 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
36 5 1 9 10 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to {R}\left({f}\right)\in {B}$
37 6 1 9 10 trlle
38 eqid ${⊢}\mathrm{DIsoB}\left({K}\right)\left({W}\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
39 5 6 1 3 38 dihvalb
40 35 36 37 39 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to {I}\left({R}\left({f}\right)\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({R}\left({f}\right)\right)$
41 5 1 9 10 12 2 38 18 dib1dim2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to \mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({R}\left({f}\right)\right)={N}\left(\left\{⟨{f},{O}⟩\right\}\right)$
42 40 41 eqtr2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to {N}\left(\left\{⟨{f},{O}⟩\right\}\right)={I}\left({R}\left({f}\right)\right)$
43 5 1 3 2 17 dihf11 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:{B}\underset{1-1}{⟶}{S}$
44 43 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to {I}:{B}\underset{1-1}{⟶}{S}$
45 f1fn ${⊢}{I}:{B}\underset{1-1}{⟶}{S}\to {I}Fn{B}$
46 44 45 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to {I}Fn{B}$
47 fnfvelrn ${⊢}\left({I}Fn{B}\wedge {R}\left({f}\right)\in {B}\right)\to {I}\left({R}\left({f}\right)\right)\in \mathrm{ran}{I}$
48 46 36 47 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to {I}\left({R}\left({f}\right)\right)\in \mathrm{ran}{I}$
49 42 48 eqeltrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in {T}\right)\to {N}\left(\left\{⟨{f},{O}⟩\right\}\right)\in \mathrm{ran}{I}$
50 49 adantrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\to {N}\left(\left\{⟨{f},{O}⟩\right\}\right)\in \mathrm{ran}{I}$
51 50 adantr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}={O}\right)\to {N}\left(\left\{⟨{f},{O}⟩\right\}\right)\in \mathrm{ran}{I}$
52 34 51 eqeltrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}={O}\right)\to {N}\left(\left\{⟨{f},{s}⟩\right\}\right)\in \mathrm{ran}{I}$
53 simpll ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
54 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
55 1 11 2 13 54 dvhbase ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{Base}}_{{F}}={E}$
56 53 55 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {\mathrm{Base}}_{{F}}={E}$
57 56 rexeqdv
58 simplll ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\wedge {t}\in {E}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
59 simpr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\wedge {t}\in {E}\right)\to {t}\in {E}$
60 opelxpi ${⊢}\left({f}\in {T}\wedge {s}\in {E}\right)\to ⟨{f},{s}⟩\in \left({T}×{E}\right)$
61 60 ad3antlr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\wedge {t}\in {E}\right)\to ⟨{f},{s}⟩\in \left({T}×{E}\right)$
62 1 9 11 2 16 dvhvscacl
63 58 59 61 62 syl12anc
64 eleq1a
65 63 64 syl
66 65 rexlimdva
67 66 pm4.71rd
68 simplrl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {f}\in {T}$
69 68 adantr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\wedge {t}\in {E}\right)\to {f}\in {T}$
70 simplrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {s}\in {E}$
71 70 adantr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\wedge {t}\in {E}\right)\to {s}\in {E}$
72 1 9 11 2 16 dvhopvsca
73 58 59 69 71 72 syl13anc
74 73 eqeq2d
75 74 rexbidva
76 75 anbi2d
77 57 67 76 3bitrd
78 77 abbidv
79 df-rab ${⊢}\left\{{u}\in \left({T}×{E}\right)|\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩\right\}=\left\{{u}|\left({u}\in \left({T}×{E}\right)\wedge \exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩\right)\right\}$
80 78 79 syl6eqr
81 ssrab2 ${⊢}\left\{{u}\in \left({T}×{E}\right)|\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩\right\}\subseteq {T}×{E}$
82 relxp ${⊢}\mathrm{Rel}\left({T}×{E}\right)$
83 relss ${⊢}\left\{{u}\in \left({T}×{E}\right)|\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩\right\}\subseteq {T}×{E}\to \left(\mathrm{Rel}\left({T}×{E}\right)\to \mathrm{Rel}\left\{{u}\in \left({T}×{E}\right)|\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩\right\}\right)$
84 81 82 83 mp2 ${⊢}\mathrm{Rel}\left\{{u}\in \left({T}×{E}\right)|\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩\right\}$
85 relopab ${⊢}\mathrm{Rel}\left\{⟨{g},{r}⟩|\left({g}={r}\left({G}\right)\wedge {r}\in {E}\right)\right\}$
86 vex ${⊢}{i}\in \mathrm{V}$
87 vex ${⊢}{p}\in \mathrm{V}$
88 eqeq1 ${⊢}{g}={i}\to \left({g}={r}\left({G}\right)↔{i}={r}\left({G}\right)\right)$
89 88 anbi1d ${⊢}{g}={i}\to \left(\left({g}={r}\left({G}\right)\wedge {r}\in {E}\right)↔\left({i}={r}\left({G}\right)\wedge {r}\in {E}\right)\right)$
90 fveq1 ${⊢}{r}={p}\to {r}\left({G}\right)={p}\left({G}\right)$
91 90 eqeq2d ${⊢}{r}={p}\to \left({i}={r}\left({G}\right)↔{i}={p}\left({G}\right)\right)$
92 eleq1w ${⊢}{r}={p}\to \left({r}\in {E}↔{p}\in {E}\right)$
93 91 92 anbi12d ${⊢}{r}={p}\to \left(\left({i}={r}\left({G}\right)\wedge {r}\in {E}\right)↔\left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)$
94 86 87 89 93 opelopab ${⊢}⟨{i},{p}⟩\in \left\{⟨{g},{r}⟩|\left({g}={r}\left({G}\right)\wedge {r}\in {E}\right)\right\}↔\left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)$
95 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dih1dimatlem0 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\wedge {s}\ne {O}\right)\to \left(\left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)↔\left(\left({i}\in {T}\wedge {p}\in {E}\right)\wedge \exists {t}\in {E}\phantom{\rule{.4em}{0ex}}\left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\right)$
96 95 3expa ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to \left(\left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)↔\left(\left({i}\in {T}\wedge {p}\in {E}\right)\wedge \exists {t}\in {E}\phantom{\rule{.4em}{0ex}}\left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\right)$
97 opelxp ${⊢}⟨{i},{p}⟩\in \left({T}×{E}\right)↔\left({i}\in {T}\wedge {p}\in {E}\right)$
98 86 87 opth ${⊢}⟨{i},{p}⟩=⟨{t}\left({f}\right),{t}\circ {s}⟩↔\left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)$
99 98 rexbii ${⊢}\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}⟨{i},{p}⟩=⟨{t}\left({f}\right),{t}\circ {s}⟩↔\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}\left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)$
100 97 99 anbi12i ${⊢}\left(⟨{i},{p}⟩\in \left({T}×{E}\right)\wedge \exists {t}\in {E}\phantom{\rule{.4em}{0ex}}⟨{i},{p}⟩=⟨{t}\left({f}\right),{t}\circ {s}⟩\right)↔\left(\left({i}\in {T}\wedge {p}\in {E}\right)\wedge \exists {t}\in {E}\phantom{\rule{.4em}{0ex}}\left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)$
101 96 100 syl6bbr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to \left(\left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)↔\left(⟨{i},{p}⟩\in \left({T}×{E}\right)\wedge \exists {t}\in {E}\phantom{\rule{.4em}{0ex}}⟨{i},{p}⟩=⟨{t}\left({f}\right),{t}\circ {s}⟩\right)\right)$
102 eqeq1 ${⊢}{u}=⟨{i},{p}⟩\to \left({u}=⟨{t}\left({f}\right),{t}\circ {s}⟩↔⟨{i},{p}⟩=⟨{t}\left({f}\right),{t}\circ {s}⟩\right)$
103 102 rexbidv ${⊢}{u}=⟨{i},{p}⟩\to \left(\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩↔\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}⟨{i},{p}⟩=⟨{t}\left({f}\right),{t}\circ {s}⟩\right)$
104 103 elrab ${⊢}⟨{i},{p}⟩\in \left\{{u}\in \left({T}×{E}\right)|\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩\right\}↔\left(⟨{i},{p}⟩\in \left({T}×{E}\right)\wedge \exists {t}\in {E}\phantom{\rule{.4em}{0ex}}⟨{i},{p}⟩=⟨{t}\left({f}\right),{t}\circ {s}⟩\right)$
105 101 104 syl6bbr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to \left(\left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)↔⟨{i},{p}⟩\in \left\{{u}\in \left({T}×{E}\right)|\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩\right\}\right)$
106 94 105 syl5rbb ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to \left(⟨{i},{p}⟩\in \left\{{u}\in \left({T}×{E}\right)|\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩\right\}↔⟨{i},{p}⟩\in \left\{⟨{g},{r}⟩|\left({g}={r}\left({G}\right)\wedge {r}\in {E}\right)\right\}\right)$
107 84 85 106 eqrelrdv ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to \left\{{u}\in \left({T}×{E}\right)|\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}{u}=⟨{t}\left({f}\right),{t}\circ {s}⟩\right\}=\left\{⟨{g},{r}⟩|\left({g}={r}\left({G}\right)\wedge {r}\in {E}\right)\right\}$
108 80 107 eqtrd
109 1 2 53 dvhlmod ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {U}\in \mathrm{LMod}$
110 1 9 11 2 15 dvhelvbasei ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\to ⟨{f},{s}⟩\in {V}$
111 110 adantr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to ⟨{f},{s}⟩\in {V}$
112 13 54 15 16 18 lspsn
113 109 111 112 syl2anc
114 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {s}\ne {O}$
115 5 1 9 11 12 2 13 14 tendoinvcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in {E}\wedge {s}\ne {O}\right)\to \left({J}\left({s}\right)\in {E}\wedge {J}\left({s}\right)\ne {O}\right)$
116 115 simpld ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in {E}\wedge {s}\ne {O}\right)\to {J}\left({s}\right)\in {E}$
117 53 70 114 116 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {J}\left({s}\right)\in {E}$
118 1 9 11 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {J}\left({s}\right)\in {E}\wedge {f}\in {T}\right)\to {J}\left({s}\right)\left({f}\right)\in {T}$
119 53 117 68 118 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {J}\left({s}\right)\left({f}\right)\in {T}$
120 6 7 1 8 lhpocnel2
121 53 120 syl
122 6 7 1 9 ltrnel
123 53 119 121 122 syl3anc
124 eqid ${⊢}\mathrm{DIsoC}\left({K}\right)\left({W}\right)=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
125 6 7 1 124 3 dihvalcqat
126 53 123 125 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {I}\left({J}\left({s}\right)\left({f}\right)\left({P}\right)\right)=\mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({J}\left({s}\right)\left({f}\right)\left({P}\right)\right)$
127 6 7 1 8 9 11 124 20 dicval2
128 53 123 127 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to \mathrm{DIsoC}\left({K}\right)\left({W}\right)\left({J}\left({s}\right)\left({f}\right)\left({P}\right)\right)=\left\{⟨{g},{r}⟩|\left({g}={r}\left({G}\right)\wedge {r}\in {E}\right)\right\}$
129 126 128 eqtrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {I}\left({J}\left({s}\right)\left({f}\right)\left({P}\right)\right)=\left\{⟨{g},{r}⟩|\left({g}={r}\left({G}\right)\wedge {r}\in {E}\right)\right\}$
130 108 113 129 3eqtr4d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {N}\left(\left\{⟨{f},{s}⟩\right\}\right)={I}\left({J}\left({s}\right)\left({f}\right)\left({P}\right)\right)$
131 5 1 3 dihfn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}Fn{B}$
132 131 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\to {I}Fn{B}$
133 132 adantr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {I}Fn{B}$
134 simplll ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {K}\in \mathrm{HL}$
135 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
136 134 135 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {K}\in \mathrm{OP}$
137 5 1 lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$
138 137 ad3antlr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {W}\in {B}$
139 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
140 5 139 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {W}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({W}\right)\in {B}$
141 136 138 140 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to \mathrm{oc}\left({K}\right)\left({W}\right)\in {B}$
142 8 141 eqeltrid ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {P}\in {B}$
143 5 1 9 ltrncl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {J}\left({s}\right)\left({f}\right)\in {T}\wedge {P}\in {B}\right)\to {J}\left({s}\right)\left({f}\right)\left({P}\right)\in {B}$
144 53 119 142 143 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {J}\left({s}\right)\left({f}\right)\left({P}\right)\in {B}$
145 fnfvelrn ${⊢}\left({I}Fn{B}\wedge {J}\left({s}\right)\left({f}\right)\left({P}\right)\in {B}\right)\to {I}\left({J}\left({s}\right)\left({f}\right)\left({P}\right)\right)\in \mathrm{ran}{I}$
146 133 144 145 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {I}\left({J}\left({s}\right)\left({f}\right)\left({P}\right)\right)\in \mathrm{ran}{I}$
147 130 146 eqeltrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\wedge {s}\ne {O}\right)\to {N}\left(\left\{⟨{f},{s}⟩\right\}\right)\in \mathrm{ran}{I}$
148 52 147 pm2.61dane ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in {T}\wedge {s}\in {E}\right)\right)\to {N}\left(\left\{⟨{f},{s}⟩\right\}\right)\in \mathrm{ran}{I}$
149 148 ralrimivva ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\forall {s}\in {E}\phantom{\rule{.4em}{0ex}}{N}\left(\left\{⟨{f},{s}⟩\right\}\right)\in \mathrm{ran}{I}$
150 sneq ${⊢}{v}=⟨{f},{s}⟩\to \left\{{v}\right\}=\left\{⟨{f},{s}⟩\right\}$
151 150 fveq2d ${⊢}{v}=⟨{f},{s}⟩\to {N}\left(\left\{{v}\right\}\right)={N}\left(\left\{⟨{f},{s}⟩\right\}\right)$
152 151 eleq1d ${⊢}{v}=⟨{f},{s}⟩\to \left({N}\left(\left\{{v}\right\}\right)\in \mathrm{ran}{I}↔{N}\left(\left\{⟨{f},{s}⟩\right\}\right)\in \mathrm{ran}{I}\right)$
153 152 ralxp ${⊢}\forall {v}\in \left({T}×{E}\right)\phantom{\rule{.4em}{0ex}}{N}\left(\left\{{v}\right\}\right)\in \mathrm{ran}{I}↔\forall {f}\in {T}\phantom{\rule{.4em}{0ex}}\forall {s}\in {E}\phantom{\rule{.4em}{0ex}}{N}\left(\left\{⟨{f},{s}⟩\right\}\right)\in \mathrm{ran}{I}$
154 149 153 sylibr ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \forall {v}\in \left({T}×{E}\right)\phantom{\rule{.4em}{0ex}}{N}\left(\left\{{v}\right\}\right)\in \mathrm{ran}{I}$
155 154 r19.21bi ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {v}\in \left({T}×{E}\right)\right)\to {N}\left(\left\{{v}\right\}\right)\in \mathrm{ran}{I}$
156 30 155 syldan
157 eleq1a ${⊢}{N}\left(\left\{{v}\right\}\right)\in \mathrm{ran}{I}\to \left({D}={N}\left(\left\{{v}\right\}\right)\to {D}\in \mathrm{ran}{I}\right)$
158 156 157 syl
159 158 rexlimdva
161 25 160 mpd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {D}\in {A}\right)\to {D}\in \mathrm{ran}{I}$