Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ⊥ ‘ 𝐻 ) = ( ⊥ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) |
2 |
1
|
eleq2d |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ 𝐴 ∈ ( ⊥ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) ) |
3 |
|
fveq2 |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( projℎ ‘ 𝐻 ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) |
4 |
3
|
fveq1d |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ‘ 𝐴 ) ) |
5 |
4
|
eqeq1d |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 0ℎ ↔ ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ‘ 𝐴 ) = 0ℎ ) ) |
6 |
2 5
|
bibi12d |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 0ℎ ) ↔ ( 𝐴 ∈ ( ⊥ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ↔ ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ‘ 𝐴 ) = 0ℎ ) ) ) |
7 |
|
eleq1 |
⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐴 ∈ ( ⊥ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ↔ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ( ⊥ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) ) |
8 |
|
fveqeq2 |
⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ‘ 𝐴 ) = 0ℎ ↔ ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = 0ℎ ) ) |
9 |
7 8
|
bibi12d |
⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( 𝐴 ∈ ( ⊥ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ↔ ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ‘ 𝐴 ) = 0ℎ ) ↔ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ( ⊥ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ↔ ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = 0ℎ ) ) ) |
10 |
|
h0elch |
⊢ 0ℋ ∈ Cℋ |
11 |
10
|
elimel |
⊢ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ∈ Cℋ |
12 |
|
ifhvhv0 |
⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ |
13 |
11 12
|
pjoc2i |
⊢ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ( ⊥ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ↔ ( ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ) = 0ℎ ) |
14 |
6 9 13
|
dedth2h |
⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 0ℎ ) ) |