Step | Hyp | Ref
| Expression |
1 | | dvhgrp.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | dvhgrp.t |
. . . . 5
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
3 | | dvhgrp.e |
. . . . 5
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
4 | | dvhgrp.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
5 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑈) =
(Base‘𝑈) |
6 | 1, 2, 3, 4, 5 | dvhvbase 38724 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝑈) = (𝑇 × 𝐸)) |
7 | 6 | eqcomd 2744 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑇 × 𝐸) = (Base‘𝑈)) |
8 | | dvhgrp.a |
. . . 4
⊢ + =
(+g‘𝑈) |
9 | 8 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → + =
(+g‘𝑈)) |
10 | | dvhgrp.d |
. . . 4
⊢ 𝐷 = (Scalar‘𝑈) |
11 | 10 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 = (Scalar‘𝑈)) |
12 | | dvhlvec.s |
. . . 4
⊢ · = (
·𝑠 ‘𝑈) |
13 | 12 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → · = (
·𝑠 ‘𝑈)) |
14 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) |
15 | 1, 3, 4, 10, 14 | dvhbase 38720 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝐷) = 𝐸) |
16 | 15 | eqcomd 2744 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐸 = (Base‘𝐷)) |
17 | | dvhgrp.p |
. . . 4
⊢ ⨣ =
(+g‘𝐷) |
18 | 17 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ⨣ =
(+g‘𝐷)) |
19 | | dvhlvec.m |
. . . 4
⊢ × =
(.r‘𝐷) |
20 | 19 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → × =
(.r‘𝐷)) |
21 | | eqid 2738 |
. . . . . 6
⊢
((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊) |
22 | 1, 21, 4, 10 | dvhsca 38719 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 = ((EDRing‘𝐾)‘𝑊)) |
23 | 22 | fveq2d 6678 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (1r‘𝐷) =
(1r‘((EDRing‘𝐾)‘𝑊))) |
24 | | eqid 2738 |
. . . . 5
⊢
(1r‘((EDRing‘𝐾)‘𝑊)) =
(1r‘((EDRing‘𝐾)‘𝑊)) |
25 | 1, 2, 21, 24 | erng1r 38632 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) →
(1r‘((EDRing‘𝐾)‘𝑊)) = ( I ↾ 𝑇)) |
26 | 23, 25 | eqtr2d 2774 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) = (1r‘𝐷)) |
27 | 1, 21 | erngdv 38630 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ DivRing) |
28 | 22, 27 | eqeltrd 2833 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ DivRing) |
29 | | drngring 19628 |
. . . 4
⊢ (𝐷 ∈ DivRing → 𝐷 ∈ Ring) |
30 | 28, 29 | syl 17 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ Ring) |
31 | | dvhgrp.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
32 | | dvhgrp.o |
. . . 4
⊢ 0 =
(0g‘𝐷) |
33 | | dvhgrp.i |
. . . 4
⊢ 𝐼 = (invg‘𝐷) |
34 | 31, 1, 2, 3, 4, 10,
17, 8, 32, 33 | dvhgrp 38744 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ Grp) |
35 | 1, 2, 3, 4, 12 | dvhvscacl 38740 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸)) |
36 | 35 | 3impb 1116 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸)) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸)) |
37 | | simpl 486 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
38 | | simpr1 1195 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ 𝐸) |
39 | | simpr2 1196 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ (𝑇 × 𝐸)) |
40 | | xp1st 7746 |
. . . . . . . 8
⊢ (𝑡 ∈ (𝑇 × 𝐸) → (1st ‘𝑡) ∈ 𝑇) |
41 | 39, 40 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘𝑡) ∈ 𝑇) |
42 | | simpr3 1197 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑓 ∈ (𝑇 × 𝐸)) |
43 | | xp1st 7746 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝑇 × 𝐸) → (1st ‘𝑓) ∈ 𝑇) |
44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘𝑓) ∈ 𝑇) |
45 | 1, 2, 3 | tendospdi1 38657 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (1st ‘𝑡) ∈ 𝑇 ∧ (1st ‘𝑓) ∈ 𝑇)) → (𝑠‘((1st ‘𝑡) ∘ (1st
‘𝑓))) = ((𝑠‘(1st
‘𝑡)) ∘ (𝑠‘(1st
‘𝑓)))) |
46 | 37, 38, 41, 44, 45 | syl13anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘((1st ‘𝑡) ∘ (1st
‘𝑓))) = ((𝑠‘(1st
‘𝑡)) ∘ (𝑠‘(1st
‘𝑓)))) |
47 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 38729 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) = 〈((1st ‘𝑡) ∘ (1st
‘𝑓)),
((2nd ‘𝑡)
⨣
(2nd ‘𝑓))〉) |
48 | 47 | 3adantr1 1170 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) = 〈((1st ‘𝑡) ∘ (1st
‘𝑓)),
((2nd ‘𝑡)
⨣
(2nd ‘𝑓))〉) |
49 | 48 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 + 𝑓)) = (1st
‘〈((1st ‘𝑡) ∘ (1st ‘𝑓)), ((2nd
‘𝑡) ⨣
(2nd ‘𝑓))〉)) |
50 | | fvex 6687 |
. . . . . . . . . 10
⊢
(1st ‘𝑡) ∈ V |
51 | | fvex 6687 |
. . . . . . . . . 10
⊢
(1st ‘𝑓) ∈ V |
52 | 50, 51 | coex 7661 |
. . . . . . . . 9
⊢
((1st ‘𝑡) ∘ (1st ‘𝑓)) ∈ V |
53 | | ovex 7203 |
. . . . . . . . 9
⊢
((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) ∈
V |
54 | 52, 53 | op1st 7722 |
. . . . . . . 8
⊢
(1st ‘〈((1st ‘𝑡) ∘ (1st ‘𝑓)), ((2nd
‘𝑡) ⨣
(2nd ‘𝑓))〉) = ((1st ‘𝑡) ∘ (1st
‘𝑓)) |
55 | 49, 54 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 + 𝑓)) = ((1st ‘𝑡) ∘ (1st
‘𝑓))) |
56 | 55 | fveq2d 6678 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘(1st ‘(𝑡 + 𝑓))) = (𝑠‘((1st ‘𝑡) ∘ (1st
‘𝑓)))) |
57 | 1, 2, 3, 4, 12 | dvhvsca 38738 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) = 〈(𝑠‘(1st ‘𝑡)), (𝑠 ∘ (2nd ‘𝑡))〉) |
58 | 57 | 3adantr3 1172 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) = 〈(𝑠‘(1st ‘𝑡)), (𝑠 ∘ (2nd ‘𝑡))〉) |
59 | 58 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑡)) = (1st ‘〈(𝑠‘(1st
‘𝑡)), (𝑠 ∘ (2nd
‘𝑡))〉)) |
60 | | fvex 6687 |
. . . . . . . . 9
⊢ (𝑠‘(1st
‘𝑡)) ∈
V |
61 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑠 ∈ V |
62 | | fvex 6687 |
. . . . . . . . . 10
⊢
(2nd ‘𝑡) ∈ V |
63 | 61, 62 | coex 7661 |
. . . . . . . . 9
⊢ (𝑠 ∘ (2nd
‘𝑡)) ∈
V |
64 | 60, 63 | op1st 7722 |
. . . . . . . 8
⊢
(1st ‘〈(𝑠‘(1st ‘𝑡)), (𝑠 ∘ (2nd ‘𝑡))〉) = (𝑠‘(1st ‘𝑡)) |
65 | 59, 64 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑡)) = (𝑠‘(1st ‘𝑡))) |
66 | 1, 2, 3, 4, 12 | dvhvsca 38738 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) |
67 | 66 | 3adantr2 1171 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) |
68 | 67 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (1st ‘〈(𝑠‘(1st
‘𝑓)), (𝑠 ∘ (2nd
‘𝑓))〉)) |
69 | | fvex 6687 |
. . . . . . . . 9
⊢ (𝑠‘(1st
‘𝑓)) ∈
V |
70 | | fvex 6687 |
. . . . . . . . . 10
⊢
(2nd ‘𝑓) ∈ V |
71 | 61, 70 | coex 7661 |
. . . . . . . . 9
⊢ (𝑠 ∘ (2nd
‘𝑓)) ∈
V |
72 | 69, 71 | op1st 7722 |
. . . . . . . 8
⊢
(1st ‘〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) = (𝑠‘(1st ‘𝑓)) |
73 | 68, 72 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (𝑠‘(1st ‘𝑓))) |
74 | 65, 73 | coeq12d 5707 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))) = ((𝑠‘(1st ‘𝑡)) ∘ (𝑠‘(1st ‘𝑓)))) |
75 | 46, 56, 74 | 3eqtr4d 2783 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘(1st ‘(𝑡 + 𝑓))) = ((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓)))) |
76 | 30 | adantr 484 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐷 ∈ Ring) |
77 | 16 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐸 = (Base‘𝐷)) |
78 | 38, 77 | eleqtrd 2835 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ (Base‘𝐷)) |
79 | | xp2nd 7747 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (𝑇 × 𝐸) → (2nd ‘𝑡) ∈ 𝐸) |
80 | 39, 79 | syl 17 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑡) ∈ 𝐸) |
81 | 80, 77 | eleqtrd 2835 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑡) ∈ (Base‘𝐷)) |
82 | | xp2nd 7747 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (𝑇 × 𝐸) → (2nd ‘𝑓) ∈ 𝐸) |
83 | 42, 82 | syl 17 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑓) ∈ 𝐸) |
84 | 83, 77 | eleqtrd 2835 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑓) ∈ (Base‘𝐷)) |
85 | 14, 17, 19 | ringdi 19438 |
. . . . . . . 8
⊢ ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Base‘𝐷) ∧ (2nd
‘𝑡) ∈
(Base‘𝐷) ∧
(2nd ‘𝑓)
∈ (Base‘𝐷)))
→ (𝑠 ×
((2nd ‘𝑡)
⨣
(2nd ‘𝑓)))
= ((𝑠 × (2nd
‘𝑡)) ⨣ (𝑠 × (2nd
‘𝑓)))) |
86 | 76, 78, 81, 84, 85 | syl13anc 1373 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × ((2nd
‘𝑡) ⨣
(2nd ‘𝑓)))
= ((𝑠 × (2nd
‘𝑡)) ⨣ (𝑠 × (2nd
‘𝑓)))) |
87 | 14, 17 | ringacl 19450 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ Ring ∧
(2nd ‘𝑡)
∈ (Base‘𝐷) ∧
(2nd ‘𝑓)
∈ (Base‘𝐷))
→ ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) ∈
(Base‘𝐷)) |
88 | 76, 81, 84, 87 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) ∈
(Base‘𝐷)) |
89 | 88, 77 | eleqtrrd 2836 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) ∈ 𝐸) |
90 | 1, 2, 3, 4, 10, 19 | dvhmulr 38723 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) ∈ 𝐸)) → (𝑠 × ((2nd
‘𝑡) ⨣
(2nd ‘𝑓)))
= (𝑠 ∘
((2nd ‘𝑡)
⨣
(2nd ‘𝑓)))) |
91 | 37, 38, 89, 90 | syl12anc 836 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × ((2nd
‘𝑡) ⨣
(2nd ‘𝑓)))
= (𝑠 ∘
((2nd ‘𝑡)
⨣
(2nd ‘𝑓)))) |
92 | 1, 2, 3, 4, 10, 19 | dvhmulr 38723 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (2nd ‘𝑡) ∈ 𝐸)) → (𝑠 × (2nd
‘𝑡)) = (𝑠 ∘ (2nd
‘𝑡))) |
93 | 37, 38, 80, 92 | syl12anc 836 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd
‘𝑡)) = (𝑠 ∘ (2nd
‘𝑡))) |
94 | 1, 2, 3, 4, 10, 19 | dvhmulr 38723 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (2nd ‘𝑓) ∈ 𝐸)) → (𝑠 × (2nd
‘𝑓)) = (𝑠 ∘ (2nd
‘𝑓))) |
95 | 37, 38, 83, 94 | syl12anc 836 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd
‘𝑓)) = (𝑠 ∘ (2nd
‘𝑓))) |
96 | 93, 95 | oveq12d 7188 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × (2nd
‘𝑡)) ⨣ (𝑠 × (2nd
‘𝑓))) = ((𝑠 ∘ (2nd
‘𝑡)) ⨣ (𝑠 ∘ (2nd
‘𝑓)))) |
97 | 86, 91, 96 | 3eqtr3d 2781 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ ((2nd ‘𝑡) ⨣ (2nd
‘𝑓))) = ((𝑠 ∘ (2nd
‘𝑡)) ⨣ (𝑠 ∘ (2nd
‘𝑓)))) |
98 | 48 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 + 𝑓)) = (2nd
‘〈((1st ‘𝑡) ∘ (1st ‘𝑓)), ((2nd
‘𝑡) ⨣
(2nd ‘𝑓))〉)) |
99 | 52, 53 | op2nd 7723 |
. . . . . . . 8
⊢
(2nd ‘〈((1st ‘𝑡) ∘ (1st ‘𝑓)), ((2nd
‘𝑡) ⨣
(2nd ‘𝑓))〉) = ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) |
100 | 98, 99 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 + 𝑓)) = ((2nd ‘𝑡) ⨣ (2nd
‘𝑓))) |
101 | 100 | coeq2d 5705 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ (2nd ‘(𝑡 + 𝑓))) = (𝑠 ∘ ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)))) |
102 | 58 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑡)) = (2nd ‘〈(𝑠‘(1st
‘𝑡)), (𝑠 ∘ (2nd
‘𝑡))〉)) |
103 | 60, 63 | op2nd 7723 |
. . . . . . . 8
⊢
(2nd ‘〈(𝑠‘(1st ‘𝑡)), (𝑠 ∘ (2nd ‘𝑡))〉) = (𝑠 ∘ (2nd ‘𝑡)) |
104 | 102, 103 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑡)) = (𝑠 ∘ (2nd ‘𝑡))) |
105 | 67 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (2nd ‘〈(𝑠‘(1st
‘𝑓)), (𝑠 ∘ (2nd
‘𝑓))〉)) |
106 | 69, 71 | op2nd 7723 |
. . . . . . . 8
⊢
(2nd ‘〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) = (𝑠 ∘ (2nd ‘𝑓)) |
107 | 105, 106 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (𝑠 ∘ (2nd ‘𝑓))) |
108 | 104, 107 | oveq12d 7188 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝑠 · 𝑡)) ⨣ (2nd
‘(𝑠 · 𝑓))) = ((𝑠 ∘ (2nd ‘𝑡)) ⨣ (𝑠 ∘ (2nd ‘𝑓)))) |
109 | 97, 101, 108 | 3eqtr4d 2783 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ (2nd ‘(𝑡 + 𝑓))) = ((2nd ‘(𝑠 · 𝑡)) ⨣ (2nd
‘(𝑠 · 𝑓)))) |
110 | 75, 109 | opeq12d 4769 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 〈(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))〉 = 〈((1st
‘(𝑠 · 𝑡)) ∘ (1st
‘(𝑠 · 𝑓))), ((2nd
‘(𝑠 · 𝑡)) ⨣ (2nd
‘(𝑠 · 𝑓)))〉) |
111 | 1, 2, 3, 4, 10, 17, 8 | dvhvaddcl 38732 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) ∈ (𝑇 × 𝐸)) |
112 | 111 | 3adantr1 1170 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) ∈ (𝑇 × 𝐸)) |
113 | 1, 2, 3, 4, 12 | dvhvsca 38738 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = 〈(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))〉) |
114 | 37, 38, 112, 113 | syl12anc 836 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = 〈(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))〉) |
115 | 35 | 3adantr3 1172 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸)) |
116 | 1, 2, 3, 4, 12 | dvhvscacl 38740 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸)) |
117 | 116 | 3adantr2 1171 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸)) |
118 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 38729 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 · 𝑡) ∈ (𝑇 × 𝐸) ∧ (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = 〈((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) ⨣ (2nd
‘(𝑠 · 𝑓)))〉) |
119 | 37, 115, 117, 118 | syl12anc 836 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = 〈((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) ⨣ (2nd
‘(𝑠 · 𝑓)))〉) |
120 | 110, 114,
119 | 3eqtr4d 2783 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ((𝑠 · 𝑡) + (𝑠 · 𝑓))) |
121 | | simpl 486 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
122 | | simpr1 1195 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ 𝐸) |
123 | | simpr2 1196 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ 𝐸) |
124 | | simpr3 1197 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑓 ∈ (𝑇 × 𝐸)) |
125 | 124, 43 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘𝑓) ∈ 𝑇) |
126 | | eqid 2738 |
. . . . . . . 8
⊢
(+g‘((EDRing‘𝐾)‘𝑊)) =
(+g‘((EDRing‘𝐾)‘𝑊)) |
127 | 1, 2, 3, 21, 126 | erngplus2 38441 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ (1st ‘𝑓) ∈ 𝑇)) → ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st ‘𝑓)) = ((𝑠‘(1st ‘𝑓)) ∘ (𝑡‘(1st ‘𝑓)))) |
128 | 121, 122,
123, 125, 127 | syl13anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st ‘𝑓)) = ((𝑠‘(1st ‘𝑓)) ∘ (𝑡‘(1st ‘𝑓)))) |
129 | 22 | fveq2d 6678 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+g‘𝐷) =
(+g‘((EDRing‘𝐾)‘𝑊))) |
130 | 17, 129 | syl5eq 2785 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ⨣ =
(+g‘((EDRing‘𝐾)‘𝑊))) |
131 | 130 | oveqd 7187 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑠 ⨣ 𝑡) = (𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)) |
132 | 131 | fveq1d 6676 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)) = ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st ‘𝑓))) |
133 | 132 | adantr 484 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)) = ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st ‘𝑓))) |
134 | 66 | 3adantr2 1171 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) |
135 | 134 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (1st ‘〈(𝑠‘(1st
‘𝑓)), (𝑠 ∘ (2nd
‘𝑓))〉)) |
136 | 135, 72 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (𝑠‘(1st ‘𝑓))) |
137 | 1, 2, 3, 4, 12 | dvhvsca 38738 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) = 〈(𝑡‘(1st ‘𝑓)), (𝑡 ∘ (2nd ‘𝑓))〉) |
138 | 137 | 3adantr1 1170 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) = 〈(𝑡‘(1st ‘𝑓)), (𝑡 ∘ (2nd ‘𝑓))〉) |
139 | 138 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 · 𝑓)) = (1st ‘〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉)) |
140 | | fvex 6687 |
. . . . . . . . 9
⊢ (𝑡‘(1st
‘𝑓)) ∈
V |
141 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑡 ∈ V |
142 | 141, 70 | coex 7661 |
. . . . . . . . 9
⊢ (𝑡 ∘ (2nd
‘𝑓)) ∈
V |
143 | 140, 142 | op1st 7722 |
. . . . . . . 8
⊢
(1st ‘〈(𝑡‘(1st ‘𝑓)), (𝑡 ∘ (2nd ‘𝑓))〉) = (𝑡‘(1st ‘𝑓)) |
144 | 139, 143 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 · 𝑓)) = (𝑡‘(1st ‘𝑓))) |
145 | 136, 144 | coeq12d 5707 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))) = ((𝑠‘(1st ‘𝑓)) ∘ (𝑡‘(1st ‘𝑓)))) |
146 | 128, 133,
145 | 3eqtr4d 2783 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)) = ((1st
‘(𝑠 · 𝑓)) ∘ (1st
‘(𝑡 · 𝑓)))) |
147 | 30 | adantr 484 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐷 ∈ Ring) |
148 | 16 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐸 = (Base‘𝐷)) |
149 | 122, 148 | eleqtrd 2835 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ (Base‘𝐷)) |
150 | 123, 148 | eleqtrd 2835 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ (Base‘𝐷)) |
151 | 124, 82 | syl 17 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑓) ∈ 𝐸) |
152 | 151, 148 | eleqtrd 2835 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑓) ∈ (Base‘𝐷)) |
153 | 14, 17, 19 | ringdir 19439 |
. . . . . . . 8
⊢ ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Base‘𝐷) ∧ 𝑡 ∈ (Base‘𝐷) ∧ (2nd ‘𝑓) ∈ (Base‘𝐷))) → ((𝑠 ⨣ 𝑡) × (2nd
‘𝑓)) = ((𝑠 × (2nd
‘𝑓)) ⨣ (𝑡 × (2nd
‘𝑓)))) |
154 | 147, 149,
150, 152, 153 | syl13anc 1373 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) × (2nd
‘𝑓)) = ((𝑠 × (2nd
‘𝑓)) ⨣ (𝑡 × (2nd
‘𝑓)))) |
155 | 14, 17 | ringacl 19450 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ Ring ∧ 𝑠 ∈ (Base‘𝐷) ∧ 𝑡 ∈ (Base‘𝐷)) → (𝑠 ⨣ 𝑡) ∈ (Base‘𝐷)) |
156 | 147, 149,
150, 155 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ⨣ 𝑡) ∈ (Base‘𝐷)) |
157 | 156, 148 | eleqtrrd 2836 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ⨣ 𝑡) ∈ 𝐸) |
158 | 1, 2, 3, 4, 10, 19 | dvhmulr 38723 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 ⨣ 𝑡) ∈ 𝐸 ∧ (2nd ‘𝑓) ∈ 𝐸)) → ((𝑠 ⨣ 𝑡) × (2nd
‘𝑓)) = ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓))) |
159 | 121, 157,
151, 158 | syl12anc 836 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) × (2nd
‘𝑓)) = ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓))) |
160 | 121, 122,
151, 94 | syl12anc 836 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd
‘𝑓)) = (𝑠 ∘ (2nd
‘𝑓))) |
161 | 1, 2, 3, 4, 10, 19 | dvhmulr 38723 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐸 ∧ (2nd ‘𝑓) ∈ 𝐸)) → (𝑡 × (2nd
‘𝑓)) = (𝑡 ∘ (2nd
‘𝑓))) |
162 | 121, 123,
151, 161 | syl12anc 836 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 × (2nd
‘𝑓)) = (𝑡 ∘ (2nd
‘𝑓))) |
163 | 160, 162 | oveq12d 7188 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × (2nd
‘𝑓)) ⨣ (𝑡 × (2nd
‘𝑓))) = ((𝑠 ∘ (2nd
‘𝑓)) ⨣ (𝑡 ∘ (2nd
‘𝑓)))) |
164 | 154, 159,
163 | 3eqtr3d 2781 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓)) = ((𝑠 ∘ (2nd ‘𝑓)) ⨣ (𝑡 ∘ (2nd ‘𝑓)))) |
165 | 134 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (2nd ‘〈(𝑠‘(1st
‘𝑓)), (𝑠 ∘ (2nd
‘𝑓))〉)) |
166 | 165, 106 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (𝑠 ∘ (2nd ‘𝑓))) |
167 | 138 | fveq2d 6678 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 · 𝑓)) = (2nd ‘〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉)) |
168 | 140, 142 | op2nd 7723 |
. . . . . . . 8
⊢
(2nd ‘〈(𝑡‘(1st ‘𝑓)), (𝑡 ∘ (2nd ‘𝑓))〉) = (𝑡 ∘ (2nd ‘𝑓)) |
169 | 167, 168 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 · 𝑓)) = (𝑡 ∘ (2nd ‘𝑓))) |
170 | 166, 169 | oveq12d 7188 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝑠 · 𝑓)) ⨣ (2nd
‘(𝑡 · 𝑓))) = ((𝑠 ∘ (2nd ‘𝑓)) ⨣ (𝑡 ∘ (2nd ‘𝑓)))) |
171 | 164, 170 | eqtr4d 2776 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓)) = ((2nd
‘(𝑠 · 𝑓)) ⨣ (2nd
‘(𝑡 · 𝑓)))) |
172 | 146, 171 | opeq12d 4769 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 〈((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)), ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓))〉 =
〈((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) ⨣ (2nd
‘(𝑡 · 𝑓)))〉) |
173 | 1, 2, 3, 4, 12 | dvhvsca 38738 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 ⨣ 𝑡) ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) · 𝑓) = 〈((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)), ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓))〉) |
174 | 121, 157,
124, 173 | syl12anc 836 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) · 𝑓) = 〈((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)), ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓))〉) |
175 | 116 | 3adantr2 1171 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸)) |
176 | 1, 2, 3, 4, 12 | dvhvscacl 38740 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) ∈ (𝑇 × 𝐸)) |
177 | 176 | 3adantr1 1170 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) ∈ (𝑇 × 𝐸)) |
178 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 38729 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 · 𝑓) ∈ (𝑇 × 𝐸) ∧ (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = 〈((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) ⨣ (2nd
‘(𝑡 · 𝑓)))〉) |
179 | 121, 175,
177, 178 | syl12anc 836 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = 〈((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) ⨣ (2nd
‘(𝑡 · 𝑓)))〉) |
180 | 172, 174,
179 | 3eqtr4d 2783 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) · 𝑓) = ((𝑠 · 𝑓) + (𝑡 · 𝑓))) |
181 | 1, 2, 3 | tendocoval 38403 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) ∧ (1st ‘𝑓) ∈ 𝑇) → ((𝑠 ∘ 𝑡)‘(1st ‘𝑓)) = (𝑠‘(𝑡‘(1st ‘𝑓)))) |
182 | 121, 122,
123, 125, 181 | syl121anc 1376 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ∘ 𝑡)‘(1st ‘𝑓)) = (𝑠‘(𝑡‘(1st ‘𝑓)))) |
183 | | coass 6098 |
. . . . . . 7
⊢ ((𝑠 ∘ 𝑡) ∘ (2nd ‘𝑓)) = (𝑠 ∘ (𝑡 ∘ (2nd ‘𝑓))) |
184 | 183 | a1i 11 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ∘ 𝑡) ∘ (2nd ‘𝑓)) = (𝑠 ∘ (𝑡 ∘ (2nd ‘𝑓)))) |
185 | 182, 184 | opeq12d 4769 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 〈((𝑠 ∘ 𝑡)‘(1st ‘𝑓)), ((𝑠 ∘ 𝑡) ∘ (2nd ‘𝑓))〉 = 〈(𝑠‘(𝑡‘(1st ‘𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd ‘𝑓)))〉) |
186 | 1, 3 | tendococl 38409 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠 ∘ 𝑡) ∈ 𝐸) |
187 | 121, 122,
123, 186 | syl3anc 1372 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ 𝑡) ∈ 𝐸) |
188 | 1, 2, 3, 4, 12 | dvhvsca 38738 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 ∘ 𝑡) ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ∘ 𝑡) · 𝑓) = 〈((𝑠 ∘ 𝑡)‘(1st ‘𝑓)), ((𝑠 ∘ 𝑡) ∘ (2nd ‘𝑓))〉) |
189 | 121, 187,
124, 188 | syl12anc 836 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ∘ 𝑡) · 𝑓) = 〈((𝑠 ∘ 𝑡)‘(1st ‘𝑓)), ((𝑠 ∘ 𝑡) ∘ (2nd ‘𝑓))〉) |
190 | 1, 2, 3 | tendocl 38404 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑡 ∈ 𝐸 ∧ (1st ‘𝑓) ∈ 𝑇) → (𝑡‘(1st ‘𝑓)) ∈ 𝑇) |
191 | 121, 123,
125, 190 | syl3anc 1372 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡‘(1st ‘𝑓)) ∈ 𝑇) |
192 | 1, 3 | tendococl 38409 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑡 ∈ 𝐸 ∧ (2nd ‘𝑓) ∈ 𝐸) → (𝑡 ∘ (2nd ‘𝑓)) ∈ 𝐸) |
193 | 121, 123,
151, 192 | syl3anc 1372 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 ∘ (2nd ‘𝑓)) ∈ 𝐸) |
194 | 1, 2, 3, 4, 12 | dvhopvsca 38739 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (𝑡‘(1st ‘𝑓)) ∈ 𝑇 ∧ (𝑡 ∘ (2nd ‘𝑓)) ∈ 𝐸)) → (𝑠 · 〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉) =
〈(𝑠‘(𝑡‘(1st
‘𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd ‘𝑓)))〉) |
195 | 121, 122,
191, 193, 194 | syl13anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉) =
〈(𝑠‘(𝑡‘(1st
‘𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd ‘𝑓)))〉) |
196 | 185, 189,
195 | 3eqtr4d 2783 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ∘ 𝑡) · 𝑓) = (𝑠 · 〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉)) |
197 | 1, 2, 3, 4, 10, 19 | dvhmulr 38723 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸)) → (𝑠 × 𝑡) = (𝑠 ∘ 𝑡)) |
198 | 197 | 3adantr3 1172 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × 𝑡) = (𝑠 ∘ 𝑡)) |
199 | 198 | oveq1d 7185 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × 𝑡) · 𝑓) = ((𝑠 ∘ 𝑡) · 𝑓)) |
200 | 138 | oveq2d 7186 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 · 𝑓)) = (𝑠 · 〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉)) |
201 | 196, 199,
200 | 3eqtr4d 2783 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × 𝑡) · 𝑓) = (𝑠 · (𝑡 · 𝑓))) |
202 | | xp1st 7746 |
. . . . . . 7
⊢ (𝑠 ∈ (𝑇 × 𝐸) → (1st ‘𝑠) ∈ 𝑇) |
203 | 202 | adantl 485 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (1st ‘𝑠) ∈ 𝑇) |
204 | | fvresi 6945 |
. . . . . 6
⊢
((1st ‘𝑠) ∈ 𝑇 → (( I ↾ 𝑇)‘(1st ‘𝑠)) = (1st
‘𝑠)) |
205 | 203, 204 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇)‘(1st ‘𝑠)) = (1st
‘𝑠)) |
206 | | xp2nd 7747 |
. . . . . . 7
⊢ (𝑠 ∈ (𝑇 × 𝐸) → (2nd ‘𝑠) ∈ 𝐸) |
207 | 1, 2, 3 | tendof 38400 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (2nd ‘𝑠) ∈ 𝐸) → (2nd ‘𝑠):𝑇⟶𝑇) |
208 | 206, 207 | sylan2 596 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (2nd ‘𝑠):𝑇⟶𝑇) |
209 | | fcoi2 6553 |
. . . . . 6
⊢
((2nd ‘𝑠):𝑇⟶𝑇 → (( I ↾ 𝑇) ∘ (2nd ‘𝑠)) = (2nd
‘𝑠)) |
210 | 208, 209 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) ∘ (2nd ‘𝑠)) = (2nd
‘𝑠)) |
211 | 205, 210 | opeq12d 4769 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → 〈(( I ↾ 𝑇)‘(1st
‘𝑠)), (( I ↾
𝑇) ∘ (2nd
‘𝑠))〉 =
〈(1st ‘𝑠), (2nd ‘𝑠)〉) |
212 | 1, 2, 3 | tendoidcl 38406 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ 𝐸) |
213 | 212 | anim1i 618 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) ∈ 𝐸 ∧ 𝑠 ∈ (𝑇 × 𝐸))) |
214 | 1, 2, 3, 4, 12 | dvhvsca 38738 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (( I ↾ 𝑇) ∈ 𝐸 ∧ 𝑠 ∈ (𝑇 × 𝐸))) → (( I ↾ 𝑇) · 𝑠) = 〈(( I ↾ 𝑇)‘(1st ‘𝑠)), (( I ↾ 𝑇) ∘ (2nd
‘𝑠))〉) |
215 | 213, 214 | syldan 594 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) · 𝑠) = 〈(( I ↾ 𝑇)‘(1st ‘𝑠)), (( I ↾ 𝑇) ∘ (2nd
‘𝑠))〉) |
216 | | 1st2nd2 7753 |
. . . . 5
⊢ (𝑠 ∈ (𝑇 × 𝐸) → 𝑠 = 〈(1st ‘𝑠), (2nd ‘𝑠)〉) |
217 | 216 | adantl 485 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → 𝑠 = 〈(1st ‘𝑠), (2nd ‘𝑠)〉) |
218 | 211, 215,
217 | 3eqtr4d 2783 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) · 𝑠) = 𝑠) |
219 | 7, 9, 11, 13, 16, 18, 20, 26, 30, 34, 36, 120, 180, 201, 218 | islmodd 19759 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LMod) |
220 | 10 | islvec 19995 |
. 2
⊢ (𝑈 ∈ LVec ↔ (𝑈 ∈ LMod ∧ 𝐷 ∈
DivRing)) |
221 | 219, 28, 220 | sylanbrc 586 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec) |