pjhtheu2

Description: Uniqueness of y for the projection theorem. (Contributed by NM, 6-Nov-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

		Ref	Expression
	Assertion	pjhtheu2	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to \exists! y \in ⊥ (H) \exists x \in H A = x +_{ℎ} y$

Proof

Step	Hyp	Ref	Expression
1		choccl	$⊢ H \in C_{ℋ} \to ⊥ (H) \in C_{ℋ}$
2		pjhtheu	$⊢ (⊥ (H) \in C_{ℋ} \land A \in ℋ) \to \exists! y \in ⊥ (H) \exists x \in ⊥ (⊥ (H)) A = y +_{ℎ} x$
3	1 2	sylan	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to \exists! y \in ⊥ (H) \exists x \in ⊥ (⊥ (H)) A = y +_{ℎ} x$
4		simpll	$⊢ ((H \in C_{ℋ} \land A \in ℋ) \land y \in ⊥ (H)) \to H \in C_{ℋ}$
5		ococ	$⊢ H \in C_{ℋ} \to ⊥ (⊥ (H)) = H$
6	4 5	syl	$⊢ ((H \in C_{ℋ} \land A \in ℋ) \land y \in ⊥ (H)) \to ⊥ (⊥ (H)) = H$
7	6	rexeqdv	$⊢ ((H \in C_{ℋ} \land A \in ℋ) \land y \in ⊥ (H)) \to (\exists x \in ⊥ (⊥ (H)) A = y +_{ℎ} x \leftrightarrow \exists x \in H A = y +_{ℎ} x)$
8	1	adantr	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to ⊥ (H) \in C_{ℋ}$
9		chel	$⊢ (⊥ (H) \in C_{ℋ} \land y \in ⊥ (H)) \to y \in ℋ$
10	8 9	sylan	$⊢ ((H \in C_{ℋ} \land A \in ℋ) \land y \in ⊥ (H)) \to y \in ℋ$
11	10	adantr	$⊢ (((H \in C_{ℋ} \land A \in ℋ) \land y \in ⊥ (H)) \land x \in H) \to y \in ℋ$
12		chel	$⊢ (H \in C_{ℋ} \land x \in H) \to x \in ℋ$
13	4 12	sylan	$⊢ (((H \in C_{ℋ} \land A \in ℋ) \land y \in ⊥ (H)) \land x \in H) \to x \in ℋ$
14		ax-hvcom	$⊢ (y \in ℋ \land x \in ℋ) \to y +_{ℎ} x = x +_{ℎ} y$
15	11 13 14	syl2anc	$⊢ (((H \in C_{ℋ} \land A \in ℋ) \land y \in ⊥ (H)) \land x \in H) \to y +_{ℎ} x = x +_{ℎ} y$
16	15	eqeq2d	$⊢ (((H \in C_{ℋ} \land A \in ℋ) \land y \in ⊥ (H)) \land x \in H) \to (A = y +_{ℎ} x \leftrightarrow A = x +_{ℎ} y)$
17	16	rexbidva	$⊢ ((H \in C_{ℋ} \land A \in ℋ) \land y \in ⊥ (H)) \to (\exists x \in H A = y +_{ℎ} x \leftrightarrow \exists x \in H A = x +_{ℎ} y)$
18	7 17	bitrd	$⊢ ((H \in C_{ℋ} \land A \in ℋ) \land y \in ⊥ (H)) \to (\exists x \in ⊥ (⊥ (H)) A = y +_{ℎ} x \leftrightarrow \exists x \in H A = x +_{ℎ} y)$
19	18	reubidva	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to (\exists! y \in ⊥ (H) \exists x \in ⊥ (⊥ (H)) A = y +_{ℎ} x \leftrightarrow \exists! y \in ⊥ (H) \exists x \in H A = x +_{ℎ} y)$
20	3 19	mpbid	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to \exists! y \in ⊥ (H) \exists x \in H A = x +_{ℎ} y$

Metamath Proof Explorer

Theorem pjhtheu2

Proof