Step |
Hyp |
Ref |
Expression |
1 |
|
tendosp.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
tendosp.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
tendosp.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
simp1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
5 |
1 2 3
|
tendocl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
7 |
6 1 2
|
ltrn1o |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 ) → ( 𝑆 ‘ 𝐹 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
8 |
4 5 7
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑆 ‘ 𝐹 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
9 |
|
f1ococnv1 |
⊢ ( ( 𝑆 ‘ 𝐹 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐹 ) ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) |
10 |
8 9
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐹 ) ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) |
11 |
10
|
coeq1d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐹 ) ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) = ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) ) |
12 |
|
simp2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → 𝑆 ∈ 𝐸 ) |
13 |
6 1 3
|
tendoid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑆 ‘ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) |
14 |
4 12 13
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑆 ‘ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) |
15 |
6 1 2
|
ltrn1o |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
16 |
15
|
3adant2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
17 |
|
f1ococnv2 |
⊢ ( 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) |
18 |
16 17
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) |
19 |
18
|
fveq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐹 ) ) = ( 𝑆 ‘ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) |
20 |
|
f1ococnv2 |
⊢ ( ( 𝑆 ‘ 𝐹 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) |
21 |
8 20
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) = ( I ↾ ( Base ‘ 𝐾 ) ) ) |
22 |
14 19 21
|
3eqtr4rd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) = ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐹 ) ) ) |
23 |
|
simp3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝑇 ) |
24 |
1 2
|
ltrncnv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ◡ 𝐹 ∈ 𝑇 ) |
25 |
24
|
3adant2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ◡ 𝐹 ∈ 𝑇 ) |
26 |
1 2 3
|
tendospdi1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) ) → ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐹 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) ) |
27 |
4 12 23 25 26
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐹 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) ) |
28 |
22 27
|
eqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) ) |
29 |
28
|
coeq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) ) = ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) ) ) |
30 |
|
coass |
⊢ ( ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐹 ) ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) = ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) ) |
31 |
|
coass |
⊢ ( ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐹 ) ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) = ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) ) |
32 |
29 30 31
|
3eqtr4g |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐹 ) ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) = ( ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐹 ) ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) ) |
33 |
10
|
coeq1d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐹 ) ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) = ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) ) |
34 |
1 2 3
|
tendocl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ◡ 𝐹 ∈ 𝑇 ) → ( 𝑆 ‘ ◡ 𝐹 ) ∈ 𝑇 ) |
35 |
25 34
|
syld3an3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑆 ‘ ◡ 𝐹 ) ∈ 𝑇 ) |
36 |
6 1 2
|
ltrn1o |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ ◡ 𝐹 ) ∈ 𝑇 ) → ( 𝑆 ‘ ◡ 𝐹 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
37 |
4 35 36
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑆 ‘ ◡ 𝐹 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
38 |
|
f1of |
⊢ ( ( 𝑆 ‘ ◡ 𝐹 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → ( 𝑆 ‘ ◡ 𝐹 ) : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) ) |
39 |
|
fcoi2 |
⊢ ( ( 𝑆 ‘ ◡ 𝐹 ) : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) = ( 𝑆 ‘ ◡ 𝐹 ) ) |
40 |
37 38 39
|
3syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ ( 𝑆 ‘ ◡ 𝐹 ) ) = ( 𝑆 ‘ ◡ 𝐹 ) ) |
41 |
32 33 40
|
3eqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( ◡ ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐹 ) ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) = ( 𝑆 ‘ ◡ 𝐹 ) ) |
42 |
1 2
|
ltrncnv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 ) |
43 |
4 5 42
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 ) |
44 |
6 1 2
|
ltrn1o |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ◡ ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝐹 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
45 |
4 43 44
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝐹 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
46 |
|
f1of |
⊢ ( ◡ ( 𝑆 ‘ 𝐹 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → ◡ ( 𝑆 ‘ 𝐹 ) : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) ) |
47 |
|
fcoi2 |
⊢ ( ◡ ( 𝑆 ‘ 𝐹 ) : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) = ◡ ( 𝑆 ‘ 𝐹 ) ) |
48 |
45 46 47
|
3syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ ◡ ( 𝑆 ‘ 𝐹 ) ) = ◡ ( 𝑆 ‘ 𝐹 ) ) |
49 |
11 41 48
|
3eqtr3rd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ ◡ 𝐹 ) ) |