Step |
Hyp |
Ref |
Expression |
1 |
|
tendoid.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
tendoid.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
3 |
|
tendoid.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
eqid |
⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
1 2 4
|
idltrn |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
6 |
5
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
7 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
8 |
|
eqid |
⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
9 |
7 2 4 8 3
|
tendotp |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( I ↾ 𝐵 ) ) ) |
10 |
6 9
|
mpd3an3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( I ↾ 𝐵 ) ) ) |
11 |
|
eqid |
⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 ) |
12 |
1 11 2 8
|
trlid0 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( I ↾ 𝐵 ) ) = ( 0. ‘ 𝐾 ) ) |
13 |
12
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( I ↾ 𝐵 ) ) = ( 0. ‘ 𝐾 ) ) |
14 |
10 13
|
breqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ) |
15 |
|
hlop |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP ) |
16 |
15
|
ad2antrr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → 𝐾 ∈ OP ) |
17 |
2 4 3
|
tendocl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( I ↾ 𝐵 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
18 |
6 17
|
mpd3an3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) |
19 |
1 2 4 8
|
trlcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) ∈ 𝐵 ) |
20 |
18 19
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) ∈ 𝐵 ) |
21 |
1 7 11
|
ople0 |
⊢ ( ( 𝐾 ∈ OP ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) ∈ 𝐵 ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) = ( 0. ‘ 𝐾 ) ) ) |
22 |
16 20 21
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) = ( 0. ‘ 𝐾 ) ) ) |
23 |
14 22
|
mpbid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) = ( 0. ‘ 𝐾 ) ) |
24 |
1 11 2 4 8
|
trlid0b |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) = ( 0. ‘ 𝐾 ) ) ) |
25 |
18 24
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( ( 𝑆 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( I ↾ 𝐵 ) ) ) = ( 0. ‘ 𝐾 ) ) ) |
26 |
23 25
|
mpbird |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ) → ( 𝑆 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) ) |