Proof of Theorem tendospcanN
Step | Hyp | Ref
| Expression |
1 | | tendospcan.h |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | tendospcan.t |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
3 | | tendospcan.e |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
4 | 1, 2, 3 | tendocnv 39035 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → ◡(𝑆‘𝐺) = (𝑆‘◡𝐺)) |
5 | 4 | 3adant3l 1179 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ◡(𝑆‘𝐺) = (𝑆‘◡𝐺)) |
6 | 5 | coeq2d 5771 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑆‘𝐹) ∘ ◡(𝑆‘𝐺)) = ((𝑆‘𝐹) ∘ (𝑆‘◡𝐺))) |
7 | | simp1 1135 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
8 | | simp2 1136 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → 𝑆 ∈ 𝐸) |
9 | | simp3l 1200 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → 𝐹 ∈ 𝑇) |
10 | | simp3r 1201 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → 𝐺 ∈ 𝑇) |
11 | 1, 2 | ltrncnv 38160 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → ◡𝐺 ∈ 𝑇) |
12 | 7, 10, 11 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ◡𝐺 ∈ 𝑇) |
13 | 1, 2, 3 | tendospdi1 39034 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ ◡𝐺 ∈ 𝑇)) → (𝑆‘(𝐹 ∘ ◡𝐺)) = ((𝑆‘𝐹) ∘ (𝑆‘◡𝐺))) |
14 | 7, 8, 9, 12, 13 | syl13anc 1371 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → (𝑆‘(𝐹 ∘ ◡𝐺)) = ((𝑆‘𝐹) ∘ (𝑆‘◡𝐺))) |
15 | 6, 14 | eqtr4d 2781 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑆‘𝐹) ∘ ◡(𝑆‘𝐺)) = (𝑆‘(𝐹 ∘ ◡𝐺))) |
16 | 15 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → ((𝑆‘𝐹) ∘ ◡(𝑆‘𝐺)) = (𝑆‘(𝐹 ∘ ◡𝐺))) |
17 | 16 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → (((𝑆‘𝐹) ∘ ◡(𝑆‘𝐺)) = ( I ↾ 𝐵) ↔ (𝑆‘(𝐹 ∘ ◡𝐺)) = ( I ↾ 𝐵))) |
18 | | simpl1 1190 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
19 | | simpl2 1191 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → 𝑆 ∈ 𝐸) |
20 | | simpl3l 1227 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → 𝐹 ∈ 𝑇) |
21 | 1, 2, 3 | tendocl 38781 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑆‘𝐹) ∈ 𝑇) |
22 | 18, 19, 20, 21 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → (𝑆‘𝐹) ∈ 𝑇) |
23 | | simpl3r 1228 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → 𝐺 ∈ 𝑇) |
24 | 1, 2, 3 | tendocl 38781 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑆‘𝐺) ∈ 𝑇) |
25 | 18, 19, 23, 24 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → (𝑆‘𝐺) ∈ 𝑇) |
26 | | tendospcan.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 = (Base‘𝐾) |
27 | 26, 1, 2 | ltrncoidN 38142 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐹) ∈ 𝑇 ∧ (𝑆‘𝐺) ∈ 𝑇) → (((𝑆‘𝐹) ∘ ◡(𝑆‘𝐺)) = ( I ↾ 𝐵) ↔ (𝑆‘𝐹) = (𝑆‘𝐺))) |
28 | 18, 22, 25, 27 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → (((𝑆‘𝐹) ∘ ◡(𝑆‘𝐺)) = ( I ↾ 𝐵) ↔ (𝑆‘𝐹) = (𝑆‘𝐺))) |
29 | 18, 23, 11 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → ◡𝐺 ∈ 𝑇) |
30 | 1, 2 | ltrnco 38733 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ◡𝐺 ∈ 𝑇) → (𝐹 ∘ ◡𝐺) ∈ 𝑇) |
31 | 18, 20, 29, 30 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → (𝐹 ∘ ◡𝐺) ∈ 𝑇) |
32 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) |
33 | | tendospcan.o |
. . . . . . . . . . . . . 14
⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
34 | 26, 1, 2, 3, 33 | tendoid0 38839 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ ((𝐹 ∘ ◡𝐺) ∈ 𝑇 ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵))) → ((𝑆‘(𝐹 ∘ ◡𝐺)) = ( I ↾ 𝐵) ↔ 𝑆 = 𝑂)) |
35 | 18, 19, 31, 32, 34 | syl112anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → ((𝑆‘(𝐹 ∘ ◡𝐺)) = ( I ↾ 𝐵) ↔ 𝑆 = 𝑂)) |
36 | 17, 28, 35 | 3bitr3d 309 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → ((𝑆‘𝐹) = (𝑆‘𝐺) ↔ 𝑆 = 𝑂)) |
37 | 36 | biimpd 228 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵)) → ((𝑆‘𝐹) = (𝑆‘𝐺) → 𝑆 = 𝑂)) |
38 | 37 | impancom 452 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑆‘𝐹) = (𝑆‘𝐺)) → ((𝐹 ∘ ◡𝐺) ≠ ( I ↾ 𝐵) → 𝑆 = 𝑂)) |
39 | 38 | necon1d 2965 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑆‘𝐹) = (𝑆‘𝐺)) → (𝑆 ≠ 𝑂 → (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵))) |
40 | | simpl1 1190 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑆‘𝐹) = (𝑆‘𝐺)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
41 | | simpl3l 1227 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑆‘𝐹) = (𝑆‘𝐺)) → 𝐹 ∈ 𝑇) |
42 | | simpl3r 1228 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑆‘𝐹) = (𝑆‘𝐺)) → 𝐺 ∈ 𝑇) |
43 | 26, 1, 2 | ltrncoidN 38142 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵) ↔ 𝐹 = 𝐺)) |
44 | 40, 41, 42, 43 | syl3anc 1370 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑆‘𝐹) = (𝑆‘𝐺)) → ((𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵) ↔ 𝐹 = 𝐺)) |
45 | 39, 44 | sylibd 238 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑆‘𝐹) = (𝑆‘𝐺)) → (𝑆 ≠ 𝑂 → 𝐹 = 𝐺)) |
46 | 45 | 3exp1 1351 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑆 ∈ 𝐸 → ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑆‘𝐹) = (𝑆‘𝐺) → (𝑆 ≠ 𝑂 → 𝐹 = 𝐺))))) |
47 | 46 | com24 95 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((𝑆‘𝐹) = (𝑆‘𝐺) → ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑆 ∈ 𝐸 → (𝑆 ≠ 𝑂 → 𝐹 = 𝐺))))) |
48 | 47 | imp5a 441 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((𝑆‘𝐹) = (𝑆‘𝐺) → ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → 𝐹 = 𝐺)))) |
49 | 48 | com24 95 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → ((𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑆‘𝐹) = (𝑆‘𝐺) → 𝐹 = 𝐺)))) |
50 | 49 | 3imp 1110 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑆‘𝐹) = (𝑆‘𝐺) → 𝐹 = 𝐺)) |
51 | | fveq2 6774 |
. 2
⊢ (𝐹 = 𝐺 → (𝑆‘𝐹) = (𝑆‘𝐺)) |
52 | 50, 51 | impbid1 224 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑆‘𝐹) = (𝑆‘𝐺) ↔ 𝐹 = 𝐺)) |