Proof of Theorem tendoeq2
| Step | Hyp | Ref
| Expression |
| 1 | | tendoeq2.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐾) |
| 2 | | tendoeq2.h |
. . . . . . . 8
⊢ 𝐻 = (LHyp‘𝐾) |
| 3 | | tendoeq2.e |
. . . . . . . 8
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
| 4 | 1, 2, 3 | tendoid 40775 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (𝑈‘( I ↾ 𝐵)) = ( I ↾ 𝐵)) |
| 5 | 4 | adantrr 717 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑈‘( I ↾ 𝐵)) = ( I ↾ 𝐵)) |
| 6 | 1, 2, 3 | tendoid 40775 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑉 ∈ 𝐸) → (𝑉‘( I ↾ 𝐵)) = ( I ↾ 𝐵)) |
| 7 | 6 | adantrl 716 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑉‘( I ↾ 𝐵)) = ( I ↾ 𝐵)) |
| 8 | 5, 7 | eqtr4d 2780 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑈‘( I ↾ 𝐵)) = (𝑉‘( I ↾ 𝐵))) |
| 9 | | fveq2 6906 |
. . . . . 6
⊢ (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑈‘( I ↾ 𝐵))) |
| 10 | | fveq2 6906 |
. . . . . 6
⊢ (𝑓 = ( I ↾ 𝐵) → (𝑉‘𝑓) = (𝑉‘( I ↾ 𝐵))) |
| 11 | 9, 10 | eqeq12d 2753 |
. . . . 5
⊢ (𝑓 = ( I ↾ 𝐵) → ((𝑈‘𝑓) = (𝑉‘𝑓) ↔ (𝑈‘( I ↾ 𝐵)) = (𝑉‘( I ↾ 𝐵)))) |
| 12 | 8, 11 | syl5ibrcom 247 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) |
| 13 | 12 | ralrimivw 3150 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → ∀𝑓 ∈ 𝑇 (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) |
| 14 | | r19.26 3111 |
. . . . 5
⊢
(∀𝑓 ∈
𝑇 ((𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) ↔ (∀𝑓 ∈ 𝑇 (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ ∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)))) |
| 15 | | jaob 964 |
. . . . . . 7
⊢ (((𝑓 = ( I ↾ 𝐵) ∨ 𝑓 ≠ ( I ↾ 𝐵)) → (𝑈‘𝑓) = (𝑉‘𝑓)) ↔ ((𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)))) |
| 16 | | exmidne 2950 |
. . . . . . . 8
⊢ (𝑓 = ( I ↾ 𝐵) ∨ 𝑓 ≠ ( I ↾ 𝐵)) |
| 17 | | pm5.5 361 |
. . . . . . . 8
⊢ ((𝑓 = ( I ↾ 𝐵) ∨ 𝑓 ≠ ( I ↾ 𝐵)) → (((𝑓 = ( I ↾ 𝐵) ∨ 𝑓 ≠ ( I ↾ 𝐵)) → (𝑈‘𝑓) = (𝑉‘𝑓)) ↔ (𝑈‘𝑓) = (𝑉‘𝑓))) |
| 18 | 16, 17 | ax-mp 5 |
. . . . . . 7
⊢ (((𝑓 = ( I ↾ 𝐵) ∨ 𝑓 ≠ ( I ↾ 𝐵)) → (𝑈‘𝑓) = (𝑉‘𝑓)) ↔ (𝑈‘𝑓) = (𝑉‘𝑓)) |
| 19 | 15, 18 | bitr3i 277 |
. . . . . 6
⊢ (((𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) ↔ (𝑈‘𝑓) = (𝑉‘𝑓)) |
| 20 | 19 | ralbii 3093 |
. . . . 5
⊢
(∀𝑓 ∈
𝑇 ((𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) ↔ ∀𝑓 ∈ 𝑇 (𝑈‘𝑓) = (𝑉‘𝑓)) |
| 21 | 14, 20 | bitr3i 277 |
. . . 4
⊢
((∀𝑓 ∈
𝑇 (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ ∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) ↔ ∀𝑓 ∈ 𝑇 (𝑈‘𝑓) = (𝑉‘𝑓)) |
| 22 | | tendoeq2.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 23 | 2, 22, 3 | tendoeq1 40766 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ∀𝑓 ∈ 𝑇 (𝑈‘𝑓) = (𝑉‘𝑓)) → 𝑈 = 𝑉) |
| 24 | 23 | 3expia 1122 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (∀𝑓 ∈ 𝑇 (𝑈‘𝑓) = (𝑉‘𝑓) → 𝑈 = 𝑉)) |
| 25 | 21, 24 | biimtrid 242 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → ((∀𝑓 ∈ 𝑇 (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ ∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) → 𝑈 = 𝑉)) |
| 26 | 13, 25 | mpand 695 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) → 𝑈 = 𝑉)) |
| 27 | 26 | 3impia 1118 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) → 𝑈 = 𝑉) |