Step | Hyp | Ref
| Expression |
1 | | ax-hv0cl 27244 |
. . 3
⊢
0ℎ ∈ ℋ |
2 | | nlelch.1 |
. . . . . . 7
⊢ 𝑇 ∈ LinFn |
3 | 2 | lnfnfi 28284 |
. . . . . 6
⊢ 𝑇:
ℋ⟶ℂ |
4 | | fveq2 6103 |
. . . . . . . . 9
⊢
((⊥‘(null‘𝑇)) = 0ℋ →
(⊥‘(⊥‘(null‘𝑇))) =
(⊥‘0ℋ)) |
5 | | nlelch.2 |
. . . . . . . . . . 11
⊢ 𝑇 ∈ ConFn |
6 | 2, 5 | nlelchi 28304 |
. . . . . . . . . 10
⊢
(null‘𝑇)
∈ Cℋ |
7 | 6 | ococi 27648 |
. . . . . . . . 9
⊢
(⊥‘(⊥‘(null‘𝑇))) = (null‘𝑇) |
8 | | choc0 27569 |
. . . . . . . . 9
⊢
(⊥‘0ℋ) = ℋ |
9 | 4, 7, 8 | 3eqtr3g 2667 |
. . . . . . . 8
⊢
((⊥‘(null‘𝑇)) = 0ℋ →
(null‘𝑇) =
ℋ) |
10 | 9 | eleq2d 2673 |
. . . . . . 7
⊢
((⊥‘(null‘𝑇)) = 0ℋ → (𝑣 ∈ (null‘𝑇) ↔ 𝑣 ∈ ℋ)) |
11 | 10 | biimpar 501 |
. . . . . 6
⊢
(((⊥‘(null‘𝑇)) = 0ℋ ∧ 𝑣 ∈ ℋ) → 𝑣 ∈ (null‘𝑇)) |
12 | | elnlfn2 28172 |
. . . . . 6
⊢ ((𝑇: ℋ⟶ℂ ∧
𝑣 ∈ (null‘𝑇)) → (𝑇‘𝑣) = 0) |
13 | 3, 11, 12 | sylancr 694 |
. . . . 5
⊢
(((⊥‘(null‘𝑇)) = 0ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘𝑣) = 0) |
14 | | hi02 27338 |
. . . . . 6
⊢ (𝑣 ∈ ℋ → (𝑣
·ih 0ℎ) = 0) |
15 | 14 | adantl 481 |
. . . . 5
⊢
(((⊥‘(null‘𝑇)) = 0ℋ ∧ 𝑣 ∈ ℋ) → (𝑣
·ih 0ℎ) = 0) |
16 | 13, 15 | eqtr4d 2647 |
. . . 4
⊢
(((⊥‘(null‘𝑇)) = 0ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘𝑣) = (𝑣 ·ih
0ℎ)) |
17 | 16 | ralrimiva 2949 |
. . 3
⊢
((⊥‘(null‘𝑇)) = 0ℋ →
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih
0ℎ)) |
18 | | oveq2 6557 |
. . . . . 6
⊢ (𝑤 = 0ℎ →
(𝑣
·ih 𝑤) = (𝑣 ·ih
0ℎ)) |
19 | 18 | eqeq2d 2620 |
. . . . 5
⊢ (𝑤 = 0ℎ →
((𝑇‘𝑣) = (𝑣 ·ih 𝑤) ↔ (𝑇‘𝑣) = (𝑣 ·ih
0ℎ))) |
20 | 19 | ralbidv 2969 |
. . . 4
⊢ (𝑤 = 0ℎ →
(∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤) ↔ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih
0ℎ))) |
21 | 20 | rspcev 3282 |
. . 3
⊢
((0ℎ ∈ ℋ ∧ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih
0ℎ)) → ∃𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
22 | 1, 17, 21 | sylancr 694 |
. 2
⊢
((⊥‘(null‘𝑇)) = 0ℋ → ∃𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
23 | 6 | choccli 27550 |
. . . 4
⊢
(⊥‘(null‘𝑇)) ∈
Cℋ |
24 | 23 | chne0i 27696 |
. . 3
⊢
((⊥‘(null‘𝑇)) ≠ 0ℋ ↔
∃𝑢 ∈
(⊥‘(null‘𝑇))𝑢 ≠ 0ℎ) |
25 | 23 | cheli 27473 |
. . . . 5
⊢ (𝑢 ∈
(⊥‘(null‘𝑇)) → 𝑢 ∈ ℋ) |
26 | 3 | ffvelrni 6266 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℋ → (𝑇‘𝑢) ∈ ℂ) |
27 | 26 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ (𝑇‘𝑢) ∈
ℂ) |
28 | | hicl 27321 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (𝑢
·ih 𝑢) ∈ ℂ) |
29 | 28 | anidms 675 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℋ → (𝑢
·ih 𝑢) ∈ ℂ) |
30 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ (𝑢
·ih 𝑢) ∈ ℂ) |
31 | | his6 27340 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℋ → ((𝑢
·ih 𝑢) = 0 ↔ 𝑢 = 0ℎ)) |
32 | 31 | necon3bid 2826 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ ℋ → ((𝑢
·ih 𝑢) ≠ 0 ↔ 𝑢 ≠ 0ℎ)) |
33 | 32 | biimpar 501 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ (𝑢
·ih 𝑢) ≠ 0) |
34 | 27, 30, 33 | divcld 10680 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ ((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) ∈
ℂ) |
35 | 34 | cjcld 13784 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ (∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢))) ∈
ℂ) |
36 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ 𝑢 ∈
ℋ) |
37 | | hvmulcl 27254 |
. . . . . . . . 9
⊢
(((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢))) ∈ ℂ ∧ 𝑢 ∈ ℋ) →
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) ∈ ℋ) |
38 | 35, 36, 37 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) ∈ ℋ) |
39 | 38 | adantll 746 |
. . . . . . 7
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) →
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) ∈ ℋ) |
40 | | hvmulcl 27254 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇‘𝑢) ∈ ℂ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) ·ℎ 𝑣) ∈
ℋ) |
41 | 26, 40 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) ·ℎ 𝑣) ∈
ℋ) |
42 | 3 | ffvelrni 6266 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ ℋ → (𝑇‘𝑣) ∈ ℂ) |
43 | | hvmulcl 27254 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ 𝑢 ∈ ℋ) → ((𝑇‘𝑣) ·ℎ 𝑢) ∈
ℋ) |
44 | 42, 43 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → ((𝑇‘𝑣) ·ℎ 𝑢) ∈
ℋ) |
45 | 44 | ancoms 468 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑣) ·ℎ 𝑢) ∈
ℋ) |
46 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → 𝑢 ∈
ℋ) |
47 | | his2sub 27333 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑇‘𝑢) ·ℎ 𝑣) ∈ ℋ ∧ ((𝑇‘𝑣) ·ℎ 𝑢) ∈ ℋ ∧ 𝑢 ∈ ℋ) →
((((𝑇‘𝑢)
·ℎ 𝑣) −ℎ ((𝑇‘𝑣) ·ℎ 𝑢))
·ih 𝑢) = ((((𝑇‘𝑢) ·ℎ 𝑣)
·ih 𝑢) − (((𝑇‘𝑣) ·ℎ 𝑢)
·ih 𝑢))) |
48 | 41, 45, 46, 47 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) →
((((𝑇‘𝑢)
·ℎ 𝑣) −ℎ ((𝑇‘𝑣) ·ℎ 𝑢))
·ih 𝑢) = ((((𝑇‘𝑢) ·ℎ 𝑣)
·ih 𝑢) − (((𝑇‘𝑣) ·ℎ 𝑢)
·ih 𝑢))) |
49 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘𝑢) ∈ ℂ) |
50 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → 𝑣 ∈
ℋ) |
51 | | ax-his3 27325 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇‘𝑢) ∈ ℂ ∧ 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (((𝑇‘𝑢) ·ℎ 𝑣)
·ih 𝑢) = ((𝑇‘𝑢) · (𝑣 ·ih 𝑢))) |
52 | 49, 50, 46, 51 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) ·ℎ 𝑣)
·ih 𝑢) = ((𝑇‘𝑢) · (𝑣 ·ih 𝑢))) |
53 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘𝑣) ∈ ℂ) |
54 | | ax-his3 27325 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ 𝑢 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (((𝑇‘𝑣) ·ℎ 𝑢)
·ih 𝑢) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) |
55 | 53, 46, 46, 54 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑣) ·ℎ 𝑢)
·ih 𝑢) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) |
56 | 52, 55 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) →
((((𝑇‘𝑢)
·ℎ 𝑣) ·ih 𝑢) − (((𝑇‘𝑣) ·ℎ 𝑢)
·ih 𝑢)) = (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
57 | 48, 56 | eqtr2d 2645 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) = ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢)) |
58 | 57 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) = ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢)) |
59 | | hvsubcl 27258 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑇‘𝑢) ·ℎ 𝑣) ∈ ℋ ∧ ((𝑇‘𝑣) ·ℎ 𝑢) ∈ ℋ) →
(((𝑇‘𝑢)
·ℎ 𝑣) −ℎ ((𝑇‘𝑣) ·ℎ 𝑢)) ∈
ℋ) |
60 | 41, 45, 59 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ ℋ) |
61 | 2 | lnfnsubi 28289 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑇‘𝑢) ·ℎ 𝑣) ∈ ℋ ∧ ((𝑇‘𝑣) ·ℎ 𝑢) ∈ ℋ) → (𝑇‘(((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢))) = ((𝑇‘((𝑇‘𝑢) ·ℎ 𝑣)) − (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)))) |
62 | 41, 45, 61 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘(((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢))) = ((𝑇‘((𝑇‘𝑢) ·ℎ 𝑣)) − (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)))) |
63 | 2 | lnfnmuli 28287 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑇‘𝑢) ∈ ℂ ∧ 𝑣 ∈ ℋ) → (𝑇‘((𝑇‘𝑢) ·ℎ 𝑣)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
64 | 26, 63 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘((𝑇‘𝑢) ·ℎ 𝑣)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
65 | 2 | lnfnmuli 28287 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ 𝑢 ∈ ℋ) → (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)) = ((𝑇‘𝑣) · (𝑇‘𝑢))) |
66 | | mulcom 9901 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ (𝑇‘𝑢) ∈ ℂ) → ((𝑇‘𝑣) · (𝑇‘𝑢)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
67 | 26, 66 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ 𝑢 ∈ ℋ) → ((𝑇‘𝑣) · (𝑇‘𝑢)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
68 | 65, 67 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ 𝑢 ∈ ℋ) → (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
69 | 42, 68 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
70 | 69 | ancoms 468 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢)) = ((𝑇‘𝑢) · (𝑇‘𝑣))) |
71 | 64, 70 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘((𝑇‘𝑢) ·ℎ 𝑣)) − (𝑇‘((𝑇‘𝑣) ·ℎ 𝑢))) = (((𝑇‘𝑢) · (𝑇‘𝑣)) − ((𝑇‘𝑢) · (𝑇‘𝑣)))) |
72 | | mulcl 9899 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑇‘𝑢) ∈ ℂ ∧ (𝑇‘𝑣) ∈ ℂ) → ((𝑇‘𝑢) · (𝑇‘𝑣)) ∈ ℂ) |
73 | 26, 42, 72 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) · (𝑇‘𝑣)) ∈ ℂ) |
74 | 73 | subidd 10259 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑇‘𝑣)) − ((𝑇‘𝑢) · (𝑇‘𝑣))) = 0) |
75 | 62, 71, 74 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑇‘(((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢))) = 0) |
76 | | elnlfn 28171 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇: ℋ⟶ℂ →
((((𝑇‘𝑢)
·ℎ 𝑣) −ℎ ((𝑇‘𝑣) ·ℎ 𝑢)) ∈ (null‘𝑇) ↔ ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ ℋ ∧ (𝑇‘(((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢))) = 0))) |
77 | 3, 76 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ (null‘𝑇) ↔ ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ ℋ ∧ (𝑇‘(((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢))) = 0)) |
78 | 60, 75, 77 | sylanbrc 695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ (null‘𝑇)) |
79 | 6 | chssii 27472 |
. . . . . . . . . . . . . . . . 17
⊢
(null‘𝑇)
⊆ ℋ |
80 | | ocorth 27534 |
. . . . . . . . . . . . . . . . 17
⊢
((null‘𝑇)
⊆ ℋ → (((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ∈ (null‘𝑇) ∧ 𝑢 ∈ (⊥‘(null‘𝑇))) → ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢) = 0)) |
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑇‘𝑢)
·ℎ 𝑣) −ℎ ((𝑇‘𝑣) ·ℎ 𝑢)) ∈ (null‘𝑇) ∧ 𝑢 ∈ (⊥‘(null‘𝑇))) → ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢) = 0) |
82 | 78, 81 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) ∧ 𝑢 ∈
(⊥‘(null‘𝑇))) → ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢) = 0) |
83 | 82 | ancoms 468 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ (𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ)) → ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢) = 0) |
84 | 83 | anassrs 678 |
. . . . . . . . . . . . 13
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑣 ∈ ℋ) → ((((𝑇‘𝑢) ·ℎ 𝑣) −ℎ
((𝑇‘𝑣)
·ℎ 𝑢)) ·ih 𝑢) = 0) |
85 | 58, 84 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) = 0) |
86 | | hicl 27321 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (𝑣
·ih 𝑢) ∈ ℂ) |
87 | 86 | ancoms 468 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → (𝑣
·ih 𝑢) ∈ ℂ) |
88 | 49, 87 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) ∈
ℂ) |
89 | | mulcl 9899 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇‘𝑣) ∈ ℂ ∧ (𝑢 ·ih 𝑢) ∈ ℂ) → ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)) ∈
ℂ) |
90 | 42, 29, 89 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)) ∈
ℂ) |
91 | 88, 90 | subeq0ad 10281 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ) →
((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) = 0 ↔ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
92 | 91 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑣 ∈ ℋ) → ((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) − ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) = 0 ↔ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
93 | 85, 92 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) |
94 | 93 | adantlr 747 |
. . . . . . . . . 10
⊢ ((((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) ∧ 𝑣 ∈ ℋ) → ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢))) |
95 | 88 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) ∈
ℂ) |
96 | 42 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (𝑇‘𝑣) ∈
ℂ) |
97 | 30, 33 | jca 553 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
→ ((𝑢
·ih 𝑢) ∈ ℂ ∧ (𝑢 ·ih 𝑢) ≠ 0)) |
98 | 97 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ ((𝑢
·ih 𝑢) ∈ ℂ ∧ (𝑢 ·ih 𝑢) ≠ 0)) |
99 | | divmul3 10569 |
. . . . . . . . . . . 12
⊢ ((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) ∈ ℂ ∧ (𝑇‘𝑣) ∈ ℂ ∧ ((𝑢 ·ih 𝑢) ∈ ℂ ∧ (𝑢
·ih 𝑢) ≠ 0)) → ((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑇‘𝑣) ↔ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
100 | 95, 96, 98, 99 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ ((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑇‘𝑣) ↔ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
101 | 100 | adantlll 750 |
. . . . . . . . . 10
⊢ ((((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) ∧ 𝑣 ∈ ℋ) →
((((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑇‘𝑣) ↔ ((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) = ((𝑇‘𝑣) · (𝑢 ·ih 𝑢)))) |
102 | 94, 101 | mpbird 246 |
. . . . . . . . 9
⊢ ((((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑇‘𝑣)) |
103 | 27 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (𝑇‘𝑢) ∈
ℂ) |
104 | 87 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (𝑣
·ih 𝑢) ∈ ℂ) |
105 | | div23 10583 |
. . . . . . . . . . . 12
⊢ (((𝑇‘𝑢) ∈ ℂ ∧ (𝑣 ·ih 𝑢) ∈ ℂ ∧ ((𝑢
·ih 𝑢) ∈ ℂ ∧ (𝑢 ·ih 𝑢) ≠ 0)) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) · (𝑣 ·ih 𝑢))) |
106 | 103, 104,
98, 105 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) · (𝑣 ·ih 𝑢))) |
107 | 34 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ ((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) ∈
ℂ) |
108 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ 𝑣 ∈
ℋ) |
109 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ 𝑢 ∈
ℋ) |
110 | | his52 27328 |
. . . . . . . . . . . 12
⊢ ((((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) ∈ ℂ ∧ 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (𝑣
·ih ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢)) = (((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) · (𝑣 ·ih 𝑢))) |
111 | 107, 108,
109, 110 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (𝑣
·ih ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢)) = (((𝑇‘𝑢) / (𝑢 ·ih 𝑢)) · (𝑣 ·ih 𝑢))) |
112 | 106, 111 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ (((𝑢 ∈ ℋ ∧ 𝑢 ≠ 0ℎ)
∧ 𝑣 ∈ ℋ)
→ (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) |
113 | 112 | adantlll 750 |
. . . . . . . . 9
⊢ ((((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) ∧ 𝑣 ∈ ℋ) → (((𝑇‘𝑢) · (𝑣 ·ih 𝑢)) / (𝑢 ·ih 𝑢)) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) |
114 | 102, 113 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) ∧ 𝑣 ∈ ℋ) → (𝑇‘𝑣) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) |
115 | 114 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) →
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) |
116 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑤 = ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) → (𝑣 ·ih 𝑤) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) |
117 | 116 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑤 = ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) → ((𝑇‘𝑣) = (𝑣 ·ih 𝑤) ↔ (𝑇‘𝑣) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢)))) |
118 | 117 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑤 = ((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) → (∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤) ↔ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢)))) |
119 | 118 | rspcev 3282 |
. . . . . . 7
⊢
((((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢) ∈ ℋ ∧ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih
((∗‘((𝑇‘𝑢) / (𝑢 ·ih 𝑢)))
·ℎ 𝑢))) → ∃𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
120 | 39, 115, 119 | syl2anc 691 |
. . . . . 6
⊢ (((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) ∧ 𝑢 ≠ 0ℎ) →
∃𝑤 ∈ ℋ
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
121 | 120 | ex 449 |
. . . . 5
⊢ ((𝑢 ∈
(⊥‘(null‘𝑇)) ∧ 𝑢 ∈ ℋ) → (𝑢 ≠ 0ℎ →
∃𝑤 ∈ ℋ
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤))) |
122 | 25, 121 | mpdan 699 |
. . . 4
⊢ (𝑢 ∈
(⊥‘(null‘𝑇)) → (𝑢 ≠ 0ℎ →
∃𝑤 ∈ ℋ
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤))) |
123 | 122 | rexlimiv 3009 |
. . 3
⊢
(∃𝑢 ∈
(⊥‘(null‘𝑇))𝑢 ≠ 0ℎ →
∃𝑤 ∈ ℋ
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
124 | 24, 123 | sylbi 206 |
. 2
⊢
((⊥‘(null‘𝑇)) ≠ 0ℋ →
∃𝑤 ∈ ℋ
∀𝑣 ∈ ℋ
(𝑇‘𝑣) = (𝑣 ·ih 𝑤)) |
125 | 22, 124 | pm2.61ine 2865 |
1
⊢
∃𝑤 ∈
ℋ ∀𝑣 ∈
ℋ (𝑇‘𝑣) = (𝑣 ·ih 𝑤) |