# Metamath Proof Explorer

## Theorem dih1dimatlem0

Description: Lemma for dih1dimat . (Contributed by NM, 11-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 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)$

### 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 simprl ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {i}={p}\left({G}\right)$
22 simpl1 ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
23 simprr ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {p}\in {E}$
24 6 7 1 8 lhpocnel2
25 22 24 syl
26 simpl2r ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {s}\in {E}$
27 simpl3 ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {s}\ne {O}$
28 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)$
29 28 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}$
30 22 26 27 29 syl3anc ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {J}\left({s}\right)\in {E}$
31 simpl2l ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {f}\in {T}$
32 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}$
33 22 30 31 32 syl3anc ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {J}\left({s}\right)\left({f}\right)\in {T}$
34 6 7 1 9 ltrnel
35 22 33 25 34 syl3anc
36 6 7 1 9 20 ltrniotacl
37 22 25 35 36 syl3anc ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {G}\in {T}$
38 1 9 11 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {p}\in {E}\wedge {G}\in {T}\right)\to {p}\left({G}\right)\in {T}$
39 22 23 37 38 syl3anc ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {p}\left({G}\right)\in {T}$
40 21 39 eqeltrd ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {i}\in {T}$
41 1 11 tendococl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {p}\in {E}\wedge {J}\left({s}\right)\in {E}\right)\to {p}\circ {J}\left({s}\right)\in {E}$
42 22 23 30 41 syl3anc ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {p}\circ {J}\left({s}\right)\in {E}$
43 simp1 ${⊢}\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({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
45 29 3adant2l ${⊢}\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 {J}\left({s}\right)\in {E}$
46 simp2l ${⊢}\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 {f}\in {T}$
47 43 45 46 32 syl3anc ${⊢}\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 {J}\left({s}\right)\left({f}\right)\in {T}$
48 43 47 44 34 syl3anc
49 43 44 48 36 syl3anc ${⊢}\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 {G}\in {T}$
50 6 7 1 9 20 ltrniotaval
51 43 44 48 50 syl3anc ${⊢}\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 {G}\left({P}\right)={J}\left({s}\right)\left({f}\right)\left({P}\right)$
52 6 7 1 9 cdlemd
53 43 49 47 44 51 52 syl311anc ${⊢}\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 {G}={J}\left({s}\right)\left({f}\right)$
54 53 adantr ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {G}={J}\left({s}\right)\left({f}\right)$
55 54 fveq2d ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {p}\left({G}\right)={p}\left({J}\left({s}\right)\left({f}\right)\right)$
56 1 9 11 tendocoval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({p}\in {E}\wedge {J}\left({s}\right)\in {E}\right)\wedge {f}\in {T}\right)\to \left({p}\circ {J}\left({s}\right)\right)\left({f}\right)={p}\left({J}\left({s}\right)\left({f}\right)\right)$
57 22 23 30 31 56 syl121anc ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to \left({p}\circ {J}\left({s}\right)\right)\left({f}\right)={p}\left({J}\left({s}\right)\left({f}\right)\right)$
58 55 21 57 3eqtr4d ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {i}=\left({p}\circ {J}\left({s}\right)\right)\left({f}\right)$
59 coass ${⊢}\left({p}\circ {J}\left({s}\right)\right)\circ {s}={p}\circ \left({J}\left({s}\right)\circ {s}\right)$
60 5 1 9 11 12 2 13 14 tendolinv ${⊢}\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)\circ {s}={\mathrm{I}↾}_{{T}}$
61 22 26 27 60 syl3anc ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {J}\left({s}\right)\circ {s}={\mathrm{I}↾}_{{T}}$
62 61 coeq2d ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {p}\circ \left({J}\left({s}\right)\circ {s}\right)={p}\circ \left({\mathrm{I}↾}_{{T}}\right)$
63 1 9 11 tendo1mulr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {p}\in {E}\right)\to {p}\circ \left({\mathrm{I}↾}_{{T}}\right)={p}$
64 22 23 63 syl2anc ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {p}\circ \left({\mathrm{I}↾}_{{T}}\right)={p}$
65 62 64 eqtrd ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {p}\circ \left({J}\left({s}\right)\circ {s}\right)={p}$
66 59 65 syl5req ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to {p}=\left({p}\circ {J}\left({s}\right)\right)\circ {s}$
67 fveq1 ${⊢}{t}={p}\circ {J}\left({s}\right)\to {t}\left({f}\right)=\left({p}\circ {J}\left({s}\right)\right)\left({f}\right)$
68 67 eqeq2d ${⊢}{t}={p}\circ {J}\left({s}\right)\to \left({i}={t}\left({f}\right)↔{i}=\left({p}\circ {J}\left({s}\right)\right)\left({f}\right)\right)$
69 coeq1 ${⊢}{t}={p}\circ {J}\left({s}\right)\to {t}\circ {s}=\left({p}\circ {J}\left({s}\right)\right)\circ {s}$
70 69 eqeq2d ${⊢}{t}={p}\circ {J}\left({s}\right)\to \left({p}={t}\circ {s}↔{p}=\left({p}\circ {J}\left({s}\right)\right)\circ {s}\right)$
71 68 70 anbi12d ${⊢}{t}={p}\circ {J}\left({s}\right)\to \left(\left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)↔\left({i}=\left({p}\circ {J}\left({s}\right)\right)\left({f}\right)\wedge {p}=\left({p}\circ {J}\left({s}\right)\right)\circ {s}\right)\right)$
72 71 rspcev ${⊢}\left({p}\circ {J}\left({s}\right)\in {E}\wedge \left({i}=\left({p}\circ {J}\left({s}\right)\right)\left({f}\right)\wedge {p}=\left({p}\circ {J}\left({s}\right)\right)\circ {s}\right)\right)\to \exists {t}\in {E}\phantom{\rule{.4em}{0ex}}\left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)$
73 42 58 66 72 syl12anc ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to \exists {t}\in {E}\phantom{\rule{.4em}{0ex}}\left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)$
74 40 23 73 jca31 ${⊢}\left(\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)\wedge \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)\right)\to \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)$
75 simp3r ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {p}={t}\circ {s}$
76 75 fveq1d ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {p}\left({J}\left({s}\right)\left({f}\right)\right)=\left({t}\circ {s}\right)\left({J}\left({s}\right)\left({f}\right)\right)$
77 simp1l1 ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
78 simp2 ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {t}\in {E}$
79 simpl2r ${⊢}\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\to {s}\in {E}$
80 79 3ad2ant1 ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {s}\in {E}$
81 1 11 tendococl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {t}\in {E}\wedge {s}\in {E}\right)\to {t}\circ {s}\in {E}$
82 77 78 80 81 syl3anc ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {t}\circ {s}\in {E}$
83 simp1l3 ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {s}\ne {O}$
84 77 80 83 29 syl3anc ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {J}\left({s}\right)\in {E}$
85 simpl2l ${⊢}\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\to {f}\in {T}$
86 85 3ad2ant1 ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {f}\in {T}$
87 1 9 11 tendocoval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({t}\circ {s}\in {E}\wedge {J}\left({s}\right)\in {E}\right)\wedge {f}\in {T}\right)\to \left(\left({t}\circ {s}\right)\circ {J}\left({s}\right)\right)\left({f}\right)=\left({t}\circ {s}\right)\left({J}\left({s}\right)\left({f}\right)\right)$
88 77 82 84 86 87 syl121anc ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to \left(\left({t}\circ {s}\right)\circ {J}\left({s}\right)\right)\left({f}\right)=\left({t}\circ {s}\right)\left({J}\left({s}\right)\left({f}\right)\right)$
89 coass ${⊢}\left({t}\circ {s}\right)\circ {J}\left({s}\right)={t}\circ \left({s}\circ {J}\left({s}\right)\right)$
90 5 1 9 11 12 2 13 14 tendorinv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {s}\in {E}\wedge {s}\ne {O}\right)\to {s}\circ {J}\left({s}\right)={\mathrm{I}↾}_{{T}}$
91 77 80 83 90 syl3anc ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {s}\circ {J}\left({s}\right)={\mathrm{I}↾}_{{T}}$
92 91 coeq2d ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {t}\circ \left({s}\circ {J}\left({s}\right)\right)={t}\circ \left({\mathrm{I}↾}_{{T}}\right)$
93 1 9 11 tendo1mulr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {t}\in {E}\right)\to {t}\circ \left({\mathrm{I}↾}_{{T}}\right)={t}$
94 77 78 93 syl2anc ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {t}\circ \left({\mathrm{I}↾}_{{T}}\right)={t}$
95 92 94 eqtrd ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {t}\circ \left({s}\circ {J}\left({s}\right)\right)={t}$
96 89 95 syl5eq ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to \left({t}\circ {s}\right)\circ {J}\left({s}\right)={t}$
97 96 fveq1d ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to \left(\left({t}\circ {s}\right)\circ {J}\left({s}\right)\right)\left({f}\right)={t}\left({f}\right)$
98 76 88 97 3eqtr2rd ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {t}\left({f}\right)={p}\left({J}\left({s}\right)\left({f}\right)\right)$
99 simp3l ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {i}={t}\left({f}\right)$
100 53 adantr ${⊢}\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\to {G}={J}\left({s}\right)\left({f}\right)$
101 100 3ad2ant1 ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {G}={J}\left({s}\right)\left({f}\right)$
102 101 fveq2d ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {p}\left({G}\right)={p}\left({J}\left({s}\right)\left({f}\right)\right)$
103 98 99 102 3eqtr4d ${⊢}\left(\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\wedge {t}\in {E}\wedge \left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\right)\to {i}={p}\left({G}\right)$
104 103 rexlimdv3a ${⊢}\left(\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)\wedge \left({i}\in {T}\wedge {p}\in {E}\right)\right)\to \left(\exists {t}\in {E}\phantom{\rule{.4em}{0ex}}\left({i}={t}\left({f}\right)\wedge {p}={t}\circ {s}\right)\to {i}={p}\left({G}\right)\right)$
105 104 impr ${⊢}\left(\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)\wedge \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)\to {i}={p}\left({G}\right)$
106 simprlr ${⊢}\left(\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)\wedge \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)\to {p}\in {E}$
107 105 106 jca ${⊢}\left(\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)\wedge \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)\to \left({i}={p}\left({G}\right)\wedge {p}\in {E}\right)$
108 74 107 impbida ${⊢}\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)$