Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
2 | 1 | obsne0 21280 |
. . . . . 6
β’ ((π΅ β (OBasisβπ) β§ π΄ β π΅) β π΄ β (0gβπ)) |
3 | 2 | 3adant2 1132 |
. . . . 5
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β π΄ β (0gβπ)) |
4 | | elin 3965 |
. . . . . . . 8
β’ (π΄ β (πΆ β© ( β₯ βπΆ)) β (π΄ β πΆ β§ π΄ β ( β₯ βπΆ))) |
5 | | obsrcl 21278 |
. . . . . . . . . . . . . 14
β’ (π΅ β (OBasisβπ) β π β PreHil) |
6 | 5 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β π β PreHil) |
7 | | phllmod 21183 |
. . . . . . . . . . . . 13
β’ (π β PreHil β π β LMod) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β π β LMod) |
9 | | simp2 1138 |
. . . . . . . . . . . . 13
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β πΆ β π΅) |
10 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(Baseβπ) =
(Baseβπ) |
11 | 10 | obsss 21279 |
. . . . . . . . . . . . . 14
β’ (π΅ β (OBasisβπ) β π΅ β (Baseβπ)) |
12 | 11 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β π΅ β (Baseβπ)) |
13 | 9, 12 | sstrd 3993 |
. . . . . . . . . . . 12
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β πΆ β (Baseβπ)) |
14 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(LSpanβπ) =
(LSpanβπ) |
15 | 10, 14 | lspssid 20596 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ πΆ β (Baseβπ)) β πΆ β ((LSpanβπ)βπΆ)) |
16 | 8, 13, 15 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β πΆ β ((LSpanβπ)βπΆ)) |
17 | 16 | ssrind 4236 |
. . . . . . . . . 10
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (πΆ β© ( β₯ βπΆ)) β (((LSpanβπ)βπΆ) β© ( β₯ βπΆ))) |
18 | | obselocv.o |
. . . . . . . . . . . . . 14
β’ β₯ =
(ocvβπ) |
19 | 10, 18, 14 | ocvlsp 21229 |
. . . . . . . . . . . . 13
β’ ((π β PreHil β§ πΆ β (Baseβπ)) β ( β₯
β((LSpanβπ)βπΆ)) = ( β₯ βπΆ)) |
20 | 6, 13, 19 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β ( β₯
β((LSpanβπ)βπΆ)) = ( β₯ βπΆ)) |
21 | 20 | ineq2d 4213 |
. . . . . . . . . . 11
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (((LSpanβπ)βπΆ) β© ( β₯
β((LSpanβπ)βπΆ))) = (((LSpanβπ)βπΆ) β© ( β₯ βπΆ))) |
22 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(LSubSpβπ) =
(LSubSpβπ) |
23 | 10, 22, 14 | lspcl 20587 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ πΆ β (Baseβπ)) β ((LSpanβπ)βπΆ) β (LSubSpβπ)) |
24 | 8, 13, 23 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β ((LSpanβπ)βπΆ) β (LSubSpβπ)) |
25 | 18, 22, 1 | ocvin 21227 |
. . . . . . . . . . . 12
β’ ((π β PreHil β§
((LSpanβπ)βπΆ) β (LSubSpβπ)) β (((LSpanβπ)βπΆ) β© ( β₯
β((LSpanβπ)βπΆ))) = {(0gβπ)}) |
26 | 6, 24, 25 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (((LSpanβπ)βπΆ) β© ( β₯
β((LSpanβπ)βπΆ))) = {(0gβπ)}) |
27 | 21, 26 | eqtr3d 2775 |
. . . . . . . . . 10
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (((LSpanβπ)βπΆ) β© ( β₯ βπΆ)) = {(0gβπ)}) |
28 | 17, 27 | sseqtrd 4023 |
. . . . . . . . 9
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (πΆ β© ( β₯ βπΆ)) β
{(0gβπ)}) |
29 | 28 | sseld 3982 |
. . . . . . . 8
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (π΄ β (πΆ β© ( β₯ βπΆ)) β π΄ β {(0gβπ)})) |
30 | 4, 29 | biimtrrid 242 |
. . . . . . 7
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β ((π΄ β πΆ β§ π΄ β ( β₯ βπΆ)) β π΄ β {(0gβπ)})) |
31 | | elsni 4646 |
. . . . . . 7
β’ (π΄ β
{(0gβπ)}
β π΄ =
(0gβπ)) |
32 | 30, 31 | syl6 35 |
. . . . . 6
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β ((π΄ β πΆ β§ π΄ β ( β₯ βπΆ)) β π΄ = (0gβπ))) |
33 | 32 | necon3ad 2954 |
. . . . 5
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (π΄ β (0gβπ) β Β¬ (π΄ β πΆ β§ π΄ β ( β₯ βπΆ)))) |
34 | 3, 33 | mpd 15 |
. . . 4
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β Β¬ (π΄ β πΆ β§ π΄ β ( β₯ βπΆ))) |
35 | | imnan 401 |
. . . 4
β’ ((π΄ β πΆ β Β¬ π΄ β ( β₯ βπΆ)) β Β¬ (π΄ β πΆ β§ π΄ β ( β₯ βπΆ))) |
36 | 34, 35 | sylibr 233 |
. . 3
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (π΄ β πΆ β Β¬ π΄ β ( β₯ βπΆ))) |
37 | 36 | con2d 134 |
. 2
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (π΄ β ( β₯ βπΆ) β Β¬ π΄ β πΆ)) |
38 | | simpr 486 |
. . . . . . 7
β’ (((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β§ π₯ β πΆ) β π₯ β πΆ) |
39 | | eleq1 2822 |
. . . . . . 7
β’ (π΄ = π₯ β (π΄ β πΆ β π₯ β πΆ)) |
40 | 38, 39 | syl5ibrcom 246 |
. . . . . 6
β’ (((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β§ π₯ β πΆ) β (π΄ = π₯ β π΄ β πΆ)) |
41 | 40 | con3d 152 |
. . . . 5
β’ (((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β§ π₯ β πΆ) β (Β¬ π΄ β πΆ β Β¬ π΄ = π₯)) |
42 | | simpl1 1192 |
. . . . . . 7
β’ (((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β§ π₯ β πΆ) β π΅ β (OBasisβπ)) |
43 | | simpl3 1194 |
. . . . . . 7
β’ (((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β§ π₯ β πΆ) β π΄ β π΅) |
44 | 9 | sselda 3983 |
. . . . . . 7
β’ (((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β§ π₯ β πΆ) β π₯ β π΅) |
45 | | eqid 2733 |
. . . . . . . 8
β’
(Β·πβπ) =
(Β·πβπ) |
46 | | eqid 2733 |
. . . . . . . 8
β’
(Scalarβπ) =
(Scalarβπ) |
47 | | eqid 2733 |
. . . . . . . 8
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
48 | | eqid 2733 |
. . . . . . . 8
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
49 | 10, 45, 46, 47, 48 | obsip 21276 |
. . . . . . 7
β’ ((π΅ β (OBasisβπ) β§ π΄ β π΅ β§ π₯ β π΅) β (π΄(Β·πβπ)π₯) = if(π΄ = π₯, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) |
50 | 42, 43, 44, 49 | syl3anc 1372 |
. . . . . 6
β’ (((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β§ π₯ β πΆ) β (π΄(Β·πβπ)π₯) = if(π΄ = π₯, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ)))) |
51 | | iffalse 4538 |
. . . . . . 7
β’ (Β¬
π΄ = π₯ β if(π΄ = π₯, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))) =
(0gβ(Scalarβπ))) |
52 | 51 | eqeq2d 2744 |
. . . . . 6
β’ (Β¬
π΄ = π₯ β ((π΄(Β·πβπ)π₯) = if(π΄ = π₯, (1rβ(Scalarβπ)),
(0gβ(Scalarβπ))) β (π΄(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
53 | 50, 52 | syl5ibcom 244 |
. . . . 5
β’ (((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β§ π₯ β πΆ) β (Β¬ π΄ = π₯ β (π΄(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
54 | 41, 53 | syld 47 |
. . . 4
β’ (((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β§ π₯ β πΆ) β (Β¬ π΄ β πΆ β (π΄(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
55 | 54 | ralrimdva 3155 |
. . 3
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (Β¬ π΄ β πΆ β βπ₯ β πΆ (π΄(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
56 | | simp3 1139 |
. . . . 5
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β π΄ β π΅) |
57 | 12, 56 | sseldd 3984 |
. . . 4
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β π΄ β (Baseβπ)) |
58 | 10, 45, 46, 48, 18 | elocv 21221 |
. . . . . 6
β’ (π΄ β ( β₯ βπΆ) β (πΆ β (Baseβπ) β§ π΄ β (Baseβπ) β§ βπ₯ β πΆ (π΄(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
59 | | df-3an 1090 |
. . . . . 6
β’ ((πΆ β (Baseβπ) β§ π΄ β (Baseβπ) β§ βπ₯ β πΆ (π΄(Β·πβπ)π₯) = (0gβ(Scalarβπ))) β ((πΆ β (Baseβπ) β§ π΄ β (Baseβπ)) β§ βπ₯ β πΆ (π΄(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
60 | 58, 59 | bitri 275 |
. . . . 5
β’ (π΄ β ( β₯ βπΆ) β ((πΆ β (Baseβπ) β§ π΄ β (Baseβπ)) β§ βπ₯ β πΆ (π΄(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
61 | 60 | baib 537 |
. . . 4
β’ ((πΆ β (Baseβπ) β§ π΄ β (Baseβπ)) β (π΄ β ( β₯ βπΆ) β βπ₯ β πΆ (π΄(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
62 | 13, 57, 61 | syl2anc 585 |
. . 3
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (π΄ β ( β₯ βπΆ) β βπ₯ β πΆ (π΄(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
63 | 55, 62 | sylibrd 259 |
. 2
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (Β¬ π΄ β πΆ β π΄ β ( β₯ βπΆ))) |
64 | 37, 63 | impbid 211 |
1
β’ ((π΅ β (OBasisβπ) β§ πΆ β π΅ β§ π΄ β π΅) β (π΄ β ( β₯ βπΆ) β Β¬ π΄ β πΆ)) |