Step | Hyp | Ref
| Expression |
1 | | isobs.v |
. . . . . 6
β’ π = (Baseβπ) |
2 | | isobs.h |
. . . . . 6
β’ , =
(Β·πβπ) |
3 | | isobs.f |
. . . . . 6
β’ πΉ = (Scalarβπ) |
4 | | isobs.u |
. . . . . 6
β’ 1 =
(1rβπΉ) |
5 | | isobs.z |
. . . . . 6
β’ 0 =
(0gβπΉ) |
6 | | eqid 2736 |
. . . . . 6
β’
(ocvβπ) =
(ocvβπ) |
7 | | eqid 2736 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
8 | 1, 2, 3, 4, 5, 6, 7 | isobs 21126 |
. . . . 5
β’ (π΅ β (OBasisβπ) β (π β PreHil β§ π΅ β π β§ (βπ₯ β π΅ βπ¦ β π΅ (π₯ , π¦) = if(π₯ = π¦, 1 , 0 ) β§ ((ocvβπ)βπ΅) = {(0gβπ)}))) |
9 | 8 | simp3bi 1147 |
. . . 4
β’ (π΅ β (OBasisβπ) β (βπ₯ β π΅ βπ¦ β π΅ (π₯ , π¦) = if(π₯ = π¦, 1 , 0 ) β§ ((ocvβπ)βπ΅) = {(0gβπ)})) |
10 | 9 | simpld 495 |
. . 3
β’ (π΅ β (OBasisβπ) β βπ₯ β π΅ βπ¦ β π΅ (π₯ , π¦) = if(π₯ = π¦, 1 , 0 )) |
11 | | oveq1 7364 |
. . . . 5
β’ (π₯ = π β (π₯ , π¦) = (π , π¦)) |
12 | | eqeq1 2740 |
. . . . . 6
β’ (π₯ = π β (π₯ = π¦ β π = π¦)) |
13 | 12 | ifbid 4509 |
. . . . 5
β’ (π₯ = π β if(π₯ = π¦, 1 , 0 ) = if(π = π¦, 1 , 0 )) |
14 | 11, 13 | eqeq12d 2752 |
. . . 4
β’ (π₯ = π β ((π₯ , π¦) = if(π₯ = π¦, 1 , 0 ) β (π , π¦) = if(π = π¦, 1 , 0 ))) |
15 | | oveq2 7365 |
. . . . 5
β’ (π¦ = π β (π , π¦) = (π , π)) |
16 | | eqeq2 2748 |
. . . . . 6
β’ (π¦ = π β (π = π¦ β π = π)) |
17 | 16 | ifbid 4509 |
. . . . 5
β’ (π¦ = π β if(π = π¦, 1 , 0 ) = if(π = π, 1 , 0 )) |
18 | 15, 17 | eqeq12d 2752 |
. . . 4
β’ (π¦ = π β ((π , π¦) = if(π = π¦, 1 , 0 ) β (π , π) = if(π = π, 1 , 0 ))) |
19 | 14, 18 | rspc2v 3590 |
. . 3
β’ ((π β π΅ β§ π β π΅) β (βπ₯ β π΅ βπ¦ β π΅ (π₯ , π¦) = if(π₯ = π¦, 1 , 0 ) β (π , π) = if(π = π, 1 , 0 ))) |
20 | 10, 19 | syl5com 31 |
. 2
β’ (π΅ β (OBasisβπ) β ((π β π΅ β§ π β π΅) β (π , π) = if(π = π, 1 , 0 ))) |
21 | 20 | 3impib 1116 |
1
β’ ((π΅ β (OBasisβπ) β§ π β π΅ β§ π β π΅) β (π , π) = if(π = π, 1 , 0 )) |