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	$⊢ (oc (ndx) \neq comp (ndx) \land oc (ndx) \neq Hom (ndx))$

Proof

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

Metamath Proof Explorer

Theorem slotsdifocndx

Proof