# 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 ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={B}↔\left({B}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={B}{+}_{ℎ}{x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 chsh ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to {H}\in {\mathbf{S}}_{ℋ}$
2 shocsh ${⊢}{H}\in {\mathbf{S}}_{ℋ}\to \perp \left({H}\right)\in {\mathbf{S}}_{ℋ}$
3 shsel ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge \perp \left({H}\right)\in {\mathbf{S}}_{ℋ}\right)\to \left({A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)↔\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)$
4 1 2 3 syl2anc2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to \left({A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)↔\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)$
5 4 biimpa ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to \exists {y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}$
6 1 2 syl ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to \perp \left({H}\right)\in {\mathbf{S}}_{ℋ}$
7 ocin ${⊢}{H}\in {\mathbf{S}}_{ℋ}\to {H}\cap \perp \left({H}\right)={0}_{ℋ}$
8 1 7 syl ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to {H}\cap \perp \left({H}\right)={0}_{ℋ}$
9 pjhthmo ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge \perp \left({H}\right)\in {\mathbf{S}}_{ℋ}\wedge {H}\cap \perp \left({H}\right)={0}_{ℋ}\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)$
10 1 6 8 9 syl3anc ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)$
11 10 adantr ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)$
12 reu5 ${⊢}\exists !{y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}↔\left(\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\wedge {\exists }^{*}{y}\in {H}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)$
13 df-rmo ${⊢}{\exists }^{*}{y}\in {H}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)$
14 13 anbi2i ${⊢}\left(\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\wedge {\exists }^{*}{y}\in {H}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)↔\left(\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\wedge {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)\right)$
15 12 14 bitri ${⊢}\exists !{y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}↔\left(\exists {y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\wedge {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)\right)$
16 5 11 15 sylanbrc ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to \exists !{y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}$
17 riotacl ${⊢}\exists !{y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\to \left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)\in {H}$
18 16 17 syl ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to \left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)\in {H}$
19 eleq1 ${⊢}\left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)={B}\to \left(\left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)\in {H}↔{B}\in {H}\right)$
20 18 19 syl5ibcom ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to \left(\left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)={B}\to {B}\in {H}\right)$
21 20 pm4.71rd ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to \left(\left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)={B}↔\left({B}\in {H}\wedge \left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)={B}\right)\right)$
22 shsss ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge \perp \left({H}\right)\in {\mathbf{S}}_{ℋ}\right)\to {H}{+}_{ℋ}\perp \left({H}\right)\subseteq ℋ$
23 1 2 22 syl2anc2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to {H}{+}_{ℋ}\perp \left({H}\right)\subseteq ℋ$
24 23 sselda ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to {A}\in ℋ$
25 pjhval ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)=\left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)$
26 24 25 syldan ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)=\left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)$
27 26 eqeq1d ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={B}↔\left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)={B}\right)$
28 id ${⊢}{B}\in {H}\to {B}\in {H}$
29 oveq1 ${⊢}{y}={B}\to {y}{+}_{ℎ}{x}={B}{+}_{ℎ}{x}$
30 29 eqeq2d ${⊢}{y}={B}\to \left({A}={y}{+}_{ℎ}{x}↔{A}={B}{+}_{ℎ}{x}\right)$
31 30 rexbidv ${⊢}{y}={B}\to \left(\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}↔\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={B}{+}_{ℎ}{x}\right)$
32 31 riota2 ${⊢}\left({B}\in {H}\wedge \exists !{y}\in {H}\phantom{\rule{.4em}{0ex}}\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)\to \left(\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={B}{+}_{ℎ}{x}↔\left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)={B}\right)$
33 28 16 32 syl2anr ${⊢}\left(\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\wedge {B}\in {H}\right)\to \left(\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={B}{+}_{ℎ}{x}↔\left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)={B}\right)$
34 33 pm5.32da ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to \left(\left({B}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={B}{+}_{ℎ}{x}\right)↔\left({B}\in {H}\wedge \left(\iota {y}\in {H}|\exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={y}{+}_{ℎ}{x}\right)={B}\right)\right)$
35 21 27 34 3bitr4d ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \left({H}{+}_{ℋ}\perp \left({H}\right)\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={B}↔\left({B}\in {H}\wedge \exists {x}\in \perp \left({H}\right)\phantom{\rule{.4em}{0ex}}{A}={B}{+}_{ℎ}{x}\right)\right)$