Step | Hyp | Ref
| Expression |
1 | | dvhgrp.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | dvhgrp.t |
. . . 4
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
3 | | dvhgrp.e |
. . . 4
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
4 | | dvhgrp.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
5 | | eqid 2738 |
. . . 4
⊢
(Base‘𝑈) =
(Base‘𝑈) |
6 | 1, 2, 3, 4, 5 | dvhvbase 39101 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝑈) = (𝑇 × 𝐸)) |
7 | 6 | eqcomd 2744 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑇 × 𝐸) = (Base‘𝑈)) |
8 | | dvhgrp.a |
. . 3
⊢ + =
(+g‘𝑈) |
9 | 8 | a1i 11 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → + =
(+g‘𝑈)) |
10 | | dvhgrp.d |
. . . 4
⊢ 𝐷 = (Scalar‘𝑈) |
11 | | dvhgrp.p |
. . . 4
⊢ ⨣ =
(+g‘𝐷) |
12 | 1, 2, 3, 4, 10, 11, 8 | dvhvaddcl 39109 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ (𝑇 × 𝐸) ∧ 𝑔 ∈ (𝑇 × 𝐸))) → (𝑓 + 𝑔) ∈ (𝑇 × 𝐸)) |
13 | 12 | 3impb 1114 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → (𝑓 + 𝑔) ∈ (𝑇 × 𝐸)) |
14 | 1, 2, 3, 4, 10, 11, 8 | dvhvaddass 39111 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ (𝑇 × 𝐸) ∧ 𝑔 ∈ (𝑇 × 𝐸) ∧ ℎ ∈ (𝑇 × 𝐸))) → ((𝑓 + 𝑔) + ℎ) = (𝑓 + (𝑔 + ℎ))) |
15 | | dvhgrp.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
16 | 15, 1, 2 | idltrn 38164 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝑇) |
17 | | eqid 2738 |
. . . . . . . 8
⊢
((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊) |
18 | 1, 17, 4, 10 | dvhsca 39096 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 = ((EDRing‘𝐾)‘𝑊)) |
19 | 1, 17 | erngdv 39007 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ DivRing) |
20 | 18, 19 | eqeltrd 2839 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ DivRing) |
21 | | drnggrp 19999 |
. . . . . 6
⊢ (𝐷 ∈ DivRing → 𝐷 ∈ Grp) |
22 | 20, 21 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ Grp) |
23 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝐷) =
(Base‘𝐷) |
24 | | dvhgrp.o |
. . . . . 6
⊢ 0 =
(0g‘𝐷) |
25 | 23, 24 | grpidcl 18607 |
. . . . 5
⊢ (𝐷 ∈ Grp → 0 ∈
(Base‘𝐷)) |
26 | 22, 25 | syl 17 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 ∈ (Base‘𝐷)) |
27 | 1, 3, 4, 10, 23 | dvhbase 39097 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝐷) = 𝐸) |
28 | 26, 27 | eleqtrd 2841 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 ∈ 𝐸) |
29 | | opelxpi 5626 |
. . 3
⊢ ((( I
↾ 𝐵) ∈ 𝑇 ∧ 0 ∈ 𝐸) → 〈( I ↾ 𝐵), 0 〉 ∈ (𝑇 × 𝐸)) |
30 | 16, 28, 29 | syl2anc 584 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 〈( I ↾ 𝐵), 0 〉 ∈ (𝑇 × 𝐸)) |
31 | | simpl 483 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
32 | 16 | adantr 481 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → ( I ↾ 𝐵) ∈ 𝑇) |
33 | 28 | adantr 481 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → 0 ∈ 𝐸) |
34 | | xp1st 7863 |
. . . . . 6
⊢ (𝑓 ∈ (𝑇 × 𝐸) → (1st ‘𝑓) ∈ 𝑇) |
35 | 34 | adantl 482 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (1st ‘𝑓) ∈ 𝑇) |
36 | | xp2nd 7864 |
. . . . . 6
⊢ (𝑓 ∈ (𝑇 × 𝐸) → (2nd ‘𝑓) ∈ 𝐸) |
37 | 36 | adantl 482 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (2nd ‘𝑓) ∈ 𝐸) |
38 | 1, 2, 3, 4, 10, 8,
11 | dvhopvadd 39107 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (( I ↾ 𝐵) ∈ 𝑇 ∧ 0 ∈ 𝐸) ∧ ((1st ‘𝑓) ∈ 𝑇 ∧ (2nd ‘𝑓) ∈ 𝐸)) → (〈( I ↾ 𝐵), 0 〉 + 〈(1st
‘𝑓), (2nd
‘𝑓)〉) = 〈((
I ↾ 𝐵) ∘
(1st ‘𝑓)),
( 0 ⨣
(2nd ‘𝑓))〉) |
39 | 31, 32, 33, 35, 37, 38 | syl122anc 1378 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (〈( I ↾ 𝐵), 0 〉 + 〈(1st
‘𝑓), (2nd
‘𝑓)〉) = 〈((
I ↾ 𝐵) ∘
(1st ‘𝑓)),
( 0 ⨣
(2nd ‘𝑓))〉) |
40 | 15, 1, 2 | ltrn1o 38138 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (1st ‘𝑓) ∈ 𝑇) → (1st ‘𝑓):𝐵–1-1-onto→𝐵) |
41 | 35, 40 | syldan 591 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (1st ‘𝑓):𝐵–1-1-onto→𝐵) |
42 | | f1of 6716 |
. . . . . 6
⊢
((1st ‘𝑓):𝐵–1-1-onto→𝐵 → (1st
‘𝑓):𝐵⟶𝐵) |
43 | | fcoi2 6649 |
. . . . . 6
⊢
((1st ‘𝑓):𝐵⟶𝐵 → (( I ↾ 𝐵) ∘ (1st ‘𝑓)) = (1st
‘𝑓)) |
44 | 41, 42, 43 | 3syl 18 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (( I ↾ 𝐵) ∘ (1st ‘𝑓)) = (1st
‘𝑓)) |
45 | 22 | adantr 481 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → 𝐷 ∈ Grp) |
46 | 27 | adantr 481 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (Base‘𝐷) = 𝐸) |
47 | 37, 46 | eleqtrrd 2842 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (2nd ‘𝑓) ∈ (Base‘𝐷)) |
48 | 23, 11, 24 | grplid 18609 |
. . . . . 6
⊢ ((𝐷 ∈ Grp ∧
(2nd ‘𝑓)
∈ (Base‘𝐷))
→ ( 0 ⨣ (2nd
‘𝑓)) =
(2nd ‘𝑓)) |
49 | 45, 47, 48 | syl2anc 584 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → ( 0 ⨣ (2nd
‘𝑓)) =
(2nd ‘𝑓)) |
50 | 44, 49 | opeq12d 4812 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → 〈(( I ↾ 𝐵) ∘ (1st
‘𝑓)), ( 0 ⨣
(2nd ‘𝑓))〉 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) |
51 | 39, 50 | eqtrd 2778 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (〈( I ↾ 𝐵), 0 〉 + 〈(1st
‘𝑓), (2nd
‘𝑓)〉) =
〈(1st ‘𝑓), (2nd ‘𝑓)〉) |
52 | | 1st2nd2 7870 |
. . . . 5
⊢ (𝑓 ∈ (𝑇 × 𝐸) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) |
53 | 52 | adantl 482 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) |
54 | 53 | oveq2d 7291 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (〈( I ↾ 𝐵), 0 〉 + 𝑓) = (〈( I ↾ 𝐵), 0 〉 + 〈(1st
‘𝑓), (2nd
‘𝑓)〉)) |
55 | 51, 54, 53 | 3eqtr4d 2788 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (〈( I ↾ 𝐵), 0 〉 + 𝑓) = 𝑓) |
56 | 1, 2 | ltrncnv 38160 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (1st ‘𝑓) ∈ 𝑇) → ◡(1st ‘𝑓) ∈ 𝑇) |
57 | 35, 56 | syldan 591 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → ◡(1st ‘𝑓) ∈ 𝑇) |
58 | | dvhgrp.i |
. . . . . 6
⊢ 𝐼 = (invg‘𝐷) |
59 | 23, 58 | grpinvcl 18627 |
. . . . 5
⊢ ((𝐷 ∈ Grp ∧
(2nd ‘𝑓)
∈ (Base‘𝐷))
→ (𝐼‘(2nd ‘𝑓)) ∈ (Base‘𝐷)) |
60 | 45, 47, 59 | syl2anc 584 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (𝐼‘(2nd ‘𝑓)) ∈ (Base‘𝐷)) |
61 | 60, 46 | eleqtrd 2841 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (𝐼‘(2nd ‘𝑓)) ∈ 𝐸) |
62 | | opelxpi 5626 |
. . 3
⊢ ((◡(1st ‘𝑓) ∈ 𝑇 ∧ (𝐼‘(2nd ‘𝑓)) ∈ 𝐸) → 〈◡(1st ‘𝑓), (𝐼‘(2nd ‘𝑓))〉 ∈ (𝑇 × 𝐸)) |
63 | 57, 61, 62 | syl2anc 584 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → 〈◡(1st ‘𝑓), (𝐼‘(2nd ‘𝑓))〉 ∈ (𝑇 × 𝐸)) |
64 | 53 | oveq2d 7291 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (〈◡(1st ‘𝑓), (𝐼‘(2nd ‘𝑓))〉 + 𝑓) = (〈◡(1st ‘𝑓), (𝐼‘(2nd ‘𝑓))〉 + 〈(1st
‘𝑓), (2nd
‘𝑓)〉)) |
65 | 1, 2, 3, 4, 10, 8,
11 | dvhopvadd 39107 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (◡(1st ‘𝑓) ∈ 𝑇 ∧ (𝐼‘(2nd ‘𝑓)) ∈ 𝐸) ∧ ((1st ‘𝑓) ∈ 𝑇 ∧ (2nd ‘𝑓) ∈ 𝐸)) → (〈◡(1st ‘𝑓), (𝐼‘(2nd ‘𝑓))〉 + 〈(1st
‘𝑓), (2nd
‘𝑓)〉) =
〈(◡(1st ‘𝑓) ∘ (1st
‘𝑓)), ((𝐼‘(2nd
‘𝑓)) ⨣
(2nd ‘𝑓))〉) |
66 | 31, 57, 61, 35, 37, 65 | syl122anc 1378 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (〈◡(1st ‘𝑓), (𝐼‘(2nd ‘𝑓))〉 + 〈(1st
‘𝑓), (2nd
‘𝑓)〉) =
〈(◡(1st ‘𝑓) ∘ (1st
‘𝑓)), ((𝐼‘(2nd
‘𝑓)) ⨣
(2nd ‘𝑓))〉) |
67 | | f1ococnv1 6745 |
. . . . . 6
⊢
((1st ‘𝑓):𝐵–1-1-onto→𝐵 → (◡(1st ‘𝑓) ∘ (1st ‘𝑓)) = ( I ↾ 𝐵)) |
68 | 41, 67 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (◡(1st ‘𝑓) ∘ (1st ‘𝑓)) = ( I ↾ 𝐵)) |
69 | 23, 11, 24, 58 | grplinv 18628 |
. . . . . 6
⊢ ((𝐷 ∈ Grp ∧
(2nd ‘𝑓)
∈ (Base‘𝐷))
→ ((𝐼‘(2nd ‘𝑓)) ⨣ (2nd
‘𝑓)) = 0
) |
70 | 45, 47, 69 | syl2anc 584 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → ((𝐼‘(2nd ‘𝑓)) ⨣ (2nd
‘𝑓)) = 0
) |
71 | 68, 70 | opeq12d 4812 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → 〈(◡(1st ‘𝑓) ∘ (1st ‘𝑓)), ((𝐼‘(2nd ‘𝑓)) ⨣ (2nd
‘𝑓))〉 = 〈(
I ↾ 𝐵), 0
〉) |
72 | 66, 71 | eqtrd 2778 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (〈◡(1st ‘𝑓), (𝐼‘(2nd ‘𝑓))〉 + 〈(1st
‘𝑓), (2nd
‘𝑓)〉) = 〈(
I ↾ 𝐵), 0
〉) |
73 | 64, 72 | eqtrd 2778 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ (𝑇 × 𝐸)) → (〈◡(1st ‘𝑓), (𝐼‘(2nd ‘𝑓))〉 + 𝑓) = 〈( I ↾ 𝐵), 0 〉) |
74 | 7, 9, 13, 14, 30, 55, 63, 73 | isgrpd 18601 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ Grp) |