Theorem jplem1

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

	Ref	Expression
Hypothesis	jplem1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		jplem1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjnorm2	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge u\in \mathscr{H}\right)\to \left(u\in A\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)={norm}_{ℎ}\left(u\right)\right)$$
3	1 2	mpan	$$⊢u\in \mathscr{H}\to \left(u\in A\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)={norm}_{ℎ}\left(u\right)\right)$$
4		eqeq2	$$⊢{norm}_{ℎ}\left(u\right)=1\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)={norm}_{ℎ}\left(u\right)\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)=1\right)$$
5	3 4	sylan9bb	$$⊢\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)=1\right)$$
6		sq1	$$⊢1^2=1$$
7	6	eqeq2i	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2=1^2\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2=1$$
8	1	pjhcli	$$⊢u\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\in \mathscr{H}$$
9		normcl	$$⊢{\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)\in ℝ$$
10	8 9	syl	$$⊢u\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)\in ℝ$$
11		normge0	$$⊢{\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)$$
12	8 11	syl	$$⊢u\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)$$
13		1re	$$⊢1\in ℝ$$
14		0le1	$$⊢0\le 1$$
15		sq11	$$⊢\left(\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)\right)\wedge \left(1\in ℝ\wedge 0\le 1\right)\right)\to \left({{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2=1^2\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)=1\right)$$
16	13 14 15	mpanr12	$$⊢\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)\right)\to \left({{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2=1^2\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)=1\right)$$
17	10 12 16	syl2anc	$$⊢u\in \mathscr{H}\to \left({{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2=1^2\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)=1\right)$$
18	7 17	bitr3id	$$⊢u\in \mathscr{H}\to \left({{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2=1\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)=1\right)$$
19	18	adantr	$$⊢\left(u\in \mathscr{H}\wedge {norm}_{ℎ}\left(u\right)=1\right)\to \left({{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)}^2=1\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(u\right)\right)=1\right)$$
20	5 19	bitr4d	$$⊢\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)$$