Step | Hyp | Ref
| Expression |
1 | | ax-hv0cl 29084 |
. . 3
⊢
0ℎ ∈ ℋ |
2 | | nlelch.1 |
. . . . . . 7
⊢ 𝑇 ∈ LinFn |
3 | 2 | lnfnfi 30122 |
. . . . . 6
⊢ 𝑇:
ℋ⟶ℂ |
4 | | fveq2 6717 |
. . . . . . . . 9
⊢
((⊥‘(null‘𝑇)) = 0ℋ →
(⊥‘(⊥‘(null‘𝑇))) =
(⊥‘0ℋ)) |
5 | | nlelch.2 |
. . . . . . . . . . 11
⊢ 𝑇 ∈ ContFn |
6 | 2, 5 | nlelchi 30142 |
. . . . . . . . . 10
⊢
(null‘𝑇)
∈ Cℋ |
7 | 6 | ococi 29486 |
. . . . . . . . 9
⊢
(⊥‘(⊥‘(null‘𝑇))) = (null‘𝑇) |
8 | | choc0 29407 |
. . . . . . . . 9
⊢
(⊥‘0ℋ) = ℋ |
9 | 4, 7, 8 | 3eqtr3g 2801 |
. . . . . . . 8
⊢
((⊥‘(null‘𝑇)) = 0ℋ →
(null‘𝑇) =
ℋ) |
10 | 9 | eleq2d 2823 |
. . . . . . 7
⊢
((⊥‘(null‘𝑇)) = 0ℋ → (𝑣 ∈ (null‘𝑇) ↔ 𝑣 ∈ ℋ)) |
11 | 10 | biimpar 481 |
. . . . . 6
⊢
(((⊥‘(null‘𝑇)) = 0ℋ ∧ 𝑣 ∈ ℋ) → 𝑣 ∈ (null‘𝑇)) |
12 | | elnlfn2 30010 |
. . . . . 6
⊢ ((𝑇: ℋ⟶ℂ ∧
𝑣 ∈ (null‘𝑇)) → (𝑇‘𝑣) = 0) |
13 | 3, 11, 12 | sylancr 590 |
. . . . 5
⊢
(((⊥‘(null‘𝑇)) = 0ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘𝑣) = 0) |
14 | | hi02 29178 |
. . . . . 6
⊢ (𝑣 ∈ ℋ → (𝑣
·ih 0ℎ) = 0) |
15 | 14 | adantl 485 |
. . . . 5
⊢
(((⊥‘(null‘𝑇)) = 0ℋ ∧ 𝑣 ∈ ℋ) → (𝑣
·ih 0ℎ) = 0) |
16 | 13, 15 | eqtr4d 2780 |
. . . 4
⊢
(((⊥‘(null‘𝑇)) = 0ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘𝑣) = (𝑣 ·ih
0ℎ)) |
17 | 16 | ralrimiva 3105 |
. . 3
⊢
((⊥‘(null‘𝑇)) = 0ℋ →
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih
0ℎ)) |
18 | | oveq2 7221 |
. . . . . 6
⊢ (𝑤 = 0ℎ →
(𝑣
·ih 𝑤) = (𝑣 ·ih
0ℎ)) |
19 | 18 | eqeq2d 2748 |
. . . . 5
⊢ (𝑤 = 0ℎ →
((𝑇‘𝑣) = (𝑣 ·ih 𝑤) ↔ (𝑇‘𝑣) = (𝑣 ·ih
0ℎ))) |
20 | 19 | ralbidv 3118 |
. . . 4
⊢ (𝑤 = 0ℎ →
(∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤) ↔ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih
0ℎ))) |
21 | 20 | rspcev 3537 |
. . 3
⊢
((0ℎ ∈ ℋ ∧ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih
0ℎ)) → ∃𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
22 | 1, 17, 21 | sylancr 590 |
. 2
⊢
((⊥‘(null‘𝑇)) = 0ℋ → ∃𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
23 | 6 | choccli 29388 |
. . . 4
⊢
(⊥‘(null‘𝑇)) ∈
Cℋ |
24 | 23 | chne0i 29534 |
. . 3
⊢
((⊥‘(null‘𝑇)) ≠ 0ℋ ↔
∃𝑢 ∈
(⊥‘(null‘𝑇))𝑢 ≠ 0ℎ) |
25 | 23 | cheli 29313 |
. . . . 5
⊢ (𝑢 ∈
(⊥‘(null‘𝑇)) → 𝑢 ∈ ℋ) |
26 | 3 | ffvelrni 6903 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℋ → (𝑇‘𝑢) ∈ ℂ) |
27 | 26 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ (𝑇‘𝑢) ∈
ℂ) |
28 | | hicl 29161 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (𝑢
·ih 𝑢) ∈ ℂ) |
29 | 28 | anidms 570 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℋ → (𝑢
·ih 𝑢) ∈ ℂ) |
30 | 29 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ (𝑢
·ih 𝑢) ∈ ℂ) |
31 | | his6 29180 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℋ → ((𝑢
·ih 𝑢) = 0 ↔ 𝑢 = 0ℎ)) |
32 | 31 | necon3bid 2985 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℋ → ((𝑢
·ih 𝑢) ≠ 0 ↔ 𝑢 ≠ 0ℎ)) |
33 | 32 | biimpar 481 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ (𝑢
·ih 𝑢) ≠ 0) |
34 | 27, 30, 33 | divcld 11608 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ ((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) ∈
ℂ) |
35 | 34 | cjcld 14759 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ (∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢))) ∈
ℂ) |
36 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ 𝑢 ∈
ℋ) |
37 | | hvmulcl 29094 |
. . . . . . . . 9
⊢
(((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢))) ∈ ℂ ∧ 𝑢 ∈ ℋ) →
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) ∈ ℋ) |
38 | 35, 36, 37 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) ∈ ℋ) |
39 | 38 | adantll 714 |
. . . . . . 7
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) →
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) ∈ ℋ) |
40 | | hvmulcl 29094 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇‘𝑢) ∈ ℂ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) ·ℎ 𝑣) ∈
ℋ) |
41 | 26, 40 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) ·ℎ 𝑣) ∈
ℋ) |
42 | 3 | ffvelrni 6903 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ ℋ → (𝑇‘𝑣) ∈ ℂ) |
43 | | hvmulcl 29094 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ 𝑢 ∈ ℋ) → ((𝑇‘𝑣) ·ℎ 𝑢) ∈
ℋ) |
44 | 42, 43 | sylan 583 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → ((𝑇‘𝑣) ·ℎ 𝑢) ∈
ℋ) |
45 | 44 | ancoms 462 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑣) ·ℎ 𝑢) ∈
ℋ) |
46 | | simpl 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → 𝑢 ∈
ℋ) |
47 | | his2sub 29173 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑇‘𝑢) ·ℎ 𝑣) ∈ ℋ ∧ ((𝑇‘𝑣) ·ℎ 𝑢) ∈ ℋ ∧ 𝑢 ∈ ℋ) →
((((𝑇‘𝑢)
·ℎ 𝑣) −ℎ ((𝑇‘𝑣) ·ℎ 𝑢))
·ih 𝑢) = ((((𝑇‘𝑢) ·ℎ 𝑣)
·ih 𝑢) − (((𝑇‘𝑣) ·ℎ 𝑢)
·ih 𝑢))) |
48 | 41, 45, 46, 47 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) →
((((𝑇‘𝑢)
·ℎ 𝑣) −ℎ ((𝑇‘𝑣) ·ℎ 𝑢))
·ih 𝑢) = ((((𝑇‘𝑢) ·ℎ 𝑣)
·ih 𝑢) − (((𝑇‘𝑣) ·ℎ 𝑢)
·ih 𝑢))) |
49 | 26 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘𝑢) ∈ ℂ) |
50 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → 𝑣 ∈
ℋ) |
51 | | ax-his3 29165 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇‘𝑢) ∈ ℂ ∧ 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (((𝑇‘𝑢) ·ℎ 𝑣)
·ih 𝑢) = ((𝑇‘𝑢) · (𝑣 ·ih 𝑢))) |
52 | 49, 50, 46, 51 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) ·ℎ 𝑣)
·ih 𝑢) = ((𝑇‘𝑢) · (𝑣 ·ih 𝑢))) |
53 | 42 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘𝑣) ∈ ℂ) |
54 | | ax-his3 29165 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ 𝑢 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (((𝑇‘𝑣) ·ℎ 𝑢)
·ih 𝑢) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) |
55 | 53, 46, 46, 54 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑣) ·ℎ 𝑢)
·ih 𝑢) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) |
56 | 52, 55 | oveq12d 7231 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) →
((((𝑇‘𝑢)
·ℎ 𝑣) ·ih 𝑢) − (((𝑇‘𝑣) ·ℎ 𝑢)
·ih 𝑢)) = (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
57 | 48, 56 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) = ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢)) |
58 | 57 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) = ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢)) |
59 | | hvsubcl 29098 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑇‘𝑢) ·ℎ 𝑣) ∈ ℋ ∧ ((𝑇‘𝑣) ·ℎ 𝑢) ∈ ℋ) →
(((𝑇‘𝑢)
·ℎ 𝑣) −ℎ ((𝑇‘𝑣) ·ℎ 𝑢)) ∈
ℋ) |
60 | 41, 45, 59 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ ℋ) |
61 | 2 | lnfnsubi 30127 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑇‘𝑢) ·ℎ 𝑣) ∈ ℋ ∧ ((𝑇‘𝑣) ·ℎ 𝑢) ∈ ℋ) → (𝑇‘(((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢))) = ((𝑇‘((𝑇‘𝑢) ·ℎ 𝑣)) − (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)))) |
62 | 41, 45, 61 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘(((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢))) = ((𝑇‘((𝑇‘𝑢) ·ℎ 𝑣)) − (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)))) |
63 | 2 | lnfnmuli 30125 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑇‘𝑢) ∈ ℂ ∧ 𝑣 ∈ ℋ) → (𝑇‘((𝑇‘𝑢) ·ℎ 𝑣)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
64 | 26, 63 | sylan 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘((𝑇‘𝑢) ·ℎ 𝑣)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
65 | 2 | lnfnmuli 30125 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ 𝑢 ∈ ℋ) → (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)) = ((𝑇‘𝑣) · (𝑇‘𝑢))) |
66 | | mulcom 10815 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ (𝑇‘𝑢) ∈ ℂ) → ((𝑇‘𝑣) · (𝑇‘𝑢)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
67 | 26, 66 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ 𝑢 ∈ ℋ) → ((𝑇‘𝑣) · (𝑇‘𝑢)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
68 | 65, 67 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ 𝑢 ∈ ℋ) → (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
69 | 42, 68 | sylan 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
70 | 69 | ancoms 462 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
71 | 64, 70 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘((𝑇‘𝑢) ·ℎ 𝑣)) − (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢))) = (((𝑇‘𝑢) · (𝑇‘𝑣)) − ((𝑇‘𝑢) · (𝑇‘𝑣)))) |
72 | | mulcl 10813 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑇‘𝑢) ∈ ℂ ∧ (𝑇‘𝑣) ∈ ℂ) → ((𝑇‘𝑢) · (𝑇‘𝑣)) ∈ ℂ) |
73 | 26, 42, 72 | syl2an 599 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) · (𝑇‘𝑣)) ∈ ℂ) |
74 | 73 | subidd 11177 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑇‘𝑣)) − ((𝑇‘𝑢) · (𝑇‘𝑣))) = 0) |
75 | 62, 71, 74 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘(((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢))) = 0) |
76 | | elnlfn 30009 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇: ℋ⟶ℂ →
((((𝑇‘𝑢)
·ℎ 𝑣) −ℎ ((𝑇‘𝑣) ·ℎ 𝑢)) ∈ (null‘𝑇) ↔ ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ ℋ ∧ (𝑇‘(((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢))) = 0))) |
77 | 3, 76 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ (null‘𝑇) ↔ ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ ℋ ∧ (𝑇‘(((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢))) = 0)) |
78 | 60, 75, 77 | sylanbrc 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ (null‘𝑇)) |
79 | 6 | chssii 29312 |
. . . . . . . . . . . . . . . . 17
⊢
(null‘𝑇)
⊆ ℋ |
80 | | ocorth 29372 |
. . . . . . . . . . . . . . . . 17
⊢
((null‘𝑇)
⊆ ℋ → (((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ (null‘𝑇) ∧ 𝑢 ∈ (⊥‘(null‘𝑇))) → ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢) = 0)) |
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑇‘𝑢)
·ℎ 𝑣) −ℎ ((𝑇‘𝑣) ·ℎ 𝑢)) ∈ (null‘𝑇) ∧ 𝑢 ∈ (⊥‘(null‘𝑇))) → ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢) = 0) |
82 | 78, 81 | sylan 583 |
. . . . . . . . . . . . . . 15
⊢ (((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) ∧ 𝑢 ∈
(⊥‘(null‘𝑇))) → ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢) = 0) |
83 | 82 | ancoms 462 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ (𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ)) → ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢) = 0) |
84 | 83 | anassrs 471 |
. . . . . . . . . . . . 13
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑣 ∈ ℋ) → ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢) = 0) |
85 | 58, 84 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) = 0) |
86 | | hicl 29161 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (𝑣
·ih 𝑢) ∈ ℂ) |
87 | 86 | ancoms 462 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑣
·ih 𝑢) ∈ ℂ) |
88 | 49, 87 | mulcld 10853 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) ∈
ℂ) |
89 | | mulcl 10813 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ (𝑢 ·ih 𝑢) ∈ ℂ) → ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)) ∈
ℂ) |
90 | 42, 29, 89 | syl2anr 600 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)) ∈
ℂ) |
91 | 88, 90 | subeq0ad 11199 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) →
((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) = 0 ↔ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
92 | 91 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑣 ∈ ℋ) → ((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) = 0 ↔ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
93 | 85, 92 | mpbid 235 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) |
94 | 93 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) |
95 | 88 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) ∈
ℂ) |
96 | 42 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (𝑇‘𝑣) ∈
ℂ) |
97 | 30, 33 | jca 515 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ ((𝑢
·ih 𝑢) ∈ ℂ ∧ (𝑢 ·ih 𝑢) ≠ 0)) |
98 | 97 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ ((𝑢
·ih 𝑢) ∈ ℂ ∧ (𝑢 ·ih 𝑢) ≠ 0)) |
99 | | divmul3 11495 |
. . . . . . . . . . . 12
⊢ ((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) ∈ ℂ ∧ (𝑇‘𝑣) ∈ ℂ ∧ ((𝑢 ·ih 𝑢) ∈ ℂ ∧ (𝑢
·ih 𝑢) ≠ 0)) → ((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑇‘𝑣) ↔ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
100 | 95, 96, 98, 99 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ ((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑇‘𝑣) ↔ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
101 | 100 | adantlll 718 |
. . . . . . . . . 10
⊢ ((((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) ∧ 𝑣 ∈ ℋ) →
((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑇‘𝑣) ↔ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
102 | 94, 101 | mpbird 260 |
. . . . . . . . 9
⊢ ((((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑇‘𝑣)) |
103 | 27 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (𝑇‘𝑢) ∈
ℂ) |
104 | 87 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (𝑣
·ih 𝑢) ∈ ℂ) |
105 | | div23 11509 |
. . . . . . . . . . . 12
⊢ (((𝑇‘𝑢) ∈ ℂ ∧ (𝑣 ·ih 𝑢) ∈ ℂ ∧ ((𝑢
·ih 𝑢) ∈ ℂ ∧ (𝑢 ·ih 𝑢) ≠ 0)) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) · (𝑣 ·ih 𝑢))) |
106 | 103, 104,
98, 105 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) · (𝑣 ·ih 𝑢))) |
107 | 34 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ ((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) ∈
ℂ) |
108 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ 𝑣 ∈
ℋ) |
109 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ 𝑢 ∈
ℋ) |
110 | | his52 29168 |
. . . . . . . . . . . 12
⊢ ((((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) ∈ ℂ ∧ 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (𝑣
·ih ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢)) = (((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) · (𝑣 ·ih 𝑢))) |
111 | 107, 108,
109, 110 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (𝑣
·ih ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢)) = (((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) · (𝑣 ·ih 𝑢))) |
112 | 106, 111 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) |
113 | 112 | adantlll 718 |
. . . . . . . . 9
⊢ ((((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) |
114 | 102, 113 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) ∧ 𝑣 ∈ ℋ) → (𝑇‘𝑣) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) |
115 | 114 | ralrimiva 3105 |
. . . . . . 7
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) →
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) |
116 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑤 = ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) → (𝑣 ·ih 𝑤) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) |
117 | 116 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑤 = ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) → ((𝑇‘𝑣) = (𝑣 ·ih 𝑤) ↔ (𝑇‘𝑣) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢)))) |
118 | 117 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝑤 = ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) → (∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤) ↔ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢)))) |
119 | 118 | rspcev 3537 |
. . . . . . 7
⊢
((((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) ∈ ℋ ∧ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) → ∃𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
120 | 39, 115, 119 | syl2anc 587 |
. . . . . 6
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) →
∃𝑤 ∈ ℋ
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
121 | 120 | ex 416 |
. . . . 5
⊢ ((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) → (𝑢 ≠ 0ℎ →
∃𝑤 ∈ ℋ
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤))) |
122 | 25, 121 | mpdan 687 |
. . . 4
⊢ (𝑢 ∈
(⊥‘(null‘𝑇)) → (𝑢 ≠ 0ℎ →
∃𝑤 ∈ ℋ
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤))) |
123 | 122 | rexlimiv 3199 |
. . 3
⊢
(∃𝑢 ∈
(⊥‘(null‘𝑇))𝑢 ≠ 0ℎ →
∃𝑤 ∈ ℋ
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
124 | 24, 123 | sylbi 220 |
. 2
⊢
((⊥‘(null‘𝑇)) ≠ 0ℋ →
∃𝑤 ∈ ℋ
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
125 | 22, 124 | pm2.61ine 3025 |
1
⊢
∃𝑤 ∈
ℋ ∀𝑣 ∈
ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤) |