Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | eqid 2733 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
3 | | dihatlat.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
4 | | dihatlat.h |
. . . . 5
β’ π» = (LHypβπΎ) |
5 | | eqid 2733 |
. . . . 5
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
6 | | eqid 2733 |
. . . . 5
β’ (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) = (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) |
7 | | dihatlat.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
8 | | dihatlat.i |
. . . . 5
β’ πΌ = ((DIsoHβπΎ)βπ) |
9 | | eqid 2733 |
. . . . 5
β’
(LSpanβπ) =
(LSpanβπ) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | dih1dimb2 39754 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π(leβπΎ)π)) β βπ β ((LTrnβπΎ)βπ)(π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©}))) |
11 | 10 | anassrs 469 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π) β βπ β ((LTrnβπΎ)βπ)(π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©}))) |
12 | | simp3rr 1248 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})) |
13 | | simp1l 1198 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β (πΎ β HL β§ π β π»)) |
14 | 4, 7, 13 | dvhlmod 39623 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β π β LMod) |
15 | | simp3l 1202 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β π β ((LTrnβπΎ)βπ)) |
16 | | eqid 2733 |
. . . . . . . . 9
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
17 | 1, 4, 5, 16, 6 | tendo0cl 39303 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) β ((TEndoβπΎ)βπ)) |
18 | 13, 17 | syl 17 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) β ((TEndoβπΎ)βπ)) |
19 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
20 | 4, 5, 16, 7, 19 | dvhelvbasei 39601 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) β ((TEndoβπΎ)βπ))) β β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β
(Baseβπ)) |
21 | 13, 15, 18, 20 | syl12anc 836 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β
β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β
(Baseβπ)) |
22 | | simp3rl 1247 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β π β ( I βΎ
(BaseβπΎ))) |
23 | 22 | neneqd 2945 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β Β¬
π = ( I βΎ
(BaseβπΎ))) |
24 | 23 | intnanrd 491 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β Β¬
(π = ( I βΎ
(BaseβπΎ)) β§
(π β
((LTrnβπΎ)βπ) β¦ ( I βΎ
(BaseβπΎ))) = (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))))) |
25 | | vex 3451 |
. . . . . . . . . 10
β’ π β V |
26 | | fvex 6859 |
. . . . . . . . . . 11
β’
((LTrnβπΎ)βπ) β V |
27 | 26 | mptex 7177 |
. . . . . . . . . 10
β’ (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) β V |
28 | 25, 27 | opth 5437 |
. . . . . . . . 9
β’
(β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© = β¨( I βΎ
(BaseβπΎ)), (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β (π = ( I βΎ (BaseβπΎ)) β§ (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) = (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))))) |
29 | 28 | necon3abii 2987 |
. . . . . . . 8
β’
(β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β β¨( I βΎ
(BaseβπΎ)), (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β Β¬ (π = ( I βΎ (BaseβπΎ)) β§ (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) = (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))))) |
30 | 24, 29 | sylibr 233 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β
β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β β¨( I βΎ
(BaseβπΎ)), (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©) |
31 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
32 | 1, 4, 5, 7, 31, 6 | dvh0g 39624 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (0gβπ) = β¨( I βΎ
(BaseβπΎ)), (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©) |
33 | 13, 32 | syl 17 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β
(0gβπ) =
β¨( I βΎ (BaseβπΎ)), (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©) |
34 | 30, 33 | neeqtrrd 3015 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β
β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β
(0gβπ)) |
35 | | dihatlat.l |
. . . . . . 7
β’ πΏ = (LSAtomsβπ) |
36 | 19, 9, 31, 35 | lsatlspsn2 37504 |
. . . . . 6
β’ ((π β LMod β§ β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β
(Baseβπ) β§
β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β
(0gβπ))
β ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©}) β πΏ) |
37 | 14, 21, 34, 36 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β
((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©}) β πΏ) |
38 | 12, 37 | eqeltrd 2834 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β (πΌβπ) β πΏ) |
39 | 38 | 3expa 1119 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ π β π΄) β§ π(leβπΎ)π) β§ (π β ((LTrnβπΎ)βπ) β§ (π β ( I βΎ (BaseβπΎ)) β§ (πΌβπ) = ((LSpanβπ)β{β¨π, (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©})))) β (πΌβπ) β πΏ) |
40 | 11, 39 | rexlimddv 3155 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ π(leβπΎ)π) β (πΌβπ) β πΏ) |
41 | | eqid 2733 |
. . . . 5
β’
((ocβπΎ)βπ) = ((ocβπΎ)βπ) |
42 | | eqid 2733 |
. . . . 5
β’
(β©π
β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) = (β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) |
43 | 2, 3, 4, 41, 5, 8,
7, 9, 42 | dih1dimc 39755 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β (πΌβπ) = ((LSpanβπ)β{β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β©})) |
44 | 43 | anassrs 469 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β (πΌβπ) = ((LSpanβπ)β{β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β©})) |
45 | | simpll 766 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β (πΎ β HL β§ π β π»)) |
46 | 4, 7, 45 | dvhlmod 39623 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β π β LMod) |
47 | | eqid 2733 |
. . . . . . . 8
β’
(ocβπΎ) =
(ocβπΎ) |
48 | 2, 47, 3, 4 | lhpocnel 38531 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (((ocβπΎ)βπ) β π΄ β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π)) |
49 | 48 | ad2antrr 725 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β (((ocβπΎ)βπ) β π΄ β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π)) |
50 | | simplr 768 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β π β π΄) |
51 | | simpr 486 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β Β¬ π(leβπΎ)π) |
52 | 2, 3, 4, 5, 42 | ltrniotacl 39092 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (((ocβπΎ)βπ) β π΄ β§ Β¬ ((ocβπΎ)βπ)(leβπΎ)π) β§ (π β π΄ β§ Β¬ π(leβπΎ)π)) β (β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) β ((LTrnβπΎ)βπ)) |
53 | 45, 49, 50, 51, 52 | syl112anc 1375 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β (β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) β ((LTrnβπΎ)βπ)) |
54 | 4, 5, 16 | tendoidcl 39282 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ( I βΎ ((LTrnβπΎ)βπ)) β ((TEndoβπΎ)βπ)) |
55 | 54 | ad2antrr 725 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β ( I βΎ ((LTrnβπΎ)βπ)) β ((TEndoβπΎ)βπ)) |
56 | 4, 5, 16, 7, 19 | dvhelvbasei 39601 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) β ((LTrnβπΎ)βπ) β§ ( I βΎ ((LTrnβπΎ)βπ)) β ((TEndoβπΎ)βπ))) β β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β (Baseβπ)) |
57 | 45, 53, 55, 56 | syl12anc 836 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β (Baseβπ)) |
58 | 1, 4, 5, 16, 6 | tendo1ne0 39341 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β ( I βΎ ((LTrnβπΎ)βπ)) β (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))) |
59 | 58 | ad2antrr 725 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β ( I βΎ ((LTrnβπΎ)βπ)) β (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))) |
60 | 59 | neneqd 2945 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β Β¬ ( I βΎ
((LTrnβπΎ)βπ)) = (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))) |
61 | 60 | intnand 490 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β Β¬ ((β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) = ( I βΎ (BaseβπΎ)) β§ ( I βΎ
((LTrnβπΎ)βπ)) = (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))))) |
62 | | riotaex 7321 |
. . . . . . . 8
β’
(β©π
β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) β V |
63 | | resiexg 7855 |
. . . . . . . . 9
β’
(((LTrnβπΎ)βπ) β V β ( I βΎ
((LTrnβπΎ)βπ)) β V) |
64 | 26, 63 | ax-mp 5 |
. . . . . . . 8
β’ ( I
βΎ ((LTrnβπΎ)βπ)) β V |
65 | 62, 64 | opth 5437 |
. . . . . . 7
β’
(β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© = β¨( I βΎ
(BaseβπΎ)), (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β
((β©π β
((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) = ( I βΎ (BaseβπΎ)) β§ ( I βΎ
((LTrnβπΎ)βπ)) = (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))))) |
66 | 65 | necon3abii 2987 |
. . . . . 6
β’
(β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β β¨( I βΎ
(BaseβπΎ)), (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β© β Β¬
((β©π β
((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π) = ( I βΎ (BaseβπΎ)) β§ ( I βΎ
((LTrnβπΎ)βπ)) = (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))))) |
67 | 61, 66 | sylibr 233 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β β¨( I βΎ
(BaseβπΎ)), (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©) |
68 | 32 | ad2antrr 725 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β (0gβπ) = β¨( I βΎ
(BaseβπΎ)), (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ)))β©) |
69 | 67, 68 | neeqtrrd 3015 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β (0gβπ)) |
70 | 19, 9, 31, 35 | lsatlspsn2 37504 |
. . . 4
β’ ((π β LMod β§
β¨(β©π
β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β (Baseβπ) β§
β¨(β©π
β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β© β (0gβπ)) β ((LSpanβπ)β{β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β©}) β πΏ) |
71 | 46, 57, 69, 70 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β ((LSpanβπ)β{β¨(β©π β ((LTrnβπΎ)βπ)(πβ((ocβπΎ)βπ)) = π), ( I βΎ ((LTrnβπΎ)βπ))β©}) β πΏ) |
72 | 44, 71 | eqeltrd 2834 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β π΄) β§ Β¬ π(leβπΎ)π) β (πΌβπ) β πΏ) |
73 | 40, 72 | pm2.61dan 812 |
1
β’ (((πΎ β HL β§ π β π») β§ π β π΄) β (πΌβπ) β πΏ) |