Step | Hyp | Ref
| Expression |
1 | | cssmre.v |
. . . . . 6
β’ π = (Baseβπ) |
2 | | cssmre.c |
. . . . . 6
β’ πΆ = (ClSubSpβπ) |
3 | 1, 2 | cssss 21105 |
. . . . 5
β’ (π₯ β πΆ β π₯ β π) |
4 | | velpw 4570 |
. . . . 5
β’ (π₯ β π« π β π₯ β π) |
5 | 3, 4 | sylibr 233 |
. . . 4
β’ (π₯ β πΆ β π₯ β π« π) |
6 | 5 | a1i 11 |
. . 3
β’ (π β PreHil β (π₯ β πΆ β π₯ β π« π)) |
7 | 6 | ssrdv 3955 |
. 2
β’ (π β PreHil β πΆ β π« π) |
8 | 1, 2 | css1 21110 |
. 2
β’ (π β PreHil β π β πΆ) |
9 | | intss1 4929 |
. . . . . . . . . . . 12
β’ (π§ β π₯ β β© π₯ β π§) |
10 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(ocvβπ) =
(ocvβπ) |
11 | 10 | ocv2ss 21093 |
. . . . . . . . . . . 12
β’ (β© π₯
β π§ β
((ocvβπ)βπ§) β ((ocvβπ)ββ© π₯)) |
12 | 10 | ocv2ss 21093 |
. . . . . . . . . . . 12
β’
(((ocvβπ)βπ§) β ((ocvβπ)ββ© π₯) β ((ocvβπ)β((ocvβπ)ββ© π₯))
β ((ocvβπ)β((ocvβπ)βπ§))) |
13 | 9, 11, 12 | 3syl 18 |
. . . . . . . . . . 11
β’ (π§ β π₯ β ((ocvβπ)β((ocvβπ)ββ© π₯)) β ((ocvβπ)β((ocvβπ)βπ§))) |
14 | 13 | ad2antll 728 |
. . . . . . . . . 10
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ (π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯)) β§ π§ β π₯)) β ((ocvβπ)β((ocvβπ)ββ© π₯)) β ((ocvβπ)β((ocvβπ)βπ§))) |
15 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ (π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯)) β§ π§ β π₯)) β π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯))) |
16 | 14, 15 | sseldd 3950 |
. . . . . . . . 9
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ (π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯)) β§ π§ β π₯)) β π¦ β ((ocvβπ)β((ocvβπ)βπ§))) |
17 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ (π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯)) β§ π§ β π₯)) β π₯ β πΆ) |
18 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ (π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯)) β§ π§ β π₯)) β π§ β π₯) |
19 | 17, 18 | sseldd 3950 |
. . . . . . . . . 10
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ (π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯)) β§ π§ β π₯)) β π§ β πΆ) |
20 | 10, 2 | cssi 21104 |
. . . . . . . . . 10
β’ (π§ β πΆ β π§ = ((ocvβπ)β((ocvβπ)βπ§))) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ (π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯)) β§ π§ β π₯)) β π§ = ((ocvβπ)β((ocvβπ)βπ§))) |
22 | 16, 21 | eleqtrrd 2841 |
. . . . . . . 8
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ (π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯)) β§ π§ β π₯)) β π¦ β π§) |
23 | 22 | expr 458 |
. . . . . . 7
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯))) β (π§ β π₯ β π¦ β π§)) |
24 | 23 | alrimiv 1931 |
. . . . . 6
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯))) β βπ§(π§ β π₯ β π¦ β π§)) |
25 | | vex 3452 |
. . . . . . 7
β’ π¦ β V |
26 | 25 | elint 4918 |
. . . . . 6
β’ (π¦ β β© π₯
β βπ§(π§ β π₯ β π¦ β π§)) |
27 | 24, 26 | sylibr 233 |
. . . . 5
β’ (((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β§ π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯))) β π¦ β β© π₯) |
28 | 27 | ex 414 |
. . . 4
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β (π¦ β ((ocvβπ)β((ocvβπ)ββ© π₯)) β π¦ β β© π₯)) |
29 | 28 | ssrdv 3955 |
. . 3
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β ((ocvβπ)β((ocvβπ)ββ© π₯))
β β© π₯) |
30 | | simp1 1137 |
. . . 4
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β π β PreHil) |
31 | | intssuni 4936 |
. . . . . 6
β’ (π₯ β β
β β© π₯
β βͺ π₯) |
32 | 31 | 3ad2ant3 1136 |
. . . . 5
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β β© π₯
β βͺ π₯) |
33 | | simp2 1138 |
. . . . . . 7
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β π₯ β πΆ) |
34 | 7 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β πΆ β π« π) |
35 | 33, 34 | sstrd 3959 |
. . . . . 6
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β π₯ β π« π) |
36 | | sspwuni 5065 |
. . . . . 6
β’ (π₯ β π« π β βͺ π₯
β π) |
37 | 35, 36 | sylib 217 |
. . . . 5
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β βͺ π₯
β π) |
38 | 32, 37 | sstrd 3959 |
. . . 4
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β β© π₯
β π) |
39 | 1, 2, 10 | iscss2 21106 |
. . . 4
β’ ((π β PreHil β§ β© π₯
β π) β (β© π₯
β πΆ β
((ocvβπ)β((ocvβπ)ββ© π₯)) β β© π₯)) |
40 | 30, 38, 39 | syl2anc 585 |
. . 3
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β (β© π₯
β πΆ β
((ocvβπ)β((ocvβπ)ββ© π₯)) β β© π₯)) |
41 | 29, 40 | mpbird 257 |
. 2
β’ ((π β PreHil β§ π₯ β πΆ β§ π₯ β β
) β β© π₯
β πΆ) |
42 | 7, 8, 41 | ismred 17489 |
1
β’ (π β PreHil β πΆ β (Mooreβπ)) |