Step | Hyp | Ref
| Expression |
1 | | dihatexv.k |
. . . . . . . . 9
β’ (π β (πΎ β HL β§ π β π»)) |
2 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π(leβπΎ)π) β (πΎ β HL β§ π β π»)) |
3 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π(leβπΎ)π) β π β π΄) |
4 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π(leβπΎ)π) β π(leβπΎ)π) |
5 | | dihatexv.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΎ) |
6 | | eqid 2737 |
. . . . . . . . 9
β’
(leβπΎ) =
(leβπΎ) |
7 | | dihatexv.a |
. . . . . . . . 9
β’ π΄ = (AtomsβπΎ) |
8 | | dihatexv.h |
. . . . . . . . 9
β’ π» = (LHypβπΎ) |
9 | | eqid 2737 |
. . . . . . . . 9
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
10 | | eqid 2737 |
. . . . . . . . 9
β’ (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅)) = (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅)) |
11 | | dihatexv.u |
. . . . . . . . 9
β’ π = ((DVecHβπΎ)βπ) |
12 | | dihatexv.i |
. . . . . . . . 9
β’ πΌ = ((DIsoHβπΎ)βπ) |
13 | | dihatexv.n |
. . . . . . . . 9
β’ π = (LSpanβπ) |
14 | 5, 6, 7, 8, 9, 10,
11, 12, 13 | dih1dimb2 39733 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π(leβπΎ)π)) β βπ β ((LTrnβπΎ)βπ)(π β ( I βΎ π΅) β§ (πΌβπ) = (πβ{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β©}))) |
15 | 2, 3, 4, 14 | syl12anc 836 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π(leβπΎ)π) β βπ β ((LTrnβπΎ)βπ)(π β ( I βΎ π΅) β§ (πΌβπ) = (πβ{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β©}))) |
16 | 1 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π(leβπΎ)π) β§ π β ((LTrnβπΎ)βπ)) β (πΎ β HL β§ π β π»)) |
17 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π(leβπΎ)π) β§ π β ((LTrnβπΎ)βπ)) β π β ((LTrnβπΎ)βπ)) |
18 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
19 | 5, 8, 9, 18, 10 | tendo0cl 39282 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ π β π») β (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅)) β ((TEndoβπΎ)βπ)) |
20 | 16, 19 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π(leβπΎ)π) β§ π β ((LTrnβπΎ)βπ)) β (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅)) β ((TEndoβπΎ)βπ)) |
21 | | dihatexv.v |
. . . . . . . . . . . . 13
β’ π = (Baseβπ) |
22 | 8, 9, 18, 11, 21 | dvhelvbasei 39580 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅)) β ((TEndoβπΎ)βπ))) β β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β© β π) |
23 | 16, 17, 20, 22 | syl12anc 836 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π(leβπΎ)π) β§ π β ((LTrnβπΎ)βπ)) β β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β© β π) |
24 | | sneq 4601 |
. . . . . . . . . . . . 13
β’ (π₯ = β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β© β {π₯} = {β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β©}) |
25 | 24 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π₯ = β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β© β (πβ{π₯}) = (πβ{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β©})) |
26 | 25 | rspceeqv 3600 |
. . . . . . . . . . 11
β’
((β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β© β π β§ (πΌβπ) = (πβ{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β©})) β βπ₯ β π (πΌβπ) = (πβ{π₯})) |
27 | 23, 26 | sylan 581 |
. . . . . . . . . 10
β’
(((((π β§ π β π΄) β§ π(leβπΎ)π) β§ π β ((LTrnβπΎ)βπ)) β§ (πΌβπ) = (πβ{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β©})) β βπ₯ β π (πΌβπ) = (πβ{π₯})) |
28 | 27 | ex 414 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π(leβπΎ)π) β§ π β ((LTrnβπΎ)βπ)) β ((πΌβπ) = (πβ{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β©}) β βπ₯ β π (πΌβπ) = (πβ{π₯}))) |
29 | 28 | adantld 492 |
. . . . . . . 8
β’ ((((π β§ π β π΄) β§ π(leβπΎ)π) β§ π β ((LTrnβπΎ)βπ)) β ((π β ( I βΎ π΅) β§ (πΌβπ) = (πβ{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β©})) β βπ₯ β π (πΌβπ) = (πβ{π₯}))) |
30 | 29 | rexlimdva 3153 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π(leβπΎ)π) β (βπ β ((LTrnβπΎ)βπ)(π β ( I βΎ π΅) β§ (πΌβπ) = (πβ{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ π΅))β©})) β βπ₯ β π (πΌβπ) = (πβ{π₯}))) |
31 | 15, 30 | mpd 15 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π(leβπΎ)π) β βπ₯ β π (πΌβπ) = (πβ{π₯})) |
32 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ Β¬ π(leβπΎ)π) β (πΎ β HL β§ π β π»)) |
33 | | eqid 2737 |
. . . . . . . . . . 11
β’
((ocβπΎ)βπ) = ((ocβπΎ)βπ) |
34 | 6, 7, 8, 33 | lhpocnel2 38511 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π») β (((ocβπΎ)βπ) β π΄ β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π)) |
35 | 32, 34 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ Β¬ π(leβπΎ)π) β (((ocβπΎ)βπ) β π΄ β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π)) |
36 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ Β¬ π(leβπΎ)π) β π β π΄) |
37 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ Β¬ π(leβπΎ)π) β Β¬ π(leβπΎ)π) |
38 | | eqid 2737 |
. . . . . . . . . 10
β’
(β©π
β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) = (β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) |
39 | 6, 7, 8, 9, 38 | ltrniotacl 39071 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (((ocβπΎ)βπ) β π΄ β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β (β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) β ((LTrnβπΎ)βπ)) |
40 | 32, 35, 36, 37, 39 | syl112anc 1375 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ Β¬ π(leβπΎ)π) β (β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) β ((LTrnβπΎ)βπ)) |
41 | 8, 9, 18 | tendoidcl 39261 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β ( I βΎ ((LTrnβπΎ)βπ)) β ((TEndoβπΎ)βπ)) |
42 | 32, 41 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ Β¬ π(leβπΎ)π) β ( I βΎ ((LTrnβπΎ)βπ)) β ((TEndoβπΎ)βπ)) |
43 | 8, 9, 18, 11, 21 | dvhelvbasei 39580 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) β ((LTrnβπΎ)βπ) β§ ( I βΎ ((LTrnβπΎ)βπ)) β ((TEndoβπΎ)βπ))) β β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β π) |
44 | 32, 40, 42, 43 | syl12anc 836 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ Β¬ π(leβπΎ)π) β β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β π) |
45 | 6, 7, 8, 33, 9, 12, 11, 13, 38 | dih1dimc 39734 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β (πΌβπ) = (πβ{β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β©})) |
46 | 32, 36, 37, 45 | syl12anc 836 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ Β¬ π(leβπΎ)π) β (πΌβπ) = (πβ{β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β©})) |
47 | | sneq 4601 |
. . . . . . . . 9
β’ (π₯ = β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β {π₯} = {β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β©}) |
48 | 47 | fveq2d 6851 |
. . . . . . . 8
β’ (π₯ = β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β (πβ{π₯}) = (πβ{β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β©})) |
49 | 48 | rspceeqv 3600 |
. . . . . . 7
β’
((β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β π β§ (πΌβπ) = (πβ{β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β©})) β βπ₯ β π (πΌβπ) = (πβ{π₯})) |
50 | 44, 46, 49 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β π΄) β§ Β¬ π(leβπΎ)π) β βπ₯ β π (πΌβπ) = (πβ{π₯})) |
51 | 31, 50 | pm2.61dan 812 |
. . . . 5
β’ ((π β§ π β π΄) β βπ₯ β π (πΌβπ) = (πβ{π₯})) |
52 | 1 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β πΎ β HL) |
53 | 52 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯})) β πΎ β HL) |
54 | | hlatl 37851 |
. . . . . . . . . . 11
β’ (πΎ β HL β πΎ β AtLat) |
55 | 53, 54 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯})) β πΎ β AtLat) |
56 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯})) β π β π΄) |
57 | | eqid 2737 |
. . . . . . . . . . 11
β’
(0.βπΎ) =
(0.βπΎ) |
58 | 57, 7 | atn0 37799 |
. . . . . . . . . 10
β’ ((πΎ β AtLat β§ π β π΄) β π β (0.βπΎ)) |
59 | 55, 56, 58 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯})) β π β (0.βπΎ)) |
60 | | sneq 4601 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = 0 β {π₯} = { 0 }) |
61 | 60 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π₯ = 0 β (πβ{π₯}) = (πβ{ 0 })) |
62 | 61 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β (πβ{π₯}) = (πβ{ 0 })) |
63 | | simp1ll 1237 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β π) |
64 | 8, 11, 1 | dvhlmod 39602 |
. . . . . . . . . . . . . . 15
β’ (π β π β LMod) |
65 | | dihatexv.o |
. . . . . . . . . . . . . . . 16
β’ 0 =
(0gβπ) |
66 | 65, 13 | lspsn0 20485 |
. . . . . . . . . . . . . . 15
β’ (π β LMod β (πβ{ 0 }) = { 0 }) |
67 | 63, 64, 66 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β (πβ{ 0 }) = { 0 }) |
68 | 62, 67 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β (πβ{π₯}) = { 0 }) |
69 | | simp2 1138 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β (πΌβπ) = (πβ{π₯})) |
70 | 57, 8, 12, 11, 65 | dih0 39772 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ π β π») β (πΌβ(0.βπΎ)) = { 0 }) |
71 | 63, 1, 70 | 3syl 18 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β (πΌβ(0.βπΎ)) = { 0 }) |
72 | 68, 69, 71 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β (πΌβπ) = (πΌβ(0.βπΎ))) |
73 | 63, 1 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β (πΎ β HL β§ π β π»)) |
74 | | dihatexv.q |
. . . . . . . . . . . . . 14
β’ (π β π β π΅) |
75 | 63, 74 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β π β π΅) |
76 | 63, 52 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β πΎ β HL) |
77 | | hlop 37853 |
. . . . . . . . . . . . . 14
β’ (πΎ β HL β πΎ β OP) |
78 | 5, 57 | op0cl 37675 |
. . . . . . . . . . . . . 14
β’ (πΎ β OP β
(0.βπΎ) β π΅) |
79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β (0.βπΎ) β π΅) |
80 | 5, 8, 12 | dih11 39757 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ (0.βπΎ) β π΅) β ((πΌβπ) = (πΌβ(0.βπΎ)) β π = (0.βπΎ))) |
81 | 73, 75, 79, 80 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β ((πΌβπ) = (πΌβ(0.βπΎ)) β π = (0.βπΎ))) |
82 | 72, 81 | mpbid 231 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯}) β§ π₯ = 0 ) β π = (0.βπΎ)) |
83 | 82 | 3expia 1122 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯})) β (π₯ = 0 β π = (0.βπΎ))) |
84 | 83 | necon3d 2965 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯})) β (π β (0.βπΎ) β π₯ β 0 )) |
85 | 59, 84 | mpd 15 |
. . . . . . . 8
β’ ((((π β§ π β π΄) β§ π₯ β π) β§ (πΌβπ) = (πβ{π₯})) β π₯ β 0 ) |
86 | 85 | ex 414 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π₯ β π) β ((πΌβπ) = (πβ{π₯}) β π₯ β 0 )) |
87 | 86 | ancrd 553 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π₯ β π) β ((πΌβπ) = (πβ{π₯}) β (π₯ β 0 β§ (πΌβπ) = (πβ{π₯})))) |
88 | 87 | reximdva 3166 |
. . . . 5
β’ ((π β§ π β π΄) β (βπ₯ β π (πΌβπ) = (πβ{π₯}) β βπ₯ β π (π₯ β 0 β§ (πΌβπ) = (πβ{π₯})))) |
89 | 51, 88 | mpd 15 |
. . . 4
β’ ((π β§ π β π΄) β βπ₯ β π (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) |
90 | 89 | ex 414 |
. . 3
β’ (π β (π β π΄ β βπ₯ β π (π₯ β 0 β§ (πΌβπ) = (πβ{π₯})))) |
91 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β (πΎ β HL β§ π β π»)) |
92 | 74 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β π β π΅) |
93 | 5, 8, 12 | dihcnvid1 39764 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (β‘πΌβ(πΌβπ)) = π) |
94 | 91, 92, 93 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β (β‘πΌβ(πΌβπ)) = π) |
95 | | fveq2 6847 |
. . . . . . . 8
β’ ((πΌβπ) = (πβ{π₯}) β (β‘πΌβ(πΌβπ)) = (β‘πΌβ(πβ{π₯}))) |
96 | 95 | ad2antll 728 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β (β‘πΌβ(πΌβπ)) = (β‘πΌβ(πβ{π₯}))) |
97 | 94, 96 | eqtr3d 2779 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β π = (β‘πΌβ(πβ{π₯}))) |
98 | 64 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β π β LMod) |
99 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β π₯ β π) |
100 | | simprl 770 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β π₯ β 0 ) |
101 | | eqid 2737 |
. . . . . . . . 9
β’
(LSAtomsβπ) =
(LSAtomsβπ) |
102 | 21, 13, 65, 101 | lsatlspsn2 37483 |
. . . . . . . 8
β’ ((π β LMod β§ π₯ β π β§ π₯ β 0 ) β (πβ{π₯}) β (LSAtomsβπ)) |
103 | 98, 99, 100, 102 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β (πβ{π₯}) β (LSAtomsβπ)) |
104 | 7, 8, 11, 12, 101 | dihlatat 39829 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πβ{π₯}) β (LSAtomsβπ)) β (β‘πΌβ(πβ{π₯})) β π΄) |
105 | 91, 103, 104 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β (β‘πΌβ(πβ{π₯})) β π΄) |
106 | 97, 105 | eqeltrd 2838 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) β π β π΄) |
107 | 106 | ex 414 |
. . . 4
β’ ((π β§ π₯ β π) β ((π₯ β 0 β§ (πΌβπ) = (πβ{π₯})) β π β π΄)) |
108 | 107 | rexlimdva 3153 |
. . 3
β’ (π β (βπ₯ β π (π₯ β 0 β§ (πΌβπ) = (πβ{π₯})) β π β π΄)) |
109 | 90, 108 | impbid 211 |
. 2
β’ (π β (π β π΄ β βπ₯ β π (π₯ β 0 β§ (πΌβπ) = (πβ{π₯})))) |
110 | | rexdifsn 4759 |
. 2
β’
(βπ₯ β
(π β { 0 })(πΌβπ) = (πβ{π₯}) β βπ₯ β π (π₯ β 0 β§ (πΌβπ) = (πβ{π₯}))) |
111 | 109, 110 | bitr4di 289 |
1
β’ (π β (π β π΄ β βπ₯ β (π β { 0 })(πΌβπ) = (πβ{π₯}))) |