| 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 2737 |
. . . . 5
⊢
(Base‘𝑈) =
(Base‘𝑈) |
| 6 | 1, 2, 3, 4, 5 | dvhvbase 41089 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝑈) = (𝑇 × 𝐸)) |
| 7 | 6 | eqcomd 2743 |
. . 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 2737 |
. . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 15 | 1, 3, 4, 10, 14 | dvhbase 41085 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝐷) = 𝐸) |
| 16 | 15 | eqcomd 2743 |
. . 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 2737 |
. . . . . 6
⊢
((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊) |
| 22 | 1, 21, 4, 10 | dvhsca 41084 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 = ((EDRing‘𝐾)‘𝑊)) |
| 23 | 22 | fveq2d 6910 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (1r‘𝐷) =
(1r‘((EDRing‘𝐾)‘𝑊))) |
| 24 | | eqid 2737 |
. . . . 5
⊢
(1r‘((EDRing‘𝐾)‘𝑊)) =
(1r‘((EDRing‘𝐾)‘𝑊)) |
| 25 | 1, 2, 21, 24 | erng1r 40997 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) →
(1r‘((EDRing‘𝐾)‘𝑊)) = ( I ↾ 𝑇)) |
| 26 | 23, 25 | eqtr2d 2778 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) = (1r‘𝐷)) |
| 27 | 1, 21 | erngdv 40995 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ DivRing) |
| 28 | 22, 27 | eqeltrd 2841 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ DivRing) |
| 29 | | drngring 20736 |
. . . 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 41109 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ Grp) |
| 35 | 1, 2, 3, 4, 12 | dvhvscacl 41105 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸)) |
| 36 | 35 | 3impb 1115 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸)) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸)) |
| 37 | | simpl 482 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 38 | | simpr1 1195 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ 𝐸) |
| 39 | | simpr2 1196 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ (𝑇 × 𝐸)) |
| 40 | | xp1st 8046 |
. . . . . . . 8
⊢ (𝑡 ∈ (𝑇 × 𝐸) → (1st ‘𝑡) ∈ 𝑇) |
| 41 | 39, 40 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘𝑡) ∈ 𝑇) |
| 42 | | simpr3 1197 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑓 ∈ (𝑇 × 𝐸)) |
| 43 | | xp1st 8046 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝑇 × 𝐸) → (1st ‘𝑓) ∈ 𝑇) |
| 44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘𝑓) ∈ 𝑇) |
| 45 | 1, 2, 3 | tendospdi1 41022 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (1st ‘𝑡) ∈ 𝑇 ∧ (1st ‘𝑓) ∈ 𝑇)) → (𝑠‘((1st ‘𝑡) ∘ (1st
‘𝑓))) = ((𝑠‘(1st
‘𝑡)) ∘ (𝑠‘(1st
‘𝑓)))) |
| 46 | 37, 38, 41, 44, 45 | syl13anc 1374 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘((1st ‘𝑡) ∘ (1st
‘𝑓))) = ((𝑠‘(1st
‘𝑡)) ∘ (𝑠‘(1st
‘𝑓)))) |
| 47 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 41094 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) = 〈((1st ‘𝑡) ∘ (1st
‘𝑓)),
((2nd ‘𝑡)
⨣
(2nd ‘𝑓))〉) |
| 48 | 47 | 3adantr1 1170 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) = 〈((1st ‘𝑡) ∘ (1st
‘𝑓)),
((2nd ‘𝑡)
⨣
(2nd ‘𝑓))〉) |
| 49 | 48 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 + 𝑓)) = (1st
‘〈((1st ‘𝑡) ∘ (1st ‘𝑓)), ((2nd
‘𝑡) ⨣
(2nd ‘𝑓))〉)) |
| 50 | | fvex 6919 |
. . . . . . . . . 10
⊢
(1st ‘𝑡) ∈ V |
| 51 | | fvex 6919 |
. . . . . . . . . 10
⊢
(1st ‘𝑓) ∈ V |
| 52 | 50, 51 | coex 7952 |
. . . . . . . . 9
⊢
((1st ‘𝑡) ∘ (1st ‘𝑓)) ∈ V |
| 53 | | ovex 7464 |
. . . . . . . . 9
⊢
((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) ∈
V |
| 54 | 52, 53 | op1st 8022 |
. . . . . . . 8
⊢
(1st ‘〈((1st ‘𝑡) ∘ (1st ‘𝑓)), ((2nd
‘𝑡) ⨣
(2nd ‘𝑓))〉) = ((1st ‘𝑡) ∘ (1st
‘𝑓)) |
| 55 | 49, 54 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 + 𝑓)) = ((1st ‘𝑡) ∘ (1st
‘𝑓))) |
| 56 | 55 | fveq2d 6910 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘(1st ‘(𝑡 + 𝑓))) = (𝑠‘((1st ‘𝑡) ∘ (1st
‘𝑓)))) |
| 57 | 1, 2, 3, 4, 12 | dvhvsca 41103 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) = 〈(𝑠‘(1st ‘𝑡)), (𝑠 ∘ (2nd ‘𝑡))〉) |
| 58 | 57 | 3adantr3 1172 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) = 〈(𝑠‘(1st ‘𝑡)), (𝑠 ∘ (2nd ‘𝑡))〉) |
| 59 | 58 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑡)) = (1st ‘〈(𝑠‘(1st
‘𝑡)), (𝑠 ∘ (2nd
‘𝑡))〉)) |
| 60 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝑠‘(1st
‘𝑡)) ∈
V |
| 61 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑠 ∈ V |
| 62 | | fvex 6919 |
. . . . . . . . . 10
⊢
(2nd ‘𝑡) ∈ V |
| 63 | 61, 62 | coex 7952 |
. . . . . . . . 9
⊢ (𝑠 ∘ (2nd
‘𝑡)) ∈
V |
| 64 | 60, 63 | op1st 8022 |
. . . . . . . 8
⊢
(1st ‘〈(𝑠‘(1st ‘𝑡)), (𝑠 ∘ (2nd ‘𝑡))〉) = (𝑠‘(1st ‘𝑡)) |
| 65 | 59, 64 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑡)) = (𝑠‘(1st ‘𝑡))) |
| 66 | 1, 2, 3, 4, 12 | dvhvsca 41103 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) |
| 67 | 66 | 3adantr2 1171 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) |
| 68 | 67 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (1st ‘〈(𝑠‘(1st
‘𝑓)), (𝑠 ∘ (2nd
‘𝑓))〉)) |
| 69 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝑠‘(1st
‘𝑓)) ∈
V |
| 70 | | fvex 6919 |
. . . . . . . . . 10
⊢
(2nd ‘𝑓) ∈ V |
| 71 | 61, 70 | coex 7952 |
. . . . . . . . 9
⊢ (𝑠 ∘ (2nd
‘𝑓)) ∈
V |
| 72 | 69, 71 | op1st 8022 |
. . . . . . . 8
⊢
(1st ‘〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) = (𝑠‘(1st ‘𝑓)) |
| 73 | 68, 72 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (𝑠‘(1st ‘𝑓))) |
| 74 | 65, 73 | coeq12d 5875 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))) = ((𝑠‘(1st ‘𝑡)) ∘ (𝑠‘(1st ‘𝑓)))) |
| 75 | 46, 56, 74 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠‘(1st ‘(𝑡 + 𝑓))) = ((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓)))) |
| 76 | 30 | adantr 480 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐷 ∈ Ring) |
| 77 | 16 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐸 = (Base‘𝐷)) |
| 78 | 38, 77 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ (Base‘𝐷)) |
| 79 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (𝑇 × 𝐸) → (2nd ‘𝑡) ∈ 𝐸) |
| 80 | 39, 79 | syl 17 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑡) ∈ 𝐸) |
| 81 | 80, 77 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑡) ∈ (Base‘𝐷)) |
| 82 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (𝑇 × 𝐸) → (2nd ‘𝑓) ∈ 𝐸) |
| 83 | 42, 82 | syl 17 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑓) ∈ 𝐸) |
| 84 | 83, 77 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑓) ∈ (Base‘𝐷)) |
| 85 | 14, 17, 19 | ringdi 20258 |
. . . . . . . 8
⊢ ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Base‘𝐷) ∧ (2nd
‘𝑡) ∈
(Base‘𝐷) ∧
(2nd ‘𝑓)
∈ (Base‘𝐷)))
→ (𝑠 ×
((2nd ‘𝑡)
⨣
(2nd ‘𝑓)))
= ((𝑠 × (2nd
‘𝑡)) ⨣ (𝑠 × (2nd
‘𝑓)))) |
| 86 | 76, 78, 81, 84, 85 | syl13anc 1374 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × ((2nd
‘𝑡) ⨣
(2nd ‘𝑓)))
= ((𝑠 × (2nd
‘𝑡)) ⨣ (𝑠 × (2nd
‘𝑓)))) |
| 87 | 14, 17 | ringacl 20275 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ Ring ∧
(2nd ‘𝑡)
∈ (Base‘𝐷) ∧
(2nd ‘𝑓)
∈ (Base‘𝐷))
→ ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) ∈
(Base‘𝐷)) |
| 88 | 76, 81, 84, 87 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) ∈
(Base‘𝐷)) |
| 89 | 88, 77 | eleqtrrd 2844 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) ∈ 𝐸) |
| 90 | 1, 2, 3, 4, 10, 19 | dvhmulr 41088 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) ∈ 𝐸)) → (𝑠 × ((2nd
‘𝑡) ⨣
(2nd ‘𝑓)))
= (𝑠 ∘
((2nd ‘𝑡)
⨣
(2nd ‘𝑓)))) |
| 91 | 37, 38, 89, 90 | syl12anc 837 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × ((2nd
‘𝑡) ⨣
(2nd ‘𝑓)))
= (𝑠 ∘
((2nd ‘𝑡)
⨣
(2nd ‘𝑓)))) |
| 92 | 1, 2, 3, 4, 10, 19 | dvhmulr 41088 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (2nd ‘𝑡) ∈ 𝐸)) → (𝑠 × (2nd
‘𝑡)) = (𝑠 ∘ (2nd
‘𝑡))) |
| 93 | 37, 38, 80, 92 | syl12anc 837 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd
‘𝑡)) = (𝑠 ∘ (2nd
‘𝑡))) |
| 94 | 1, 2, 3, 4, 10, 19 | dvhmulr 41088 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (2nd ‘𝑓) ∈ 𝐸)) → (𝑠 × (2nd
‘𝑓)) = (𝑠 ∘ (2nd
‘𝑓))) |
| 95 | 37, 38, 83, 94 | syl12anc 837 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd
‘𝑓)) = (𝑠 ∘ (2nd
‘𝑓))) |
| 96 | 93, 95 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × (2nd
‘𝑡)) ⨣ (𝑠 × (2nd
‘𝑓))) = ((𝑠 ∘ (2nd
‘𝑡)) ⨣ (𝑠 ∘ (2nd
‘𝑓)))) |
| 97 | 86, 91, 96 | 3eqtr3d 2785 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ ((2nd ‘𝑡) ⨣ (2nd
‘𝑓))) = ((𝑠 ∘ (2nd
‘𝑡)) ⨣ (𝑠 ∘ (2nd
‘𝑓)))) |
| 98 | 48 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 + 𝑓)) = (2nd
‘〈((1st ‘𝑡) ∘ (1st ‘𝑓)), ((2nd
‘𝑡) ⨣
(2nd ‘𝑓))〉)) |
| 99 | 52, 53 | op2nd 8023 |
. . . . . . . 8
⊢
(2nd ‘〈((1st ‘𝑡) ∘ (1st ‘𝑓)), ((2nd
‘𝑡) ⨣
(2nd ‘𝑓))〉) = ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)) |
| 100 | 98, 99 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 + 𝑓)) = ((2nd ‘𝑡) ⨣ (2nd
‘𝑓))) |
| 101 | 100 | coeq2d 5873 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ (2nd ‘(𝑡 + 𝑓))) = (𝑠 ∘ ((2nd ‘𝑡) ⨣ (2nd
‘𝑓)))) |
| 102 | 58 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑡)) = (2nd ‘〈(𝑠‘(1st
‘𝑡)), (𝑠 ∘ (2nd
‘𝑡))〉)) |
| 103 | 60, 63 | op2nd 8023 |
. . . . . . . 8
⊢
(2nd ‘〈(𝑠‘(1st ‘𝑡)), (𝑠 ∘ (2nd ‘𝑡))〉) = (𝑠 ∘ (2nd ‘𝑡)) |
| 104 | 102, 103 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑡)) = (𝑠 ∘ (2nd ‘𝑡))) |
| 105 | 67 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (2nd ‘〈(𝑠‘(1st
‘𝑓)), (𝑠 ∘ (2nd
‘𝑓))〉)) |
| 106 | 69, 71 | op2nd 8023 |
. . . . . . . 8
⊢
(2nd ‘〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) = (𝑠 ∘ (2nd ‘𝑓)) |
| 107 | 105, 106 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (𝑠 ∘ (2nd ‘𝑓))) |
| 108 | 104, 107 | oveq12d 7449 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝑠 · 𝑡)) ⨣ (2nd
‘(𝑠 · 𝑓))) = ((𝑠 ∘ (2nd ‘𝑡)) ⨣ (𝑠 ∘ (2nd ‘𝑓)))) |
| 109 | 97, 101, 108 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ (2nd ‘(𝑡 + 𝑓))) = ((2nd ‘(𝑠 · 𝑡)) ⨣ (2nd
‘(𝑠 · 𝑓)))) |
| 110 | 75, 109 | opeq12d 4881 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 〈(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))〉 = 〈((1st
‘(𝑠 · 𝑡)) ∘ (1st
‘(𝑠 · 𝑓))), ((2nd
‘(𝑠 · 𝑡)) ⨣ (2nd
‘(𝑠 · 𝑓)))〉) |
| 111 | 1, 2, 3, 4, 10, 17, 8 | dvhvaddcl 41097 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) ∈ (𝑇 × 𝐸)) |
| 112 | 111 | 3adantr1 1170 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 + 𝑓) ∈ (𝑇 × 𝐸)) |
| 113 | 1, 2, 3, 4, 12 | dvhvsca 41103 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (𝑡 + 𝑓) ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = 〈(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))〉) |
| 114 | 37, 38, 112, 113 | syl12anc 837 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = 〈(𝑠‘(1st ‘(𝑡 + 𝑓))), (𝑠 ∘ (2nd ‘(𝑡 + 𝑓)))〉) |
| 115 | 35 | 3adantr3 1172 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑡) ∈ (𝑇 × 𝐸)) |
| 116 | 1, 2, 3, 4, 12 | dvhvscacl 41105 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸)) |
| 117 | 116 | 3adantr2 1171 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸)) |
| 118 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 41094 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 · 𝑡) ∈ (𝑇 × 𝐸) ∧ (𝑠 · 𝑓) ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = 〈((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) ⨣ (2nd
‘(𝑠 · 𝑓)))〉) |
| 119 | 37, 115, 117, 118 | syl12anc 837 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑡) + (𝑠 · 𝑓)) = 〈((1st ‘(𝑠 · 𝑡)) ∘ (1st ‘(𝑠 · 𝑓))), ((2nd ‘(𝑠 · 𝑡)) ⨣ (2nd
‘(𝑠 · 𝑓)))〉) |
| 120 | 110, 114,
119 | 3eqtr4d 2787 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ (𝑇 × 𝐸) ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 + 𝑓)) = ((𝑠 · 𝑡) + (𝑠 · 𝑓))) |
| 121 | | simpl 482 |
. . . . . . 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 2737 |
. . . . . . . 8
⊢
(+g‘((EDRing‘𝐾)‘𝑊)) =
(+g‘((EDRing‘𝐾)‘𝑊)) |
| 127 | 1, 2, 3, 21, 126 | erngplus2 40806 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ (1st ‘𝑓) ∈ 𝑇)) → ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st ‘𝑓)) = ((𝑠‘(1st ‘𝑓)) ∘ (𝑡‘(1st ‘𝑓)))) |
| 128 | 121, 122,
123, 125, 127 | syl13anc 1374 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st ‘𝑓)) = ((𝑠‘(1st ‘𝑓)) ∘ (𝑡‘(1st ‘𝑓)))) |
| 129 | 22 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+g‘𝐷) =
(+g‘((EDRing‘𝐾)‘𝑊))) |
| 130 | 17, 129 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ⨣ =
(+g‘((EDRing‘𝐾)‘𝑊))) |
| 131 | 130 | oveqd 7448 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑠 ⨣ 𝑡) = (𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)) |
| 132 | 131 | fveq1d 6908 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)) = ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st ‘𝑓))) |
| 133 | 132 | adantr 480 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)) = ((𝑠(+g‘((EDRing‘𝐾)‘𝑊))𝑡)‘(1st ‘𝑓))) |
| 134 | 66 | 3adantr2 1171 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) = 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) |
| 135 | 134 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (1st ‘〈(𝑠‘(1st
‘𝑓)), (𝑠 ∘ (2nd
‘𝑓))〉)) |
| 136 | 135, 72 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑠 · 𝑓)) = (𝑠‘(1st ‘𝑓))) |
| 137 | 1, 2, 3, 4, 12 | dvhvsca 41103 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) = 〈(𝑡‘(1st ‘𝑓)), (𝑡 ∘ (2nd ‘𝑓))〉) |
| 138 | 137 | 3adantr1 1170 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) = 〈(𝑡‘(1st ‘𝑓)), (𝑡 ∘ (2nd ‘𝑓))〉) |
| 139 | 138 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 · 𝑓)) = (1st ‘〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉)) |
| 140 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝑡‘(1st
‘𝑓)) ∈
V |
| 141 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑡 ∈ V |
| 142 | 141, 70 | coex 7952 |
. . . . . . . . 9
⊢ (𝑡 ∘ (2nd
‘𝑓)) ∈
V |
| 143 | 140, 142 | op1st 8022 |
. . . . . . . 8
⊢
(1st ‘〈(𝑡‘(1st ‘𝑓)), (𝑡 ∘ (2nd ‘𝑓))〉) = (𝑡‘(1st ‘𝑓)) |
| 144 | 139, 143 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (1st ‘(𝑡 · 𝑓)) = (𝑡‘(1st ‘𝑓))) |
| 145 | 136, 144 | coeq12d 5875 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))) = ((𝑠‘(1st ‘𝑓)) ∘ (𝑡‘(1st ‘𝑓)))) |
| 146 | 128, 133,
145 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)) = ((1st
‘(𝑠 · 𝑓)) ∘ (1st
‘(𝑡 · 𝑓)))) |
| 147 | 30 | adantr 480 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐷 ∈ Ring) |
| 148 | 16 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝐸 = (Base‘𝐷)) |
| 149 | 122, 148 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑠 ∈ (Base‘𝐷)) |
| 150 | 123, 148 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 𝑡 ∈ (Base‘𝐷)) |
| 151 | 124, 82 | syl 17 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑓) ∈ 𝐸) |
| 152 | 151, 148 | eleqtrd 2843 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘𝑓) ∈ (Base‘𝐷)) |
| 153 | 14, 17, 19 | ringdir 20259 |
. . . . . . . 8
⊢ ((𝐷 ∈ Ring ∧ (𝑠 ∈ (Base‘𝐷) ∧ 𝑡 ∈ (Base‘𝐷) ∧ (2nd ‘𝑓) ∈ (Base‘𝐷))) → ((𝑠 ⨣ 𝑡) × (2nd
‘𝑓)) = ((𝑠 × (2nd
‘𝑓)) ⨣ (𝑡 × (2nd
‘𝑓)))) |
| 154 | 147, 149,
150, 152, 153 | syl13anc 1374 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) × (2nd
‘𝑓)) = ((𝑠 × (2nd
‘𝑓)) ⨣ (𝑡 × (2nd
‘𝑓)))) |
| 155 | 14, 17 | ringacl 20275 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ Ring ∧ 𝑠 ∈ (Base‘𝐷) ∧ 𝑡 ∈ (Base‘𝐷)) → (𝑠 ⨣ 𝑡) ∈ (Base‘𝐷)) |
| 156 | 147, 149,
150, 155 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ⨣ 𝑡) ∈ (Base‘𝐷)) |
| 157 | 156, 148 | eleqtrrd 2844 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ⨣ 𝑡) ∈ 𝐸) |
| 158 | 1, 2, 3, 4, 10, 19 | dvhmulr 41088 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 ⨣ 𝑡) ∈ 𝐸 ∧ (2nd ‘𝑓) ∈ 𝐸)) → ((𝑠 ⨣ 𝑡) × (2nd
‘𝑓)) = ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓))) |
| 159 | 121, 157,
151, 158 | syl12anc 837 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) × (2nd
‘𝑓)) = ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓))) |
| 160 | 121, 122,
151, 94 | syl12anc 837 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × (2nd
‘𝑓)) = (𝑠 ∘ (2nd
‘𝑓))) |
| 161 | 1, 2, 3, 4, 10, 19 | dvhmulr 41088 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐸 ∧ (2nd ‘𝑓) ∈ 𝐸)) → (𝑡 × (2nd
‘𝑓)) = (𝑡 ∘ (2nd
‘𝑓))) |
| 162 | 121, 123,
151, 161 | syl12anc 837 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 × (2nd
‘𝑓)) = (𝑡 ∘ (2nd
‘𝑓))) |
| 163 | 160, 162 | oveq12d 7449 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × (2nd
‘𝑓)) ⨣ (𝑡 × (2nd
‘𝑓))) = ((𝑠 ∘ (2nd
‘𝑓)) ⨣ (𝑡 ∘ (2nd
‘𝑓)))) |
| 164 | 154, 159,
163 | 3eqtr3d 2785 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓)) = ((𝑠 ∘ (2nd ‘𝑓)) ⨣ (𝑡 ∘ (2nd ‘𝑓)))) |
| 165 | 134 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (2nd ‘〈(𝑠‘(1st
‘𝑓)), (𝑠 ∘ (2nd
‘𝑓))〉)) |
| 166 | 165, 106 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑠 · 𝑓)) = (𝑠 ∘ (2nd ‘𝑓))) |
| 167 | 138 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 · 𝑓)) = (2nd ‘〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉)) |
| 168 | 140, 142 | op2nd 8023 |
. . . . . . . 8
⊢
(2nd ‘〈(𝑡‘(1st ‘𝑓)), (𝑡 ∘ (2nd ‘𝑓))〉) = (𝑡 ∘ (2nd ‘𝑓)) |
| 169 | 167, 168 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝑡 · 𝑓)) = (𝑡 ∘ (2nd ‘𝑓))) |
| 170 | 166, 169 | oveq12d 7449 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝑠 · 𝑓)) ⨣ (2nd
‘(𝑡 · 𝑓))) = ((𝑠 ∘ (2nd ‘𝑓)) ⨣ (𝑡 ∘ (2nd ‘𝑓)))) |
| 171 | 164, 170 | eqtr4d 2780 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓)) = ((2nd
‘(𝑠 · 𝑓)) ⨣ (2nd
‘(𝑡 · 𝑓)))) |
| 172 | 146, 171 | opeq12d 4881 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 〈((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)), ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓))〉 =
〈((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) ⨣ (2nd
‘(𝑡 · 𝑓)))〉) |
| 173 | 1, 2, 3, 4, 12 | dvhvsca 41103 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 ⨣ 𝑡) ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) · 𝑓) = 〈((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)), ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓))〉) |
| 174 | 121, 157,
124, 173 | syl12anc 837 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) · 𝑓) = 〈((𝑠 ⨣ 𝑡)‘(1st ‘𝑓)), ((𝑠 ⨣ 𝑡) ∘ (2nd ‘𝑓))〉) |
| 175 | 116 | 3adantr2 1171 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 𝑓) ∈ (𝑇 × 𝐸)) |
| 176 | 1, 2, 3, 4, 12 | dvhvscacl 41105 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) ∈ (𝑇 × 𝐸)) |
| 177 | 176 | 3adantr1 1170 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 · 𝑓) ∈ (𝑇 × 𝐸)) |
| 178 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 41094 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 · 𝑓) ∈ (𝑇 × 𝐸) ∧ (𝑡 · 𝑓) ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = 〈((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) ⨣ (2nd
‘(𝑡 · 𝑓)))〉) |
| 179 | 121, 175,
177, 178 | syl12anc 837 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 · 𝑓) + (𝑡 · 𝑓)) = 〈((1st ‘(𝑠 · 𝑓)) ∘ (1st ‘(𝑡 · 𝑓))), ((2nd ‘(𝑠 · 𝑓)) ⨣ (2nd
‘(𝑡 · 𝑓)))〉) |
| 180 | 172, 174,
179 | 3eqtr4d 2787 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ⨣ 𝑡) · 𝑓) = ((𝑠 · 𝑓) + (𝑡 · 𝑓))) |
| 181 | 1, 2, 3 | tendocoval 40768 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) ∧ (1st ‘𝑓) ∈ 𝑇) → ((𝑠 ∘ 𝑡)‘(1st ‘𝑓)) = (𝑠‘(𝑡‘(1st ‘𝑓)))) |
| 182 | 121, 122,
123, 125, 181 | syl121anc 1377 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ∘ 𝑡)‘(1st ‘𝑓)) = (𝑠‘(𝑡‘(1st ‘𝑓)))) |
| 183 | | coass 6285 |
. . . . . . 7
⊢ ((𝑠 ∘ 𝑡) ∘ (2nd ‘𝑓)) = (𝑠 ∘ (𝑡 ∘ (2nd ‘𝑓))) |
| 184 | 183 | a1i 11 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ∘ 𝑡) ∘ (2nd ‘𝑓)) = (𝑠 ∘ (𝑡 ∘ (2nd ‘𝑓)))) |
| 185 | 182, 184 | opeq12d 4881 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → 〈((𝑠 ∘ 𝑡)‘(1st ‘𝑓)), ((𝑠 ∘ 𝑡) ∘ (2nd ‘𝑓))〉 = 〈(𝑠‘(𝑡‘(1st ‘𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd ‘𝑓)))〉) |
| 186 | 1, 3 | tendococl 40774 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠 ∘ 𝑡) ∈ 𝐸) |
| 187 | 121, 122,
123, 186 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 ∘ 𝑡) ∈ 𝐸) |
| 188 | 1, 2, 3, 4, 12 | dvhvsca 41103 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 ∘ 𝑡) ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ∘ 𝑡) · 𝑓) = 〈((𝑠 ∘ 𝑡)‘(1st ‘𝑓)), ((𝑠 ∘ 𝑡) ∘ (2nd ‘𝑓))〉) |
| 189 | 121, 187,
124, 188 | syl12anc 837 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ∘ 𝑡) · 𝑓) = 〈((𝑠 ∘ 𝑡)‘(1st ‘𝑓)), ((𝑠 ∘ 𝑡) ∘ (2nd ‘𝑓))〉) |
| 190 | 1, 2, 3 | tendocl 40769 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑡 ∈ 𝐸 ∧ (1st ‘𝑓) ∈ 𝑇) → (𝑡‘(1st ‘𝑓)) ∈ 𝑇) |
| 191 | 121, 123,
125, 190 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡‘(1st ‘𝑓)) ∈ 𝑇) |
| 192 | 1, 3 | tendococl 40774 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑡 ∈ 𝐸 ∧ (2nd ‘𝑓) ∈ 𝐸) → (𝑡 ∘ (2nd ‘𝑓)) ∈ 𝐸) |
| 193 | 121, 123,
151, 192 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑡 ∘ (2nd ‘𝑓)) ∈ 𝐸) |
| 194 | 1, 2, 3, 4, 12 | dvhopvsca 41104 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (𝑡‘(1st ‘𝑓)) ∈ 𝑇 ∧ (𝑡 ∘ (2nd ‘𝑓)) ∈ 𝐸)) → (𝑠 · 〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉) =
〈(𝑠‘(𝑡‘(1st
‘𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd ‘𝑓)))〉) |
| 195 | 121, 122,
191, 193, 194 | syl13anc 1374 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · 〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉) =
〈(𝑠‘(𝑡‘(1st
‘𝑓))), (𝑠 ∘ (𝑡 ∘ (2nd ‘𝑓)))〉) |
| 196 | 185, 189,
195 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 ∘ 𝑡) · 𝑓) = (𝑠 · 〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉)) |
| 197 | 1, 2, 3, 4, 10, 19 | dvhmulr 41088 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸)) → (𝑠 × 𝑡) = (𝑠 ∘ 𝑡)) |
| 198 | 197 | 3adantr3 1172 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 × 𝑡) = (𝑠 ∘ 𝑡)) |
| 199 | 198 | oveq1d 7446 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × 𝑡) · 𝑓) = ((𝑠 ∘ 𝑡) · 𝑓)) |
| 200 | 138 | oveq2d 7447 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → (𝑠 · (𝑡 · 𝑓)) = (𝑠 · 〈(𝑡‘(1st
‘𝑓)), (𝑡 ∘ (2nd
‘𝑓))〉)) |
| 201 | 196, 199,
200 | 3eqtr4d 2787 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑓 ∈ (𝑇 × 𝐸))) → ((𝑠 × 𝑡) · 𝑓) = (𝑠 · (𝑡 · 𝑓))) |
| 202 | | xp1st 8046 |
. . . . . . 7
⊢ (𝑠 ∈ (𝑇 × 𝐸) → (1st ‘𝑠) ∈ 𝑇) |
| 203 | 202 | adantl 481 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (1st ‘𝑠) ∈ 𝑇) |
| 204 | | fvresi 7193 |
. . . . . 6
⊢
((1st ‘𝑠) ∈ 𝑇 → (( I ↾ 𝑇)‘(1st ‘𝑠)) = (1st
‘𝑠)) |
| 205 | 203, 204 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇)‘(1st ‘𝑠)) = (1st
‘𝑠)) |
| 206 | | xp2nd 8047 |
. . . . . . 7
⊢ (𝑠 ∈ (𝑇 × 𝐸) → (2nd ‘𝑠) ∈ 𝐸) |
| 207 | 1, 2, 3 | tendof 40765 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (2nd ‘𝑠) ∈ 𝐸) → (2nd ‘𝑠):𝑇⟶𝑇) |
| 208 | 206, 207 | sylan2 593 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (2nd ‘𝑠):𝑇⟶𝑇) |
| 209 | | fcoi2 6783 |
. . . . . 6
⊢
((2nd ‘𝑠):𝑇⟶𝑇 → (( I ↾ 𝑇) ∘ (2nd ‘𝑠)) = (2nd
‘𝑠)) |
| 210 | 208, 209 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) ∘ (2nd ‘𝑠)) = (2nd
‘𝑠)) |
| 211 | 205, 210 | opeq12d 4881 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → 〈(( I ↾ 𝑇)‘(1st
‘𝑠)), (( I ↾
𝑇) ∘ (2nd
‘𝑠))〉 =
〈(1st ‘𝑠), (2nd ‘𝑠)〉) |
| 212 | 1, 2, 3 | tendoidcl 40771 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ 𝐸) |
| 213 | 212 | anim1i 615 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) ∈ 𝐸 ∧ 𝑠 ∈ (𝑇 × 𝐸))) |
| 214 | 1, 2, 3, 4, 12 | dvhvsca 41103 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (( I ↾ 𝑇) ∈ 𝐸 ∧ 𝑠 ∈ (𝑇 × 𝐸))) → (( I ↾ 𝑇) · 𝑠) = 〈(( I ↾ 𝑇)‘(1st ‘𝑠)), (( I ↾ 𝑇) ∘ (2nd
‘𝑠))〉) |
| 215 | 213, 214 | syldan 591 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) · 𝑠) = 〈(( I ↾ 𝑇)‘(1st ‘𝑠)), (( I ↾ 𝑇) ∘ (2nd
‘𝑠))〉) |
| 216 | | 1st2nd2 8053 |
. . . . 5
⊢ (𝑠 ∈ (𝑇 × 𝐸) → 𝑠 = 〈(1st ‘𝑠), (2nd ‘𝑠)〉) |
| 217 | 216 | adantl 481 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → 𝑠 = 〈(1st ‘𝑠), (2nd ‘𝑠)〉) |
| 218 | 211, 215,
217 | 3eqtr4d 2787 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝑇) · 𝑠) = 𝑠) |
| 219 | 7, 9, 11, 13, 16, 18, 20, 26, 30, 34, 36, 120, 180, 201, 218 | islmodd 20864 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LMod) |
| 220 | 10 | islvec 21103 |
. 2
⊢ (𝑈 ∈ LVec ↔ (𝑈 ∈ LMod ∧ 𝐷 ∈
DivRing)) |
| 221 | 219, 28, 220 | sylanbrc 583 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec) |