Step | Hyp | Ref
| Expression |
1 | | dvalvec.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | dvalveclem.t |
. . . . 5
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
3 | | dvalvec.v |
. . . . 5
⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) |
4 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑈) =
(Base‘𝑈) |
5 | 1, 2, 3, 4 | dvavbase 38639 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝑈) = 𝑇) |
6 | 5 | eqcomd 2744 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑇 = (Base‘𝑈)) |
7 | | dvalveclem.a |
. . . 4
⊢ + =
(+g‘𝑈) |
8 | 7 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → + =
(+g‘𝑈)) |
9 | | dvalveclem.d |
. . . 4
⊢ 𝐷 = (Scalar‘𝑈) |
10 | 9 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 = (Scalar‘𝑈)) |
11 | | dvalveclem.s |
. . . 4
⊢ · = (
·𝑠 ‘𝑈) |
12 | 11 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → · = (
·𝑠 ‘𝑈)) |
13 | | dvalveclem.e |
. . . . 5
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
14 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) |
15 | 1, 13, 3, 9, 14 | dvabase 38633 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝐷) = 𝐸) |
16 | 15 | eqcomd 2744 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐸 = (Base‘𝐷)) |
17 | | dvalveclem.p |
. . . 4
⊢ ⨣ =
(+g‘𝐷) |
18 | 17 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ⨣ =
(+g‘𝐷)) |
19 | | dvalveclem.m |
. . . 4
⊢ × =
(.r‘𝐷) |
20 | 19 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → × =
(.r‘𝐷)) |
21 | 1, 2, 13 | tendoidcl 38395 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ 𝐸) |
22 | 21, 16 | eleqtrd 2835 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ (Base‘𝐷)) |
23 | | dvalveclem.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐾) |
24 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
25 | 23, 1, 2, 13, 24 | tendo1ne0 38454 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ≠ (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))) |
26 | | eqid 2738 |
. . . . . . . . . 10
⊢
((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊) |
27 | 1, 26, 3, 9 | dvasca 38632 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 = ((EDRing‘𝐾)‘𝑊)) |
28 | 27 | fveq2d 6672 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (0g‘𝐷) =
(0g‘((EDRing‘𝐾)‘𝑊))) |
29 | | eqid 2738 |
. . . . . . . . 9
⊢
(0g‘((EDRing‘𝐾)‘𝑊)) =
(0g‘((EDRing‘𝐾)‘𝑊)) |
30 | 23, 1, 2, 26, 24, 29 | erng0g 38620 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) →
(0g‘((EDRing‘𝐾)‘𝑊)) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))) |
31 | 28, 30 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (0g‘𝐷) = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))) |
32 | 25, 31 | neeqtrrd 3008 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ≠ (0g‘𝐷)) |
33 | 21, 21 | jca 515 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (( I ↾ 𝑇) ∈ 𝐸 ∧ ( I ↾ 𝑇) ∈ 𝐸)) |
34 | 1, 2, 13, 3, 9, 19 | dvamulr 38638 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (( I ↾ 𝑇) ∈ 𝐸 ∧ ( I ↾ 𝑇) ∈ 𝐸)) → (( I ↾ 𝑇) × ( I ↾ 𝑇)) = (( I ↾ 𝑇) ∘ ( I ↾ 𝑇))) |
35 | 33, 34 | mpdan 687 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (( I ↾ 𝑇) × ( I ↾ 𝑇)) = (( I ↾ 𝑇) ∘ ( I ↾ 𝑇))) |
36 | | f1oi 6649 |
. . . . . . . 8
⊢ ( I
↾ 𝑇):𝑇–1-1-onto→𝑇 |
37 | | f1of 6612 |
. . . . . . . 8
⊢ (( I
↾ 𝑇):𝑇–1-1-onto→𝑇 → ( I ↾ 𝑇):𝑇⟶𝑇) |
38 | | fcoi2 6547 |
. . . . . . . 8
⊢ (( I
↾ 𝑇):𝑇⟶𝑇 → (( I ↾ 𝑇) ∘ ( I ↾ 𝑇)) = ( I ↾ 𝑇)) |
39 | 36, 37, 38 | mp2b 10 |
. . . . . . 7
⊢ (( I
↾ 𝑇) ∘ ( I
↾ 𝑇)) = ( I ↾
𝑇) |
40 | 35, 39 | eqtrdi 2789 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (( I ↾ 𝑇) × ( I ↾ 𝑇)) = ( I ↾ 𝑇)) |
41 | 22, 32, 40 | 3jca 1129 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (( I ↾ 𝑇) ∈ (Base‘𝐷) ∧ ( I ↾ 𝑇) ≠ (0g‘𝐷) ∧ (( I ↾ 𝑇) × ( I ↾ 𝑇)) = ( I ↾ 𝑇))) |
42 | 1, 26 | erngdv 38619 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ DivRing) |
43 | 27, 42 | eqeltrd 2833 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ DivRing) |
44 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘𝐷) = (0g‘𝐷) |
45 | | eqid 2738 |
. . . . . . 7
⊢
(1r‘𝐷) = (1r‘𝐷) |
46 | 14, 19, 44, 45 | drngid2 19630 |
. . . . . 6
⊢ (𝐷 ∈ DivRing → ((( I
↾ 𝑇) ∈
(Base‘𝐷) ∧ ( I
↾ 𝑇) ≠
(0g‘𝐷)
∧ (( I ↾ 𝑇) × ( I
↾ 𝑇)) = ( I ↾
𝑇)) ↔
(1r‘𝐷) = (
I ↾ 𝑇))) |
47 | 43, 46 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((( I ↾ 𝑇) ∈ (Base‘𝐷) ∧ ( I ↾ 𝑇) ≠ (0g‘𝐷) ∧ (( I ↾ 𝑇) × ( I ↾ 𝑇)) = ( I ↾ 𝑇)) ↔
(1r‘𝐷) = (
I ↾ 𝑇))) |
48 | 41, 47 | mpbid 235 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (1r‘𝐷) = ( I ↾ 𝑇)) |
49 | 48 | eqcomd 2744 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) = (1r‘𝐷)) |
50 | | drngring 19621 |
. . . 4
⊢ (𝐷 ∈ DivRing → 𝐷 ∈ Ring) |
51 | 43, 50 | syl 17 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ Ring) |
52 | 1, 3 | dvaabl 38650 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ Abel) |
53 | | ablgrp 19022 |
. . . 4
⊢ (𝑈 ∈ Abel → 𝑈 ∈ Grp) |
54 | 52, 53 | syl 17 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ Grp) |
55 | 1, 2, 13, 3, 11 | dvavsca 38643 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇)) → (𝑠 · 𝑡) = (𝑠‘𝑡)) |
56 | 55 | 3impb 1116 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇) → (𝑠 · 𝑡) = (𝑠‘𝑡)) |
57 | 1, 2, 13 | tendocl 38393 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇) → (𝑠‘𝑡) ∈ 𝑇) |
58 | 56, 57 | eqeltrd 2833 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇) → (𝑠 · 𝑡) ∈ 𝑇) |
59 | 1, 2, 13 | tendospdi1 38646 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑠‘(𝑡 ∘ 𝑓)) = ((𝑠‘𝑡) ∘ (𝑠‘𝑓))) |
60 | | simpr1 1195 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → 𝑠 ∈ 𝐸) |
61 | 1, 2 | ltrnco 38345 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇) → (𝑡 ∘ 𝑓) ∈ 𝑇) |
62 | 61 | 3adant3r1 1183 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑡 ∘ 𝑓) ∈ 𝑇) |
63 | 60, 62 | jca 515 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑠 ∈ 𝐸 ∧ (𝑡 ∘ 𝑓) ∈ 𝑇)) |
64 | 1, 2, 13, 3, 11 | dvavsca 38643 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (𝑡 ∘ 𝑓) ∈ 𝑇)) → (𝑠 · (𝑡 ∘ 𝑓)) = (𝑠‘(𝑡 ∘ 𝑓))) |
65 | 63, 64 | syldan 594 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑠 · (𝑡 ∘ 𝑓)) = (𝑠‘(𝑡 ∘ 𝑓))) |
66 | 57 | 3adant3r3 1185 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑠‘𝑡) ∈ 𝑇) |
67 | 1, 2, 13 | tendocl 38393 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇) → (𝑠‘𝑓) ∈ 𝑇) |
68 | 67 | 3adant3r2 1184 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑠‘𝑓) ∈ 𝑇) |
69 | 66, 68 | jca 515 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → ((𝑠‘𝑡) ∈ 𝑇 ∧ (𝑠‘𝑓) ∈ 𝑇)) |
70 | 1, 2, 3, 7 | dvavadd 38641 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠‘𝑡) ∈ 𝑇 ∧ (𝑠‘𝑓) ∈ 𝑇)) → ((𝑠‘𝑡) + (𝑠‘𝑓)) = ((𝑠‘𝑡) ∘ (𝑠‘𝑓))) |
71 | 69, 70 | syldan 594 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → ((𝑠‘𝑡) + (𝑠‘𝑓)) = ((𝑠‘𝑡) ∘ (𝑠‘𝑓))) |
72 | 59, 65, 71 | 3eqtr4d 2783 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑠 · (𝑡 ∘ 𝑓)) = ((𝑠‘𝑡) + (𝑠‘𝑓))) |
73 | 1, 2, 3, 7 | dvavadd 38641 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑡 + 𝑓) = (𝑡 ∘ 𝑓)) |
74 | 73 | 3adantr1 1170 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑡 + 𝑓) = (𝑡 ∘ 𝑓)) |
75 | 74 | oveq2d 7180 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑠 · (𝑡 + 𝑓)) = (𝑠 · (𝑡 ∘ 𝑓))) |
76 | 55 | 3adantr3 1172 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑠 · 𝑡) = (𝑠‘𝑡)) |
77 | 1, 2, 13, 3, 11 | dvavsca 38643 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑠 · 𝑓) = (𝑠‘𝑓)) |
78 | 77 | 3adantr2 1171 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑠 · 𝑓) = (𝑠‘𝑓)) |
79 | 76, 78 | oveq12d 7182 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = ((𝑠‘𝑡) + (𝑠‘𝑓))) |
80 | 72, 75, 79 | 3eqtr4d 2783 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝑇 ∧ 𝑓 ∈ 𝑇)) → (𝑠 · (𝑡 + 𝑓)) = ((𝑠 · 𝑡) + (𝑠 · 𝑓))) |
81 | 1, 2, 13, 3, 9, 17 | dvaplusgv 38636 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 ⨣ 𝑡)‘𝑓) = ((𝑠‘𝑓) ∘ (𝑡‘𝑓))) |
82 | 1, 2, 13, 3, 9, 17 | dvafplusg 38634 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ⨣ = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑎‘𝑓) ∘ (𝑏‘𝑓))))) |
83 | 82 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → ⨣ = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑎‘𝑓) ∘ (𝑏‘𝑓))))) |
84 | 83 | oveqd 7181 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠 ⨣ 𝑡) = (𝑠(𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑎‘𝑓) ∘ (𝑏‘𝑓))))𝑡)) |
85 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑎‘𝑓) ∘ (𝑏‘𝑓)))) = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑎‘𝑓) ∘ (𝑏‘𝑓)))) |
86 | 1, 2, 13, 85 | tendoplcl 38407 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠(𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑎‘𝑓) ∘ (𝑏‘𝑓))))𝑡) ∈ 𝐸) |
87 | 84, 86 | eqeltrd 2833 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠 ⨣ 𝑡) ∈ 𝐸) |
88 | 87 | 3adant3r3 1185 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑠 ⨣ 𝑡) ∈ 𝐸) |
89 | | simpr3 1197 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → 𝑓 ∈ 𝑇) |
90 | 88, 89 | jca 515 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 ⨣ 𝑡) ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) |
91 | 1, 2, 13, 3, 11 | dvavsca 38643 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 ⨣ 𝑡) ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 ⨣ 𝑡) · 𝑓) = ((𝑠 ⨣ 𝑡)‘𝑓)) |
92 | 90, 91 | syldan 594 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 ⨣ 𝑡) · 𝑓) = ((𝑠 ⨣ 𝑡)‘𝑓)) |
93 | 77 | 3adantr2 1171 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑠 · 𝑓) = (𝑠‘𝑓)) |
94 | 1, 2, 13, 3, 11 | dvavsca 38643 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑡 · 𝑓) = (𝑡‘𝑓)) |
95 | 94 | 3adantr1 1170 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑡 · 𝑓) = (𝑡‘𝑓)) |
96 | 93, 95 | oveq12d 7182 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = ((𝑠‘𝑓) + (𝑡‘𝑓))) |
97 | 67 | 3adant3r2 1184 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑠‘𝑓) ∈ 𝑇) |
98 | 1, 2, 13 | tendospcl 38644 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇) → (𝑡‘𝑓) ∈ 𝑇) |
99 | 98 | 3adant3r1 1183 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑡‘𝑓) ∈ 𝑇) |
100 | 97, 99 | jca 515 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠‘𝑓) ∈ 𝑇 ∧ (𝑡‘𝑓) ∈ 𝑇)) |
101 | 1, 2, 3, 7 | dvavadd 38641 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠‘𝑓) ∈ 𝑇 ∧ (𝑡‘𝑓) ∈ 𝑇)) → ((𝑠‘𝑓) + (𝑡‘𝑓)) = ((𝑠‘𝑓) ∘ (𝑡‘𝑓))) |
102 | 100, 101 | syldan 594 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠‘𝑓) + (𝑡‘𝑓)) = ((𝑠‘𝑓) ∘ (𝑡‘𝑓))) |
103 | 96, 102 | eqtrd 2773 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = ((𝑠‘𝑓) ∘ (𝑡‘𝑓))) |
104 | 81, 92, 103 | 3eqtr4d 2783 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 ⨣ 𝑡) · 𝑓) = ((𝑠 · 𝑓) + (𝑡 · 𝑓))) |
105 | 1, 2, 13 | tendospass 38645 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 ∘ 𝑡)‘𝑓) = (𝑠‘(𝑡‘𝑓))) |
106 | 1, 13 | tendococl 38398 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠 ∘ 𝑡) ∈ 𝐸) |
107 | 106 | 3adant3r3 1185 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑠 ∘ 𝑡) ∈ 𝐸) |
108 | 107, 89 | jca 515 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 ∘ 𝑡) ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) |
109 | 1, 2, 13, 3, 11 | dvavsca 38643 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 ∘ 𝑡) ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 ∘ 𝑡) · 𝑓) = ((𝑠 ∘ 𝑡)‘𝑓)) |
110 | 108, 109 | syldan 594 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 ∘ 𝑡) · 𝑓) = ((𝑠 ∘ 𝑡)‘𝑓)) |
111 | | simpr1 1195 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → 𝑠 ∈ 𝐸) |
112 | 111, 99 | jca 515 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑠 ∈ 𝐸 ∧ (𝑡‘𝑓) ∈ 𝑇)) |
113 | 1, 2, 13, 3, 11 | dvavsca 38643 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (𝑡‘𝑓) ∈ 𝑇)) → (𝑠 · (𝑡‘𝑓)) = (𝑠‘(𝑡‘𝑓))) |
114 | 112, 113 | syldan 594 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑠 · (𝑡‘𝑓)) = (𝑠‘(𝑡‘𝑓))) |
115 | 105, 110,
114 | 3eqtr4d 2783 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 ∘ 𝑡) · 𝑓) = (𝑠 · (𝑡‘𝑓))) |
116 | 1, 2, 13, 3, 9, 19 | dvamulr 38638 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸)) → (𝑠 × 𝑡) = (𝑠 ∘ 𝑡)) |
117 | 116 | 3adantr3 1172 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑠 × 𝑡) = (𝑠 ∘ 𝑡)) |
118 | 117 | oveq1d 7179 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 × 𝑡) · 𝑓) = ((𝑠 ∘ 𝑡) · 𝑓)) |
119 | 95 | oveq2d 7180 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → (𝑠 · (𝑡 · 𝑓)) = (𝑠 · (𝑡‘𝑓))) |
120 | 115, 118,
119 | 3eqtr4d 2783 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇)) → ((𝑠 × 𝑡) · 𝑓) = (𝑠 · (𝑡 · 𝑓))) |
121 | 21 | anim1i 618 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝑇) → (( I ↾ 𝑇) ∈ 𝐸 ∧ 𝑠 ∈ 𝑇)) |
122 | 1, 2, 13, 3, 11 | dvavsca 38643 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (( I ↾ 𝑇) ∈ 𝐸 ∧ 𝑠 ∈ 𝑇)) → (( I ↾ 𝑇) · 𝑠) = (( I ↾ 𝑇)‘𝑠)) |
123 | 121, 122 | syldan 594 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝑇) → (( I ↾ 𝑇) · 𝑠) = (( I ↾ 𝑇)‘𝑠)) |
124 | | fvresi 6939 |
. . . . 5
⊢ (𝑠 ∈ 𝑇 → (( I ↾ 𝑇)‘𝑠) = 𝑠) |
125 | 124 | adantl 485 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝑇) → (( I ↾ 𝑇)‘𝑠) = 𝑠) |
126 | 123, 125 | eqtrd 2773 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝑇) → (( I ↾ 𝑇) · 𝑠) = 𝑠) |
127 | 6, 8, 10, 12, 16, 18, 20, 49, 51, 54, 58, 80, 104, 120, 126 | islmodd 19752 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LMod) |
128 | 9 | islvec 19988 |
. 2
⊢ (𝑈 ∈ LVec ↔ (𝑈 ∈ LMod ∧ 𝐷 ∈
DivRing)) |
129 | 127, 43, 128 | sylanbrc 586 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec) |