Step |
Hyp |
Ref |
Expression |
1 |
|
tendospcan.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
tendospcan.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
3 |
|
tendospcan.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
tendospcan.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
tendospcan.o |
⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) |
6 |
2 3 4
|
tendocnv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝐺 ) = ( 𝑆 ‘ ◡ 𝐺 ) ) |
7 |
6
|
3adant3l |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ◡ ( 𝑆 ‘ 𝐺 ) = ( 𝑆 ‘ ◡ 𝐺 ) ) |
8 |
7
|
coeq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐺 ) ) ) |
9 |
|
simp1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
10 |
|
simp2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝑆 ∈ 𝐸 ) |
11 |
|
simp3l |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝐹 ∈ 𝑇 ) |
12 |
|
simp3r |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝐺 ∈ 𝑇 ) |
13 |
2 3
|
ltrncnv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ◡ 𝐺 ∈ 𝑇 ) |
14 |
9 12 13
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ◡ 𝐺 ∈ 𝑇 ) |
15 |
2 3 4
|
tendospdi1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ ◡ 𝐺 ∈ 𝑇 ) ) → ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐺 ) ) ) |
16 |
9 10 11 14 15
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐺 ) ) ) |
17 |
8 16
|
eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) ) |
18 |
17
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) ) |
19 |
18
|
eqeq1d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( I ↾ 𝐵 ) ↔ ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) = ( I ↾ 𝐵 ) ) ) |
20 |
|
simpl1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
21 |
|
simpl2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → 𝑆 ∈ 𝐸 ) |
22 |
|
simpl3l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → 𝐹 ∈ 𝑇 ) |
23 |
2 3 4
|
tendocl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 ) |
24 |
20 21 22 23
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 ) |
25 |
|
simpl3r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → 𝐺 ∈ 𝑇 ) |
26 |
2 3 4
|
tendocl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 ) |
27 |
20 21 25 26
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 ) |
28 |
1 2 3
|
ltrncoidN |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 ∧ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 ) → ( ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( I ↾ 𝐵 ) ↔ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) ) |
29 |
20 24 27 28
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( I ↾ 𝐵 ) ↔ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) ) |
30 |
20 25 13
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ◡ 𝐺 ∈ 𝑇 ) |
31 |
2 3
|
ltrnco |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ◡ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ ◡ 𝐺 ) ∈ 𝑇 ) |
32 |
20 22 30 31
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝐹 ∘ ◡ 𝐺 ) ∈ 𝑇 ) |
33 |
|
simpr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) |
34 |
1 2 3 4 5
|
tendoid0 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( ( 𝐹 ∘ ◡ 𝐺 ) ∈ 𝑇 ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) = ( I ↾ 𝐵 ) ↔ 𝑆 = 𝑂 ) ) |
35 |
20 21 32 33 34
|
syl112anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) = ( I ↾ 𝐵 ) ↔ 𝑆 = 𝑂 ) ) |
36 |
19 29 35
|
3bitr3d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ↔ 𝑆 = 𝑂 ) ) |
37 |
36
|
biimpd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → 𝑆 = 𝑂 ) ) |
38 |
37
|
impancom |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → ( ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) → 𝑆 = 𝑂 ) ) |
39 |
38
|
necon1d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → ( 𝑆 ≠ 𝑂 → ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) ) |
40 |
|
simpl1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
41 |
|
simpl3l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → 𝐹 ∈ 𝑇 ) |
42 |
|
simpl3r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → 𝐺 ∈ 𝑇 ) |
43 |
1 2 3
|
ltrncoidN |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ↔ 𝐹 = 𝐺 ) ) |
44 |
40 41 42 43
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → ( ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ↔ 𝐹 = 𝐺 ) ) |
45 |
39 44
|
sylibd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → ( 𝑆 ≠ 𝑂 → 𝐹 = 𝐺 ) ) |
46 |
45
|
3exp1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ 𝐸 → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → ( 𝑆 ≠ 𝑂 → 𝐹 = 𝐺 ) ) ) ) ) |
47 |
46
|
com24 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ∈ 𝐸 → ( 𝑆 ≠ 𝑂 → 𝐹 = 𝐺 ) ) ) ) ) |
48 |
47
|
imp5a |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → 𝐹 = 𝐺 ) ) ) ) |
49 |
48
|
com24 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → 𝐹 = 𝐺 ) ) ) ) |
50 |
49
|
3imp |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → 𝐹 = 𝐺 ) ) |
51 |
|
fveq2 |
⊢ ( 𝐹 = 𝐺 → ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) |
52 |
50 51
|
impbid1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ↔ 𝐹 = 𝐺 ) ) |