Metamath Proof Explorer


Theorem pj11i

Description: One-to-one correspondence of projection and subspace. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjsumt.1 G C
pjsumt.2 H C
Assertion pj11i proj G = proj H G = H

Proof

Step Hyp Ref Expression
1 pjsumt.1 G C
2 pjsumt.2 H C
3 rneq proj G = proj H ran proj G = ran proj H
4 1 pjrni ran proj G = G
5 2 pjrni ran proj H = H
6 3 4 5 3eqtr3g proj G = proj H G = H
7 fveq2 G = H proj G = proj H
8 6 7 impbii proj G = proj H G = H