Step |
Hyp |
Ref |
Expression |
1 |
|
h1deot.1 |
|- B e. ~H |
2 |
|
snssi |
|- ( B e. ~H -> { B } C_ ~H ) |
3 |
|
occl |
|- ( { B } C_ ~H -> ( _|_ ` { B } ) e. CH ) |
4 |
1 2 3
|
mp2b |
|- ( _|_ ` { B } ) e. CH |
5 |
4
|
chssii |
|- ( _|_ ` { B } ) C_ ~H |
6 |
|
ocel |
|- ( ( _|_ ` { B } ) C_ ~H -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 ) ) ) |
7 |
5 6
|
ax-mp |
|- ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 ) ) |
8 |
1
|
h1deoi |
|- ( x e. ( _|_ ` { B } ) <-> ( x e. ~H /\ ( x .ih B ) = 0 ) ) |
9 |
|
orthcom |
|- ( ( x e. ~H /\ B e. ~H ) -> ( ( x .ih B ) = 0 <-> ( B .ih x ) = 0 ) ) |
10 |
1 9
|
mpan2 |
|- ( x e. ~H -> ( ( x .ih B ) = 0 <-> ( B .ih x ) = 0 ) ) |
11 |
10
|
pm5.32i |
|- ( ( x e. ~H /\ ( x .ih B ) = 0 ) <-> ( x e. ~H /\ ( B .ih x ) = 0 ) ) |
12 |
8 11
|
bitri |
|- ( x e. ( _|_ ` { B } ) <-> ( x e. ~H /\ ( B .ih x ) = 0 ) ) |
13 |
12
|
imbi1i |
|- ( ( x e. ( _|_ ` { B } ) -> ( A .ih x ) = 0 ) <-> ( ( x e. ~H /\ ( B .ih x ) = 0 ) -> ( A .ih x ) = 0 ) ) |
14 |
|
impexp |
|- ( ( ( x e. ~H /\ ( B .ih x ) = 0 ) -> ( A .ih x ) = 0 ) <-> ( x e. ~H -> ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) ) |
15 |
13 14
|
bitri |
|- ( ( x e. ( _|_ ` { B } ) -> ( A .ih x ) = 0 ) <-> ( x e. ~H -> ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) ) |
16 |
15
|
ralbii2 |
|- ( A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 <-> A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) |
17 |
16
|
anbi2i |
|- ( ( A e. ~H /\ A. x e. ( _|_ ` { B } ) ( A .ih x ) = 0 ) <-> ( A e. ~H /\ A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) ) |
18 |
7 17
|
bitri |
|- ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) ) |