Theorem jplem2

Description: Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001) (New usage is discouraged.)

	Ref	Expression
Hypotheses	jp.1	$$⊢S=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)$$
	jp.2	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	jplem2	$$⊢\left(u\in \mathscr{H}\wedge {norm}_{ℎ}\left(u\right)=1\right)\to \left(u\in A\leftrightarrow S\left(A\right)=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		jp.1	$$⊢S=\left(x\in {\mathbf{C}}_{\mathscr{H}}⟼{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(x\right)\left(u\right)\right)}^2\right)$$
2		jp.2	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
3	2	jplem1	$$⊢\left(u\in \mathscr{H}\wedge {norm}_{ℎ}\left(u\right)=1\right)\to \left(u\in A\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2=1\right)$$
4	1	strlem2	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to S\left(A\right)={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2$$
5	2 4	ax-mp	$$⊢S\left(A\right)={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2$$
6	5	eqeq1i	$$⊢S\left(A\right)=1\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2=1$$
7	3 6	bitr4di	$$⊢\left(u\in \mathscr{H}\wedge {norm}_{ℎ}\left(u\right)=1\right)\to \left(u\in A\leftrightarrow S\left(A\right)=1\right)$$