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 ∈ ⊥ ⁡ H A = 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 ∈ ⊥ ⁡ H A = y + ℎ x
4 1 2 3 syl2anc2 ⊢ H ∈ C ℋ → A ∈ H + ℋ ⊥ ⁡ H ↔ ∃ y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x
5 4 biimpa ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → ∃ y ∈ H ∃ x ∈ ⊥ ⁡ H A = 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 ℋ → ∃* y y ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = y + ℎ x
10 1 6 8 9 syl3anc ⊢ H ∈ C ℋ → ∃* y y ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = y + ℎ x
11 10 adantr ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → ∃* y y ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = y + ℎ x
12 reu5 ⊢ ∃! y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ↔ ∃ y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ∧ ∃* y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x
13 df-rmo ⊢ ∃* y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ↔ ∃* y y ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = y + ℎ x
14 13 anbi2i ⊢ ∃ y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ∧ ∃* y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ↔ ∃ y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ∧ ∃* y y ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = y + ℎ x
15 12 14 bitri ⊢ ∃! y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ↔ ∃ y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ∧ ∃* y y ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = y + ℎ x
16 5 11 15 sylanbrc ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → ∃! y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x
17 riotacl ⊢ ∃! y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x → ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ∈ H
18 16 17 syl ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ∈ H
19 eleq1 ⊢ ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = y + ℎ x = B → ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = y + ℎ x ∈ H ↔ B ∈ H
20 18 19 syl5ibcom ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = y + ℎ x = B → B ∈ H
21 20 pm4.71rd ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = y + ℎ x = B ↔ B ∈ H ∧ ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = 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 ∈ ⊥ ⁡ H A = y + ℎ x
26 24 25 syldan ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → proj ℎ ⁡ H ⁡ A = ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = y + ℎ x
27 26 eqeq1d ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → proj ℎ ⁡ H ⁡ A = B ↔ ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = 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 ∈ ⊥ ⁡ H A = y + ℎ x ↔ ∃ x ∈ ⊥ ⁡ H A = B + ℎ x
32 31 riota2 ⊢ B ∈ H ∧ ∃! y ∈ H ∃ x ∈ ⊥ ⁡ H A = y + ℎ x → ∃ x ∈ ⊥ ⁡ H A = B + ℎ x ↔ ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = y + ℎ x = B
33 28 16 32 syl2anr ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H ∧ B ∈ H → ∃ x ∈ ⊥ ⁡ H A = B + ℎ x ↔ ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = y + ℎ x = B
34 33 pm5.32da ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → B ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = B + ℎ x ↔ B ∈ H ∧ ι y ∈ H | ∃ x ∈ ⊥ ⁡ H A = y + ℎ x = B
35 21 27 34 3bitr4d ⊢ H ∈ C ℋ ∧ A ∈ H + ℋ ⊥ ⁡ H → proj ℎ ⁡ H ⁡ A = B ↔ B ∈ H ∧ ∃ x ∈ ⊥ ⁡ H A = B + ℎ x