Step |
Hyp |
Ref |
Expression |
1 |
|
fveqeq2 |
⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) → ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) ↔ ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ 𝐻 ) ) ) |
2 |
|
eqeq1 |
⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) → ( 𝐺 = 𝐻 ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = 𝐻 ) ) |
3 |
1 2
|
bibi12d |
⊢ ( 𝐺 = if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) → ( ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) ↔ 𝐺 = 𝐻 ) ↔ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ 𝐻 ) ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = 𝐻 ) ) ) |
4 |
|
fveq2 |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( projℎ ‘ 𝐻 ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) |
5 |
4
|
eqeq2d |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ 𝐻 ) ↔ ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) ) |
6 |
|
eqeq2 |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = 𝐻 ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) |
7 |
5 6
|
bibi12d |
⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ 𝐻 ) ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = 𝐻 ) ↔ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ) ) |
8 |
|
h0elch |
⊢ 0ℋ ∈ Cℋ |
9 |
8
|
elimel |
⊢ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ∈ Cℋ |
10 |
8
|
elimel |
⊢ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ∈ Cℋ |
11 |
9 10
|
pj11i |
⊢ ( ( projℎ ‘ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ↔ if ( 𝐺 ∈ Cℋ , 𝐺 , 0ℋ ) = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) |
12 |
3 7 11
|
dedth2h |
⊢ ( ( 𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ) → ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ 𝐻 ) ↔ 𝐺 = 𝐻 ) ) |