# 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 syl5req ( ( ( ( 𝐾 ∈ 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 ∧ 𝑊𝐻 ) ∧ ( 𝑓𝑇𝑠𝐸 ) ∧ 𝑠𝑂 ) → ( ( 𝑖 = ( 𝑝𝐺 ) ∧ 𝑝𝐸 ) ↔ ( ( 𝑖𝑇𝑝𝐸 ) ∧ ∃ 𝑡𝐸 ( 𝑖 = ( 𝑡𝑓 ) ∧ 𝑝 = ( 𝑡𝑠 ) ) ) ) )