Step | Hyp | Ref
| Expression |
1 | | dih1dimat.h |
. . . . 5
β’ π» = (LHypβπΎ) |
2 | | dih1dimat.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
3 | | id 22 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (πΎ β HL β§ π β π»)) |
4 | 1, 2, 3 | dvhlvec 39622 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π β LVec) |
5 | | dih1dimat.v |
. . . . 5
β’ π = (Baseβπ) |
6 | | dih1dimat.n |
. . . . 5
β’ π = (LSpanβπ) |
7 | | dih1dimat.z |
. . . . 5
β’ 0 =
(0gβπ) |
8 | | dih1dimat.a |
. . . . 5
β’ π΄ = (LSAtomsβπ) |
9 | 5, 6, 7, 8 | islsat 37503 |
. . . 4
β’ (π β LVec β (π· β π΄ β βπ£ β (π β { 0 })π· = (πβ{π£}))) |
10 | 4, 9 | syl 17 |
. . 3
β’ ((πΎ β HL β§ π β π») β (π· β π΄ β βπ£ β (π β { 0 })π· = (πβ{π£}))) |
11 | 10 | biimpa 478 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π· β π΄) β βπ£ β (π β { 0 })π· = (πβ{π£})) |
12 | | eldifi 4090 |
. . . . . . . 8
β’ (π£ β (π β { 0 }) β π£ β π) |
13 | | dih1dimat.t |
. . . . . . . . . 10
β’ π = ((LTrnβπΎ)βπ) |
14 | | dih1dimat.e |
. . . . . . . . . 10
β’ πΈ = ((TEndoβπΎ)βπ) |
15 | 1, 13, 14, 2, 5 | dvhvbase 39600 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β π = (π Γ πΈ)) |
16 | 15 | eleq2d 2820 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (π£ β π β π£ β (π Γ πΈ))) |
17 | 12, 16 | imbitrid 243 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (π£ β (π β { 0 }) β π£ β (π Γ πΈ))) |
18 | 17 | imp 408 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π£ β (π β { 0 })) β π£ β (π Γ πΈ)) |
19 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π = π) β π = π) |
20 | 19 | opeq2d 4841 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π = π) β β¨π, π β© = β¨π, πβ©) |
21 | 20 | sneqd 4602 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π = π) β {β¨π, π β©} = {β¨π, πβ©}) |
22 | 21 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π = π) β (πβ{β¨π, π β©}) = (πβ{β¨π, πβ©})) |
23 | | simpl 484 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΎ β HL β§ π β π»)) |
24 | | dih1dimat.b |
. . . . . . . . . . . . . . . . 17
β’ π΅ = (BaseβπΎ) |
25 | | dih1dimat.r |
. . . . . . . . . . . . . . . . 17
β’ π
= ((trLβπΎ)βπ) |
26 | 24, 1, 13, 25 | trlcl 38677 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π
βπ) β π΅) |
27 | | dih1dimat.l |
. . . . . . . . . . . . . . . . 17
β’ β€ =
(leβπΎ) |
28 | 27, 1, 13, 25 | trlle 38697 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π
βπ) β€ π) |
29 | | dih1dimat.i |
. . . . . . . . . . . . . . . . 17
β’ πΌ = ((DIsoHβπΎ)βπ) |
30 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
((DIsoBβπΎ)βπ) = ((DIsoBβπΎ)βπ) |
31 | 24, 27, 1, 29, 30 | dihvalb 39750 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ ((π
βπ) β π΅ β§ (π
βπ) β€ π)) β (πΌβ(π
βπ)) = (((DIsoBβπΎ)βπ)β(π
βπ))) |
32 | 23, 26, 28, 31 | syl12anc 836 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΌβ(π
βπ)) = (((DIsoBβπΎ)βπ)β(π
βπ))) |
33 | | dih1dimat.o |
. . . . . . . . . . . . . . . 16
β’ π = (β β π β¦ ( I βΎ π΅)) |
34 | 24, 1, 13, 25, 33, 2, 30, 6 | dib1dim2 39681 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((DIsoBβπΎ)βπ)β(π
βπ)) = (πβ{β¨π, πβ©})) |
35 | 32, 34 | eqtr2d 2774 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβ{β¨π, πβ©}) = (πΌβ(π
βπ))) |
36 | | dih1dimat.s |
. . . . . . . . . . . . . . . . . 18
β’ π = (LSubSpβπ) |
37 | 24, 1, 29, 2, 36 | dihf11 39780 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β HL β§ π β π») β πΌ:π΅β1-1βπ) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ π β π) β πΌ:π΅β1-1βπ) |
39 | | f1fn 6743 |
. . . . . . . . . . . . . . . 16
β’ (πΌ:π΅β1-1βπ β πΌ Fn π΅) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ π β π) β πΌ Fn π΅) |
41 | | fnfvelrn 7035 |
. . . . . . . . . . . . . . 15
β’ ((πΌ Fn π΅ β§ (π
βπ) β π΅) β (πΌβ(π
βπ)) β ran πΌ) |
42 | 40, 26, 41 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΌβ(π
βπ)) β ran πΌ) |
43 | 35, 42 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβ{β¨π, πβ©}) β ran πΌ) |
44 | 43 | adantrr 716 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β (πβ{β¨π, πβ©}) β ran πΌ) |
45 | 44 | adantr 482 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π = π) β (πβ{β¨π, πβ©}) β ran πΌ) |
46 | 22, 45 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π = π) β (πβ{β¨π, π β©}) β ran πΌ) |
47 | | simpll 766 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (πΎ β HL β§ π β π»)) |
48 | | dih1dimat.d |
. . . . . . . . . . . . . . . . . . 19
β’ πΉ = (Scalarβπ) |
49 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(BaseβπΉ) =
(BaseβπΉ) |
50 | 1, 14, 2, 48, 49 | dvhbase 39596 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β HL β§ π β π») β (BaseβπΉ) = πΈ) |
51 | 47, 50 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (BaseβπΉ) = πΈ) |
52 | 51 | rexeqdv 3313 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (βπ‘ β (BaseβπΉ)π’ = (π‘ Β· β¨π, π β©) β βπ‘ β πΈ π’ = (π‘ Β· β¨π, π β©))) |
53 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β§ π‘ β πΈ) β (πΎ β HL β§ π β π»)) |
54 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β§ π‘ β πΈ) β π‘ β πΈ) |
55 | | opelxpi 5674 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β π β§ π β πΈ) β β¨π, π β© β (π Γ πΈ)) |
56 | 55 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β§ π‘ β πΈ) β β¨π, π β© β (π Γ πΈ)) |
57 | | dih1dimat.m |
. . . . . . . . . . . . . . . . . . . . 21
β’ Β· = (
Β·π βπ) |
58 | 1, 13, 14, 2, 57 | dvhvscacl 39616 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΎ β HL β§ π β π») β§ (π‘ β πΈ β§ β¨π, π β© β (π Γ πΈ))) β (π‘ Β· β¨π, π β©) β (π Γ πΈ)) |
59 | 53, 54, 56, 58 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β§ π‘ β πΈ) β (π‘ Β· β¨π, π β©) β (π Γ πΈ)) |
60 | | eleq1a 2829 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π‘ Β· β¨π, π β©) β (π Γ πΈ) β (π’ = (π‘ Β· β¨π, π β©) β π’ β (π Γ πΈ))) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β§ π‘ β πΈ) β (π’ = (π‘ Β· β¨π, π β©) β π’ β (π Γ πΈ))) |
62 | 61 | rexlimdva 3149 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (βπ‘ β πΈ π’ = (π‘ Β· β¨π, π β©) β π’ β (π Γ πΈ))) |
63 | 62 | pm4.71rd 564 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (βπ‘ β πΈ π’ = (π‘ Β· β¨π, π β©) β (π’ β (π Γ πΈ) β§ βπ‘ β πΈ π’ = (π‘ Β· β¨π, π β©)))) |
64 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β π β π) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β§ π‘ β πΈ) β π β π) |
66 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β π β πΈ) |
67 | 66 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β§ π‘ β πΈ) β π β πΈ) |
68 | 1, 13, 14, 2, 57 | dvhopvsca 39615 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΎ β HL β§ π β π») β§ (π‘ β πΈ β§ π β π β§ π β πΈ)) β (π‘ Β· β¨π, π β©) = β¨(π‘βπ), (π‘ β π )β©) |
69 | 53, 54, 65, 67, 68 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β§ π‘ β πΈ) β (π‘ Β· β¨π, π β©) = β¨(π‘βπ), (π‘ β π )β©) |
70 | 69 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β§ π‘ β πΈ) β (π’ = (π‘ Β· β¨π, π β©) β π’ = β¨(π‘βπ), (π‘ β π )β©)) |
71 | 70 | rexbidva 3170 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (βπ‘ β πΈ π’ = (π‘ Β· β¨π, π β©) β βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©)) |
72 | 71 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β ((π’ β (π Γ πΈ) β§ βπ‘ β πΈ π’ = (π‘ Β· β¨π, π β©)) β (π’ β (π Γ πΈ) β§ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©))) |
73 | 52, 63, 72 | 3bitrd 305 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (βπ‘ β (BaseβπΉ)π’ = (π‘ Β· β¨π, π β©) β (π’ β (π Γ πΈ) β§ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©))) |
74 | 73 | abbidv 2802 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β {π’ β£ βπ‘ β (BaseβπΉ)π’ = (π‘ Β· β¨π, π β©)} = {π’ β£ (π’ β (π Γ πΈ) β§ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©)}) |
75 | | df-rab 3407 |
. . . . . . . . . . . . . 14
β’ {π’ β (π Γ πΈ) β£ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©} = {π’ β£ (π’ β (π Γ πΈ) β§ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©)} |
76 | 74, 75 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β {π’ β£ βπ‘ β (BaseβπΉ)π’ = (π‘ Β· β¨π, π β©)} = {π’ β (π Γ πΈ) β£ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©}) |
77 | | ssrab2 4041 |
. . . . . . . . . . . . . . 15
β’ {π’ β (π Γ πΈ) β£ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©} β (π Γ πΈ) |
78 | | relxp 5655 |
. . . . . . . . . . . . . . 15
β’ Rel
(π Γ πΈ) |
79 | | relss 5741 |
. . . . . . . . . . . . . . 15
β’ ({π’ β (π Γ πΈ) β£ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©} β (π Γ πΈ) β (Rel (π Γ πΈ) β Rel {π’ β (π Γ πΈ) β£ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©})) |
80 | 77, 78, 79 | mp2 9 |
. . . . . . . . . . . . . 14
β’ Rel
{π’ β (π Γ πΈ) β£ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©} |
81 | | relopabv 5781 |
. . . . . . . . . . . . . 14
β’ Rel
{β¨π, πβ© β£ (π = (πβπΊ) β§ π β πΈ)} |
82 | | vex 3451 |
. . . . . . . . . . . . . . . 16
β’ π β V |
83 | | vex 3451 |
. . . . . . . . . . . . . . . 16
β’ π β V |
84 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π = (πβπΊ) β π = (πβπΊ))) |
85 | 84 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π = (πβπΊ) β§ π β πΈ) β (π = (πβπΊ) β§ π β πΈ))) |
86 | | fveq1 6845 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πβπΊ) = (πβπΊ)) |
87 | 86 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π = (πβπΊ) β π = (πβπΊ))) |
88 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β πΈ β π β πΈ)) |
89 | 87, 88 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π = (πβπΊ) β§ π β πΈ) β (π = (πβπΊ) β§ π β πΈ))) |
90 | 82, 83, 85, 89 | opelopab 5503 |
. . . . . . . . . . . . . . 15
β’
(β¨π, πβ© β {β¨π, πβ© β£ (π = (πβπΊ) β§ π β πΈ)} β (π = (πβπΊ) β§ π β πΈ)) |
91 | | dih1dimat.c |
. . . . . . . . . . . . . . . . . . 19
β’ πΆ = (AtomsβπΎ) |
92 | | dih1dimat.p |
. . . . . . . . . . . . . . . . . . 19
β’ π = ((ocβπΎ)βπ) |
93 | | dih1dimat.j |
. . . . . . . . . . . . . . . . . . 19
β’ π½ = (invrβπΉ) |
94 | | dih1dimat.g |
. . . . . . . . . . . . . . . . . . 19
β’ πΊ = (β©β β π (ββπ) = (((π½βπ )βπ)βπ)) |
95 | 1, 2, 29, 8, 24, 27, 91, 92, 13, 25, 14, 33, 48, 93, 5, 57, 36, 6, 7, 94 | dih1dimatlem0 39841 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β ((π = (πβπΊ) β§ π β πΈ) β ((π β π β§ π β πΈ) β§ βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π ))))) |
96 | 95 | 3expa 1119 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β ((π = (πβπΊ) β§ π β πΈ) β ((π β π β§ π β πΈ) β§ βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π ))))) |
97 | | opelxp 5673 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π, πβ© β (π Γ πΈ) β (π β π β§ π β πΈ)) |
98 | 82, 83 | opth 5437 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨π, πβ© = β¨(π‘βπ), (π‘ β π )β© β (π = (π‘βπ) β§ π = (π‘ β π ))) |
99 | 98 | rexbii 3094 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ‘ β
πΈ β¨π, πβ© = β¨(π‘βπ), (π‘ β π )β© β βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π ))) |
100 | 97, 99 | anbi12i 628 |
. . . . . . . . . . . . . . . . 17
β’
((β¨π, πβ© β (π Γ πΈ) β§ βπ‘ β πΈ β¨π, πβ© = β¨(π‘βπ), (π‘ β π )β©) β ((π β π β§ π β πΈ) β§ βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π )))) |
101 | 96, 100 | bitr4di 289 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β ((π = (πβπΊ) β§ π β πΈ) β (β¨π, πβ© β (π Γ πΈ) β§ βπ‘ β πΈ β¨π, πβ© = β¨(π‘βπ), (π‘ β π )β©))) |
102 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = β¨π, πβ© β (π’ = β¨(π‘βπ), (π‘ β π )β© β β¨π, πβ© = β¨(π‘βπ), (π‘ β π )β©)) |
103 | 102 | rexbidv 3172 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = β¨π, πβ© β (βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β© β βπ‘ β πΈ β¨π, πβ© = β¨(π‘βπ), (π‘ β π )β©)) |
104 | 103 | elrab 3649 |
. . . . . . . . . . . . . . . 16
β’
(β¨π, πβ© β {π’ β (π Γ πΈ) β£ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©} β (β¨π, πβ© β (π Γ πΈ) β§ βπ‘ β πΈ β¨π, πβ© = β¨(π‘βπ), (π‘ β π )β©)) |
105 | 101, 104 | bitr4di 289 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β ((π = (πβπΊ) β§ π β πΈ) β β¨π, πβ© β {π’ β (π Γ πΈ) β£ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©})) |
106 | 90, 105 | bitr2id 284 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (β¨π, πβ© β {π’ β (π Γ πΈ) β£ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©} β β¨π, πβ© β {β¨π, πβ© β£ (π = (πβπΊ) β§ π β πΈ)})) |
107 | 80, 81, 106 | eqrelrdv 5752 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β {π’ β (π Γ πΈ) β£ βπ‘ β πΈ π’ = β¨(π‘βπ), (π‘ β π )β©} = {β¨π, πβ© β£ (π = (πβπΊ) β§ π β πΈ)}) |
108 | 76, 107 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β {π’ β£ βπ‘ β (BaseβπΉ)π’ = (π‘ Β· β¨π, π β©)} = {β¨π, πβ© β£ (π = (πβπΊ) β§ π β πΈ)}) |
109 | 1, 2, 47 | dvhlmod 39623 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β π β LMod) |
110 | 1, 13, 14, 2, 5 | dvhelvbasei 39601 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β β¨π, π β© β π) |
111 | 110 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β β¨π, π β© β π) |
112 | 48, 49, 5, 57, 6 | lspsn 20507 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ β¨π, π β© β π) β (πβ{β¨π, π β©}) = {π’ β£ βπ‘ β (BaseβπΉ)π’ = (π‘ Β· β¨π, π β©)}) |
113 | 109, 111,
112 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (πβ{β¨π, π β©}) = {π’ β£ βπ‘ β (BaseβπΉ)π’ = (π‘ Β· β¨π, π β©)}) |
114 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β π β π) |
115 | 24, 1, 13, 14, 33, 2, 48, 93 | tendoinvcl 39617 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β ((π½βπ ) β πΈ β§ (π½βπ ) β π)) |
116 | 115 | simpld 496 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (π½βπ ) β πΈ) |
117 | 47, 66, 114, 116 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (π½βπ ) β πΈ) |
118 | 1, 13, 14 | tendocl 39280 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ (π½βπ ) β πΈ β§ π β π) β ((π½βπ )βπ) β π) |
119 | 47, 117, 64, 118 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β ((π½βπ )βπ) β π) |
120 | 27, 91, 1, 92 | lhpocnel2 38532 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β HL β§ π β π») β (π β πΆ β§ Β¬ π β€ π)) |
121 | 47, 120 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (π β πΆ β§ Β¬ π β€ π)) |
122 | 27, 91, 1, 13 | ltrnel 38652 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ ((π½βπ )βπ) β π β§ (π β πΆ β§ Β¬ π β€ π)) β ((((π½βπ )βπ)βπ) β πΆ β§ Β¬ (((π½βπ )βπ)βπ) β€ π)) |
123 | 47, 119, 121, 122 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β ((((π½βπ )βπ)βπ) β πΆ β§ Β¬ (((π½βπ )βπ)βπ) β€ π)) |
124 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
((DIsoCβπΎ)βπ) = ((DIsoCβπΎ)βπ) |
125 | 27, 91, 1, 124, 29 | dihvalcqat 39752 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ ((((π½βπ )βπ)βπ) β πΆ β§ Β¬ (((π½βπ )βπ)βπ) β€ π)) β (πΌβ(((π½βπ )βπ)βπ)) = (((DIsoCβπΎ)βπ)β(((π½βπ )βπ)βπ))) |
126 | 47, 123, 125 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (πΌβ(((π½βπ )βπ)βπ)) = (((DIsoCβπΎ)βπ)β(((π½βπ )βπ)βπ))) |
127 | 27, 91, 1, 92, 13, 14, 124, 94 | dicval2 39692 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ ((((π½βπ )βπ)βπ) β πΆ β§ Β¬ (((π½βπ )βπ)βπ) β€ π)) β (((DIsoCβπΎ)βπ)β(((π½βπ )βπ)βπ)) = {β¨π, πβ© β£ (π = (πβπΊ) β§ π β πΈ)}) |
128 | 47, 123, 127 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (((DIsoCβπΎ)βπ)β(((π½βπ )βπ)βπ)) = {β¨π, πβ© β£ (π = (πβπΊ) β§ π β πΈ)}) |
129 | 126, 128 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (πΌβ(((π½βπ )βπ)βπ)) = {β¨π, πβ© β£ (π = (πβπΊ) β§ π β πΈ)}) |
130 | 108, 113,
129 | 3eqtr4d 2783 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (πβ{β¨π, π β©}) = (πΌβ(((π½βπ )βπ)βπ))) |
131 | 24, 1, 29 | dihfn 39781 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ π β π») β πΌ Fn π΅) |
132 | 131 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β πΌ Fn π΅) |
133 | 132 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β πΌ Fn π΅) |
134 | | simplll 774 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β πΎ β HL) |
135 | | hlop 37874 |
. . . . . . . . . . . . . . . 16
β’ (πΎ β HL β πΎ β OP) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β πΎ β OP) |
137 | 24, 1 | lhpbase 38511 |
. . . . . . . . . . . . . . . 16
β’ (π β π» β π β π΅) |
138 | 137 | ad3antlr 730 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β π β π΅) |
139 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(ocβπΎ) =
(ocβπΎ) |
140 | 24, 139 | opoccl 37706 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
141 | 136, 138,
140 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β ((ocβπΎ)βπ) β π΅) |
142 | 92, 141 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β π β π΅) |
143 | 24, 1, 13 | ltrncl 38638 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ ((π½βπ )βπ) β π β§ π β π΅) β (((π½βπ )βπ)βπ) β π΅) |
144 | 47, 119, 142, 143 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (((π½βπ )βπ)βπ) β π΅) |
145 | | fnfvelrn 7035 |
. . . . . . . . . . . 12
β’ ((πΌ Fn π΅ β§ (((π½βπ )βπ)βπ) β π΅) β (πΌβ(((π½βπ )βπ)βπ)) β ran πΌ) |
146 | 133, 144,
145 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (πΌβ(((π½βπ )βπ)βπ)) β ran πΌ) |
147 | 130, 146 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β§ π β π) β (πβ{β¨π, π β©}) β ran πΌ) |
148 | 46, 147 | pm2.61dane 3029 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ)) β (πβ{β¨π, π β©}) β ran πΌ) |
149 | 148 | ralrimivva 3194 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β βπ β π βπ β πΈ (πβ{β¨π, π β©}) β ran πΌ) |
150 | | sneq 4600 |
. . . . . . . . . . 11
β’ (π£ = β¨π, π β© β {π£} = {β¨π, π β©}) |
151 | 150 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π£ = β¨π, π β© β (πβ{π£}) = (πβ{β¨π, π β©})) |
152 | 151 | eleq1d 2819 |
. . . . . . . . 9
β’ (π£ = β¨π, π β© β ((πβ{π£}) β ran πΌ β (πβ{β¨π, π β©}) β ran πΌ)) |
153 | 152 | ralxp 5801 |
. . . . . . . 8
β’
(βπ£ β
(π Γ πΈ)(πβ{π£}) β ran πΌ β βπ β π βπ β πΈ (πβ{β¨π, π β©}) β ran πΌ) |
154 | 149, 153 | sylibr 233 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β βπ£ β (π Γ πΈ)(πβ{π£}) β ran πΌ) |
155 | 154 | r19.21bi 3233 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π£ β (π Γ πΈ)) β (πβ{π£}) β ran πΌ) |
156 | 18, 155 | syldan 592 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π£ β (π β { 0 })) β (πβ{π£}) β ran πΌ) |
157 | | eleq1a 2829 |
. . . . 5
β’ ((πβ{π£}) β ran πΌ β (π· = (πβ{π£}) β π· β ran πΌ)) |
158 | 156, 157 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π£ β (π β { 0 })) β (π· = (πβ{π£}) β π· β ran πΌ)) |
159 | 158 | rexlimdva 3149 |
. . 3
β’ ((πΎ β HL β§ π β π») β (βπ£ β (π β { 0 })π· = (πβ{π£}) β π· β ran πΌ)) |
160 | 159 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π· β π΄) β (βπ£ β (π β { 0 })π· = (πβ{π£}) β π· β ran πΌ)) |
161 | 11, 160 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π») β§ π· β π΄) β π· β ran πΌ) |