Theorem slotsdifocndx

Description: The index of the slot for the orthocomplementation is not the index of other slots. Formerly part of proof for prstcocval . (Contributed by AV, 12-Nov-2024)

	Ref	Expression
Assertion	slotsdifocndx	$$⊢\left(\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		1nn	$$⊢1\in \mathbb{N}$$
3	1 2	decnncl	$$⊢11\in \mathbb{N}$$
4	3	nnrei	$$⊢11\in ℝ$$
5		5nn	$$⊢5\in \mathbb{N}$$
6		1lt5	$$⊢1<5$$
7	1 1 5 6	declt	$$⊢11<15$$
8	4 7	ltneii	$$⊢11\ne 15$$
9		ocndx	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)=11$$
10		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
11	9 10	neeq12i	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\leftrightarrow 11\ne 15$$
12	8 11	mpbir	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
13		4nn	$$⊢4\in \mathbb{N}$$
14		1lt4	$$⊢1<4$$
15	1 1 13 14	declt	$$⊢11<14$$
16	4 15	ltneii	$$⊢11\ne 14$$
17		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
18	9 17	neeq12i	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\leftrightarrow 11\ne 14$$
19	16 18	mpbir	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
20	12 19	pm3.2i	$$⊢\left(\mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{oc}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\right)$$