Step |
Hyp |
Ref |
Expression |
1 |
|
tendof.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
tendof.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
tendof.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
5 |
|
eqid |
⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
4 1 2 5 3
|
istendo |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ 𝐸 ↔ ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ 𝑓 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) ) ) |
7 |
|
coeq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∘ 𝑔 ) = ( 𝐹 ∘ 𝑔 ) ) |
8 |
7
|
fveq2d |
⊢ ( 𝑓 = 𝐹 → ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑆 ‘ ( 𝐹 ∘ 𝑔 ) ) ) |
9 |
|
fveq2 |
⊢ ( 𝑓 = 𝐹 → ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝐹 ) ) |
10 |
9
|
coeq1d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ) |
11 |
8 10
|
eqeq12d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ↔ ( 𝑆 ‘ ( 𝐹 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ) ) |
12 |
|
coeq2 |
⊢ ( 𝑔 = 𝐺 → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ 𝐺 ) ) |
13 |
12
|
fveq2d |
⊢ ( 𝑔 = 𝐺 → ( 𝑆 ‘ ( 𝐹 ∘ 𝑔 ) ) = ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) ) |
14 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( 𝑆 ‘ 𝑔 ) = ( 𝑆 ‘ 𝐺 ) ) |
15 |
14
|
coeq2d |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) |
16 |
13 15
|
eqeq12d |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑆 ‘ ( 𝐹 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ↔ ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) ) |
17 |
11 16
|
rspc2v |
⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) ) |
18 |
17
|
com12 |
⊢ ( ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) ) |
19 |
18
|
3ad2ant2 |
⊢ ( ( 𝑆 : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑓 ∈ 𝑇 ∀ 𝑔 ∈ 𝑇 ( 𝑆 ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( 𝑆 ‘ 𝑓 ) ∘ ( 𝑆 ‘ 𝑔 ) ) ∧ ∀ 𝑓 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ 𝑓 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) ) |
20 |
6 19
|
syl6bi |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ 𝐸 → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) ) ) |
21 |
20
|
3impia |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ 𝑆 ∈ 𝐸 ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) ) |
22 |
21
|
imp |
⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝑆 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) |