Metamath Proof Explorer

Theorem dih1dimatlem0

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

Ref Expression
Hypotheses dih1dimat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dih1dimat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dih1dimat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dih1dimat.l ⊢ ≤ = ( le ‘ 𝐾 )
dih1dimat.c ⊢ 𝐶 = ( Atoms ‘ 𝐾 )
dih1dimat.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dih1dimat.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
dih1dimat.d ⊢ 𝐹 = ( Scalar ‘ 𝑈 )
dih1dimat.j ⊢ 𝐽 = ( invr ‘ 𝐹 )
dih1dimat.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dih1dimat.m ⊢ · = ( ·𝑠 ‘ 𝑈 )
dih1dimat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
dih1dimat.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dih1dimat.z ⊢ 0 = ( 0g ‘ 𝑈 )
dih1dimat.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) )
Assertion dih1dimatlem0 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ↔ ( ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dih1dimat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dih1dimat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dih1dimat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dih1dimat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
5 dih1dimat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
6 dih1dimat.l ⊢ ≤ = ( le ‘ 𝐾 )
7 dih1dimat.c ⊢ 𝐶 = ( Atoms ‘ 𝐾 )
8 dih1dimat.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
9 dih1dimat.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
10 dih1dimat.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
11 dih1dimat.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
12 dih1dimat.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
13 dih1dimat.d ⊢ 𝐹 = ( Scalar ‘ 𝑈 )
14 dih1dimat.j ⊢ 𝐽 = ( invr ‘ 𝐹 )
15 dih1dimat.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
16 dih1dimat.m ⊢ · = ( ·𝑠 ‘ 𝑈 )
17 dih1dimat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
18 dih1dimat.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
19 dih1dimat.z ⊢ 0 = ( 0g ‘ 𝑈 )
20 dih1dimat.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) )
21 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → 𝑖 = ( 𝑝 ‘ 𝐺 ) )
22 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → 𝑝 ∈ 𝐸 )
24 6 7 1 8 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊 ) )
25 22 24 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( 𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊 ) )
26 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → 𝑠 ∈ 𝐸 )
27 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → 𝑠 ≠ 𝑂 )
28 5 1 9 11 12 2 13 14 tendoinvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 ∧ ( 𝐽 ‘ 𝑠 ) ≠ 𝑂 ) )
29 28 simpld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) → ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 )
30 22 26 27 29 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 )
31 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → 𝑓 ∈ 𝑇 )
32 1 9 11 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ∈ 𝑇 )
33 22 30 31 32 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ∈ 𝑇 )
34 6 7 1 9 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐶 ∧ ¬ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ≤ 𝑊 ) )
35 22 33 25 34 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐶 ∧ ¬ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ≤ 𝑊 ) )
36 6 7 1 9 20 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐶 ∧ ¬ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
37 22 25 35 36 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → 𝐺 ∈ 𝑇 )
38 1 9 11 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑝 ‘ 𝐺 ) ∈ 𝑇 )
39 22 23 37 38 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( 𝑝 ‘ 𝐺 ) ∈ 𝑇 )
40 21 39 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → 𝑖 ∈ 𝑇 )
41 1 11 tendococl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ 𝐸 ∧ ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 ) → ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ∈ 𝐸 )
42 22 23 30 41 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ∈ 𝐸 )
43 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
44 24 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊 ) )
45 29 3adant2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 )
46 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → 𝑓 ∈ 𝑇 )
47 43 45 46 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ∈ 𝑇 )
48 43 47 44 34 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → ( ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐶 ∧ ¬ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ≤ 𝑊 ) )
49 43 44 48 36 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → 𝐺 ∈ 𝑇 )
50 6 7 1 9 20 ltrniotaval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ∈ 𝐶 ∧ ¬ ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ≤ 𝑊 ) ) → ( 𝐺 ‘ 𝑃 ) = ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) )
51 43 44 48 50 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → ( 𝐺 ‘ 𝑃 ) = ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) )
52 6 7 1 9 cdlemd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐺 ‘ 𝑃 ) = ( ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ‘ 𝑃 ) ) → 𝐺 = ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) )
53 43 49 47 44 51 52 syl311anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → 𝐺 = ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) )
54 53 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → 𝐺 = ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) )
55 54 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( 𝑝 ‘ 𝐺 ) = ( 𝑝 ‘ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ) )
56 1 9 11 tendocoval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐸 ∧ ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ‘ 𝑓 ) = ( 𝑝 ‘ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ) )
57 22 23 30 31 56 syl121anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ‘ 𝑓 ) = ( 𝑝 ‘ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ) )
58 55 21 57 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → 𝑖 = ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ‘ 𝑓 ) )
59 coass ⊢ ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ∘ 𝑠 ) = ( 𝑝 ∘ ( ( 𝐽 ‘ 𝑠 ) ∘ 𝑠 ) )
60 5 1 9 11 12 2 13 14 tendolinv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝐽 ‘ 𝑠 ) ∘ 𝑠 ) = ( I ↾ 𝑇 ) )
61 22 26 27 60 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( ( 𝐽 ‘ 𝑠 ) ∘ 𝑠 ) = ( I ↾ 𝑇 ) )
62 61 coeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( 𝑝 ∘ ( ( 𝐽 ‘ 𝑠 ) ∘ 𝑠 ) ) = ( 𝑝 ∘ ( I ↾ 𝑇 ) ) )
63 1 9 11 tendo1mulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑝 ∈ 𝐸 ) → ( 𝑝 ∘ ( I ↾ 𝑇 ) ) = 𝑝 )
64 22 23 63 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( 𝑝 ∘ ( I ↾ 𝑇 ) ) = 𝑝 )
65 62 64 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( 𝑝 ∘ ( ( 𝐽 ‘ 𝑠 ) ∘ 𝑠 ) ) = 𝑝 )
66 59 65 eqtr2id ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → 𝑝 = ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ∘ 𝑠 ) )
67 fveq1 ⊢ ( 𝑡 = ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) → ( 𝑡 ‘ 𝑓 ) = ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ‘ 𝑓 ) )
68 67 eqeq2d ⊢ ( 𝑡 = ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) → ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ↔ 𝑖 = ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ‘ 𝑓 ) ) )
69 coeq1 ⊢ ( 𝑡 = ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) → ( 𝑡 ∘ 𝑠 ) = ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ∘ 𝑠 ) )
70 69 eqeq2d ⊢ ( 𝑡 = ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) → ( 𝑝 = ( 𝑡 ∘ 𝑠 ) ↔ 𝑝 = ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ∘ 𝑠 ) ) )
71 68 70 anbi12d ⊢ ( 𝑡 = ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) → ( ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ↔ ( 𝑖 = ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ‘ 𝑓 ) ∧ 𝑝 = ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ∘ 𝑠 ) ) ) )
72 71 rspcev ⊢ ( ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ∈ 𝐸 ∧ ( 𝑖 = ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ‘ 𝑓 ) ∧ 𝑝 = ( ( 𝑝 ∘ ( 𝐽 ‘ 𝑠 ) ) ∘ 𝑠 ) ) ) → ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) )
73 42 58 66 72 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) )
74 40 23 73 jca31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ) → ( ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) )
75 simp3r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → 𝑝 = ( 𝑡 ∘ 𝑠 ) )
76 75 fveq1d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( 𝑝 ‘ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ) = ( ( 𝑡 ∘ 𝑠 ) ‘ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ) )
77 simp1l1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
78 simp2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → 𝑡 ∈ 𝐸 )
79 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) → 𝑠 ∈ 𝐸 )
80 79 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → 𝑠 ∈ 𝐸 )
81 1 11 tendococl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ∧ 𝑠 ∈ 𝐸 ) → ( 𝑡 ∘ 𝑠 ) ∈ 𝐸 )
82 77 78 80 81 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( 𝑡 ∘ 𝑠 ) ∈ 𝐸 )
83 simp1l3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → 𝑠 ≠ 𝑂 )
84 77 80 83 29 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 )
85 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) → 𝑓 ∈ 𝑇 )
86 85 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → 𝑓 ∈ 𝑇 )
87 1 9 11 tendocoval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑡 ∘ 𝑠 ) ∈ 𝐸 ∧ ( 𝐽 ‘ 𝑠 ) ∈ 𝐸 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( ( 𝑡 ∘ 𝑠 ) ∘ ( 𝐽 ‘ 𝑠 ) ) ‘ 𝑓 ) = ( ( 𝑡 ∘ 𝑠 ) ‘ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ) )
88 77 82 84 86 87 syl121anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( ( ( 𝑡 ∘ 𝑠 ) ∘ ( 𝐽 ‘ 𝑠 ) ) ‘ 𝑓 ) = ( ( 𝑡 ∘ 𝑠 ) ‘ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ) )
89 coass ⊢ ( ( 𝑡 ∘ 𝑠 ) ∘ ( 𝐽 ‘ 𝑠 ) ) = ( 𝑡 ∘ ( 𝑠 ∘ ( 𝐽 ‘ 𝑠 ) ) )
90 5 1 9 11 12 2 13 14 tendorinv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) → ( 𝑠 ∘ ( 𝐽 ‘ 𝑠 ) ) = ( I ↾ 𝑇 ) )
91 77 80 83 90 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( 𝑠 ∘ ( 𝐽 ‘ 𝑠 ) ) = ( I ↾ 𝑇 ) )
92 91 coeq2d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( 𝑡 ∘ ( 𝑠 ∘ ( 𝐽 ‘ 𝑠 ) ) ) = ( 𝑡 ∘ ( I ↾ 𝑇 ) ) )
93 1 9 11 tendo1mulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑡 ∈ 𝐸 ) → ( 𝑡 ∘ ( I ↾ 𝑇 ) ) = 𝑡 )
94 77 78 93 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( 𝑡 ∘ ( I ↾ 𝑇 ) ) = 𝑡 )
95 92 94 eqtrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( 𝑡 ∘ ( 𝑠 ∘ ( 𝐽 ‘ 𝑠 ) ) ) = 𝑡 )
96 89 95 syl5eq ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( ( 𝑡 ∘ 𝑠 ) ∘ ( 𝐽 ‘ 𝑠 ) ) = 𝑡 )
97 96 fveq1d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( ( ( 𝑡 ∘ 𝑠 ) ∘ ( 𝐽 ‘ 𝑠 ) ) ‘ 𝑓 ) = ( 𝑡 ‘ 𝑓 ) )
98 76 88 97 3eqtr2rd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( 𝑡 ‘ 𝑓 ) = ( 𝑝 ‘ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ) )
99 simp3l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → 𝑖 = ( 𝑡 ‘ 𝑓 ) )
100 53 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) → 𝐺 = ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) )
101 100 3ad2ant1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → 𝐺 = ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) )
102 101 fveq2d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → ( 𝑝 ‘ 𝐺 ) = ( 𝑝 ‘ ( ( 𝐽 ‘ 𝑠 ) ‘ 𝑓 ) ) )
103 98 99 102 3eqtr4d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) ∧ 𝑡 ∈ 𝐸 ∧ ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) → 𝑖 = ( 𝑝 ‘ 𝐺 ) )
104 103 rexlimdv3a ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ) → ( ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) → 𝑖 = ( 𝑝 ‘ 𝐺 ) ) )
105 104 impr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) ) → 𝑖 = ( 𝑝 ‘ 𝐺 ) )
106 simprlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) ) → 𝑝 ∈ 𝐸 )
107 105 106 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) ∧ ( ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) ) → ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) )
108 74 107 impbida ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ 𝑠 ≠ 𝑂 ) → ( ( 𝑖 = ( 𝑝 ‘ 𝐺 ) ∧ 𝑝 ∈ 𝐸 ) ↔ ( ( 𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸 ) ∧ ∃ 𝑡 ∈ 𝐸 ( 𝑖 = ( 𝑡 ‘ 𝑓 ) ∧ 𝑝 = ( 𝑡 ∘ 𝑠 ) ) ) ) )