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 2737 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
6 | 1, 2, 3, 4, 5 | dvhvbase 39553 |
. . 3
β’ ((πΎ β HL β§ π β π») β (Baseβπ) = (π Γ πΈ)) |
7 | 6 | eqcomd 2743 |
. 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 39561 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π + π) β (π Γ πΈ)) |
13 | 12 | 3impb 1116 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ) β§ π β (π Γ πΈ)) β (π + π) β (π Γ πΈ)) |
14 | 1, 2, 3, 4, 10, 11, 8 | dvhvaddass 39563 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β (π Γ πΈ) β§ π β (π Γ πΈ) β§ β β (π Γ πΈ))) β ((π + π) + β) = (π + (π + β))) |
15 | | dvhgrp.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
16 | 15, 1, 2 | idltrn 38616 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( I βΎ π΅) β π) |
17 | | eqid 2737 |
. . . . . . . 8
β’
((EDRingβπΎ)βπ) = ((EDRingβπΎ)βπ) |
18 | 1, 17, 4, 10 | dvhsca 39548 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β π· = ((EDRingβπΎ)βπ)) |
19 | 1, 17 | erngdv 39459 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β ((EDRingβπΎ)βπ) β DivRing) |
20 | 18, 19 | eqeltrd 2838 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β π· β DivRing) |
21 | | drnggrp 20196 |
. . . . . 6
β’ (π· β DivRing β π· β Grp) |
22 | 20, 21 | syl 17 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β π· β Grp) |
23 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ·) =
(Baseβπ·) |
24 | | dvhgrp.o |
. . . . . 6
β’ 0 =
(0gβπ·) |
25 | 23, 24 | grpidcl 18779 |
. . . . 5
β’ (π· β Grp β 0 β
(Baseβπ·)) |
26 | 22, 25 | syl 17 |
. . . 4
β’ ((πΎ β HL β§ π β π») β 0 β (Baseβπ·)) |
27 | 1, 3, 4, 10, 23 | dvhbase 39549 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (Baseβπ·) = πΈ) |
28 | 26, 27 | eleqtrd 2840 |
. . 3
β’ ((πΎ β HL β§ π β π») β 0 β πΈ) |
29 | | opelxpi 5671 |
. . 3
β’ ((( I
βΎ π΅) β π β§ 0 β πΈ) β β¨( I βΎ π΅), 0 β© β (π Γ πΈ)) |
30 | 16, 28, 29 | syl2anc 585 |
. 2
β’ ((πΎ β HL β§ π β π») β β¨( I βΎ π΅), 0 β© β (π Γ πΈ)) |
31 | | simpl 484 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (πΎ β HL β§ π β π»)) |
32 | 16 | adantr 482 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β ( I βΎ π΅) β π) |
33 | 28 | adantr 482 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β 0 β πΈ) |
34 | | xp1st 7954 |
. . . . . 6
β’ (π β (π Γ πΈ) β (1st βπ) β π) |
35 | 34 | adantl 483 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (1st βπ) β π) |
36 | | xp2nd 7955 |
. . . . . 6
β’ (π β (π Γ πΈ) β (2nd βπ) β πΈ) |
37 | 36 | adantl 483 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (2nd βπ) β πΈ) |
38 | 1, 2, 3, 4, 10, 8,
11 | dvhopvadd 39559 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (( I βΎ π΅) β π β§ 0 β πΈ) β§ ((1st βπ) β π β§ (2nd βπ) β πΈ)) β (β¨( I βΎ π΅), 0 β© + β¨(1st
βπ), (2nd
βπ)β©) = β¨((
I βΎ π΅) β
(1st βπ)),
( 0 ⨣
(2nd βπ))β©) |
39 | 31, 32, 33, 35, 37, 38 | syl122anc 1380 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (β¨( I βΎ π΅), 0 β© + β¨(1st
βπ), (2nd
βπ)β©) = β¨((
I βΎ π΅) β
(1st βπ)),
( 0 ⨣
(2nd βπ))β©) |
40 | 15, 1, 2 | ltrn1o 38590 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (1st βπ) β π) β (1st βπ):π΅β1-1-ontoβπ΅) |
41 | 35, 40 | syldan 592 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (1st βπ):π΅β1-1-ontoβπ΅) |
42 | | f1of 6785 |
. . . . . 6
β’
((1st βπ):π΅β1-1-ontoβπ΅ β (1st
βπ):π΅βΆπ΅) |
43 | | fcoi2 6718 |
. . . . . 6
β’
((1st βπ):π΅βΆπ΅ β (( I βΎ π΅) β (1st βπ)) = (1st
βπ)) |
44 | 41, 42, 43 | 3syl 18 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (( I βΎ π΅) β (1st βπ)) = (1st
βπ)) |
45 | 22 | adantr 482 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β π· β Grp) |
46 | 27 | adantr 482 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (Baseβπ·) = πΈ) |
47 | 37, 46 | eleqtrrd 2841 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (2nd βπ) β (Baseβπ·)) |
48 | 23, 11, 24 | grplid 18781 |
. . . . . 6
β’ ((π· β Grp β§
(2nd βπ)
β (Baseβπ·))
β ( 0 ⨣ (2nd
βπ)) =
(2nd βπ)) |
49 | 45, 47, 48 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β ( 0 ⨣ (2nd
βπ)) =
(2nd βπ)) |
50 | 44, 49 | opeq12d 4839 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β β¨(( I βΎ π΅) β (1st
βπ)), ( 0 ⨣
(2nd βπ))β© = β¨(1st βπ), (2nd βπ)β©) |
51 | 39, 50 | eqtrd 2777 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (β¨( I βΎ π΅), 0 β© + β¨(1st
βπ), (2nd
βπ)β©) =
β¨(1st βπ), (2nd βπ)β©) |
52 | | 1st2nd2 7961 |
. . . . 5
β’ (π β (π Γ πΈ) β π = β¨(1st βπ), (2nd βπ)β©) |
53 | 52 | adantl 483 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β π = β¨(1st βπ), (2nd βπ)β©) |
54 | 53 | oveq2d 7374 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (β¨( I βΎ π΅), 0 β© + π) = (β¨( I βΎ π΅), 0 β© + β¨(1st
βπ), (2nd
βπ)β©)) |
55 | 51, 54, 53 | 3eqtr4d 2787 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (β¨( I βΎ π΅), 0 β© + π) = π) |
56 | 1, 2 | ltrncnv 38612 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (1st βπ) β π) β β‘(1st βπ) β π) |
57 | 35, 56 | syldan 592 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β β‘(1st βπ) β π) |
58 | | dvhgrp.i |
. . . . . 6
β’ πΌ = (invgβπ·) |
59 | 23, 58 | grpinvcl 18799 |
. . . . 5
β’ ((π· β Grp β§
(2nd βπ)
β (Baseβπ·))
β (πΌβ(2nd βπ)) β (Baseβπ·)) |
60 | 45, 47, 59 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (πΌβ(2nd βπ)) β (Baseβπ·)) |
61 | 60, 46 | eleqtrd 2840 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (πΌβ(2nd βπ)) β πΈ) |
62 | | opelxpi 5671 |
. . 3
β’ ((β‘(1st βπ) β π β§ (πΌβ(2nd βπ)) β πΈ) β β¨β‘(1st βπ), (πΌβ(2nd βπ))β© β (π Γ πΈ)) |
63 | 57, 61, 62 | syl2anc 585 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β β¨β‘(1st βπ), (πΌβ(2nd βπ))β© β (π Γ πΈ)) |
64 | 53 | oveq2d 7374 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (β¨β‘(1st βπ), (πΌβ(2nd βπ))β© + π) = (β¨β‘(1st βπ), (πΌβ(2nd βπ))β© + β¨(1st
βπ), (2nd
βπ)β©)) |
65 | 1, 2, 3, 4, 10, 8,
11 | dvhopvadd 39559 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (β‘(1st βπ) β π β§ (πΌβ(2nd βπ)) β πΈ) β§ ((1st βπ) β π β§ (2nd βπ) β πΈ)) β (β¨β‘(1st βπ), (πΌβ(2nd βπ))β© + β¨(1st
βπ), (2nd
βπ)β©) =
β¨(β‘(1st βπ) β (1st
βπ)), ((πΌβ(2nd
βπ)) ⨣
(2nd βπ))β©) |
66 | 31, 57, 61, 35, 37, 65 | syl122anc 1380 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (β¨β‘(1st βπ), (πΌβ(2nd βπ))β© + β¨(1st
βπ), (2nd
βπ)β©) =
β¨(β‘(1st βπ) β (1st
βπ)), ((πΌβ(2nd
βπ)) ⨣
(2nd βπ))β©) |
67 | | f1ococnv1 6814 |
. . . . . 6
β’
((1st βπ):π΅β1-1-ontoβπ΅ β (β‘(1st βπ) β (1st βπ)) = ( I βΎ π΅)) |
68 | 41, 67 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (β‘(1st βπ) β (1st βπ)) = ( I βΎ π΅)) |
69 | 23, 11, 24, 58 | grplinv 18801 |
. . . . . 6
β’ ((π· β Grp β§
(2nd βπ)
β (Baseβπ·))
β ((πΌβ(2nd βπ)) ⨣ (2nd
βπ)) = 0
) |
70 | 45, 47, 69 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β ((πΌβ(2nd βπ)) ⨣ (2nd
βπ)) = 0
) |
71 | 68, 70 | opeq12d 4839 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β β¨(β‘(1st βπ) β (1st βπ)), ((πΌβ(2nd βπ)) ⨣ (2nd
βπ))β© = β¨(
I βΎ π΅), 0
β©) |
72 | 66, 71 | eqtrd 2777 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (β¨β‘(1st βπ), (πΌβ(2nd βπ))β© + β¨(1st
βπ), (2nd
βπ)β©) = β¨(
I βΎ π΅), 0
β©) |
73 | 64, 72 | eqtrd 2777 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (β¨β‘(1st βπ), (πΌβ(2nd βπ))β© + π) = β¨( I βΎ π΅), 0 β©) |
74 | 7, 9, 13, 14, 30, 55, 63, 73 | isgrpd 18773 |
1
β’ ((πΎ β HL β§ π β π») β π β Grp) |