Metamath Proof Explorer

Theorem pjhval

Description: Value of a projection. (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion pjhval ⊢H∈Cℋ∧A∈ℋ→projℎ⁡H⁡A=ιx∈H|∃y∈⊥⁡HA=x+ℎy

Proof

Step Hyp Ref Expression
1 pjhfval ⊢H∈Cℋ→projℎ⁡H=z∈ℋ⟼ιx∈H|∃y∈⊥⁡Hz=x+ℎy
2 1 fveq1d ⊢H∈Cℋ→projℎ⁡H⁡A=z∈ℋ⟼ιx∈H|∃y∈⊥⁡Hz=x+ℎy⁡A
3 eqeq1 ⊢z=A→z=x+ℎy↔A=x+ℎy
4 3 rexbidv ⊢z=A→∃y∈⊥⁡Hz=x+ℎy↔∃y∈⊥⁡HA=x+ℎy
5 4 riotabidv ⊢z=A→ιx∈H|∃y∈⊥⁡Hz=x+ℎy=ιx∈H|∃y∈⊥⁡HA=x+ℎy
6 eqid ⊢z∈ℋ⟼ιx∈H|∃y∈⊥⁡Hz=x+ℎy=z∈ℋ⟼ιx∈H|∃y∈⊥⁡Hz=x+ℎy
7 riotaex ⊢ιx∈H|∃y∈⊥⁡HA=x+ℎy∈V
8 5 6 7 fvmpt ⊢A∈ℋ→z∈ℋ⟼ιx∈H|∃y∈⊥⁡Hz=x+ℎy⁡A=ιx∈H|∃y∈⊥⁡HA=x+ℎy
9 2 8 sylan9eq ⊢H∈Cℋ∧A∈ℋ→projℎ⁡H⁡A=ιx∈H|∃y∈⊥⁡HA=x+ℎy