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