This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pj11

Description: One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pj11 ⊢ G ∈ C ℋ ∧ H ∈ C ℋ → proj ℎ ⁡ G = proj ℎ ⁡ H ↔ G = H

Proof

Step Hyp Ref Expression
1 fveqeq2 ⊢ G = if G ∈ C ℋ G 0 ℋ → proj ℎ ⁡ G = proj ℎ ⁡ H ↔ proj ℎ ⁡ if G ∈ C ℋ G 0 ℋ = proj ℎ ⁡ H
2 eqeq1 ⊢ G = if G ∈ C ℋ G 0 ℋ → G = H ↔ if G ∈ C ℋ G 0 ℋ = H
3 1 2 bibi12d ⊢ G = if G ∈ C ℋ G 0 ℋ → proj ℎ ⁡ G = proj ℎ ⁡ H ↔ G = H ↔ proj ℎ ⁡ if G ∈ C ℋ G 0 ℋ = proj ℎ ⁡ H ↔ if G ∈ C ℋ G 0 ℋ = H
4 fveq2 ⊢ H = if H ∈ C ℋ H 0 ℋ → proj ℎ ⁡ H = proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ
5 4 eqeq2d ⊢ H = if H ∈ C ℋ H 0 ℋ → proj ℎ ⁡ if G ∈ C ℋ G 0 ℋ = proj ℎ ⁡ H ↔ proj ℎ ⁡ if G ∈ C ℋ G 0 ℋ = proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ
6 eqeq2 ⊢ H = if H ∈ C ℋ H 0 ℋ → if G ∈ C ℋ G 0 ℋ = H ↔ if G ∈ C ℋ G 0 ℋ = if H ∈ C ℋ H 0 ℋ
7 5 6 bibi12d ⊢ H = if H ∈ C ℋ H 0 ℋ → proj ℎ ⁡ if G ∈ C ℋ G 0 ℋ = proj ℎ ⁡ H ↔ if G ∈ C ℋ G 0 ℋ = H ↔ proj ℎ ⁡ if G ∈ C ℋ G 0 ℋ = proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ↔ if G ∈ C ℋ G 0 ℋ = if H ∈ C ℋ H 0 ℋ
8 h0elch ⊢ 0 ℋ ∈ C ℋ
9 8 elimel ⊢ if G ∈ C ℋ G 0 ℋ ∈ C ℋ
10 8 elimel ⊢ if H ∈ C ℋ H 0 ℋ ∈ C ℋ
11 9 10 pj11i ⊢ proj ℎ ⁡ if G ∈ C ℋ G 0 ℋ = proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ↔ if G ∈ C ℋ G 0 ℋ = if H ∈ C ℋ H 0 ℋ
12 3 7 11 dedth2h ⊢ G ∈ C ℋ ∧ H ∈ C ℋ → proj ℎ ⁡ G = proj ℎ ⁡ H ↔ G = H