Metamath Proof Explorer

Theorem pjpreeq

Description: Equality with a projection. This version of pjeq does not assume the Axiom of Choice via pjhth . (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjpreeq ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→projℎ⁡H⁡A=B↔B∈H∧∃x∈⊥⁡HA=B+ℎx

Proof

Step Hyp Ref Expression
1 chsh ⊢H∈Cℋ→H∈Sℋ
2 shocsh ⊢H∈Sℋ→⊥⁡H∈Sℋ
3 shsel ⊢H∈Sℋ∧⊥⁡H∈Sℋ→A∈H+ℋ⊥⁡H↔∃y∈H∃x∈⊥⁡HA=y+ℎx
4 1 2 3 syl2anc2 ⊢H∈Cℋ→A∈H+ℋ⊥⁡H↔∃y∈H∃x∈⊥⁡HA=y+ℎx
5 4 biimpa ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→∃y∈H∃x∈⊥⁡HA=y+ℎx
6 1 2 syl ⊢H∈Cℋ→⊥⁡H∈Sℋ
7 ocin ⊢H∈Sℋ→H∩⊥⁡H=0ℋ
8 1 7 syl ⊢H∈Cℋ→H∩⊥⁡H=0ℋ
9 pjhthmo ⊢H∈Sℋ∧⊥⁡H∈Sℋ∧H∩⊥⁡H=0ℋ→∃*yy∈H∧∃x∈⊥⁡HA=y+ℎx
10 1 6 8 9 syl3anc ⊢H∈Cℋ→∃*yy∈H∧∃x∈⊥⁡HA=y+ℎx
11 10 adantr ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→∃*yy∈H∧∃x∈⊥⁡HA=y+ℎx
12 reu5 ⊢∃!y∈H∃x∈⊥⁡HA=y+ℎx↔∃y∈H∃x∈⊥⁡HA=y+ℎx∧∃*y∈H∃x∈⊥⁡HA=y+ℎx
13 df-rmo ⊢∃*y∈H∃x∈⊥⁡HA=y+ℎx↔∃*yy∈H∧∃x∈⊥⁡HA=y+ℎx
14 13 anbi2i ⊢∃y∈H∃x∈⊥⁡HA=y+ℎx∧∃*y∈H∃x∈⊥⁡HA=y+ℎx↔∃y∈H∃x∈⊥⁡HA=y+ℎx∧∃*yy∈H∧∃x∈⊥⁡HA=y+ℎx
15 12 14 bitri ⊢∃!y∈H∃x∈⊥⁡HA=y+ℎx↔∃y∈H∃x∈⊥⁡HA=y+ℎx∧∃*yy∈H∧∃x∈⊥⁡HA=y+ℎx
16 5 11 15 sylanbrc ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→∃!y∈H∃x∈⊥⁡HA=y+ℎx
17 riotacl ⊢∃!y∈H∃x∈⊥⁡HA=y+ℎx→ιy∈H|∃x∈⊥⁡HA=y+ℎx∈H
18 16 17 syl ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→ιy∈H|∃x∈⊥⁡HA=y+ℎx∈H
19 eleq1 ⊢ιy∈H|∃x∈⊥⁡HA=y+ℎx=B→ιy∈H|∃x∈⊥⁡HA=y+ℎx∈H↔B∈H
20 18 19 syl5ibcom ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→ιy∈H|∃x∈⊥⁡HA=y+ℎx=B→B∈H
21 20 pm4.71rd ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→ιy∈H|∃x∈⊥⁡HA=y+ℎx=B↔B∈H∧ιy∈H|∃x∈⊥⁡HA=y+ℎx=B
22 shsss ⊢H∈Sℋ∧⊥⁡H∈Sℋ→H+ℋ⊥⁡H⊆ℋ
23 1 2 22 syl2anc2 ⊢H∈Cℋ→H+ℋ⊥⁡H⊆ℋ
24 23 sselda ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→A∈ℋ
25 pjhval ⊢H∈Cℋ∧A∈ℋ→projℎ⁡H⁡A=ιy∈H|∃x∈⊥⁡HA=y+ℎx
26 24 25 syldan ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→projℎ⁡H⁡A=ιy∈H|∃x∈⊥⁡HA=y+ℎx
27 26 eqeq1d ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→projℎ⁡H⁡A=B↔ιy∈H|∃x∈⊥⁡HA=y+ℎx=B
28 id ⊢B∈H→B∈H
29 oveq1 ⊢y=B→y+ℎx=B+ℎx
30 29 eqeq2d ⊢y=B→A=y+ℎx↔A=B+ℎx
31 30 rexbidv ⊢y=B→∃x∈⊥⁡HA=y+ℎx↔∃x∈⊥⁡HA=B+ℎx
32 31 riota2 ⊢B∈H∧∃!y∈H∃x∈⊥⁡HA=y+ℎx→∃x∈⊥⁡HA=B+ℎx↔ιy∈H|∃x∈⊥⁡HA=y+ℎx=B
33 28 16 32 syl2anr ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H∧B∈H→∃x∈⊥⁡HA=B+ℎx↔ιy∈H|∃x∈⊥⁡HA=y+ℎx=B
34 33 pm5.32da ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→B∈H∧∃x∈⊥⁡HA=B+ℎx↔B∈H∧ιy∈H|∃x∈⊥⁡HA=y+ℎx=B
35 21 27 34 3bitr4d ⊢H∈Cℋ∧A∈H+ℋ⊥⁡H→projℎ⁡H⁡A=B↔B∈H∧∃x∈⊥⁡HA=B+ℎx