# Metamath Proof Explorer

## Definition df-inag

Description: Definition of the geometrical "in angle" relation. (Contributed by Thierry Arnoux, 15-Aug-2020)

Ref Expression
Assertion df-inag ${⊢}{\in }_{𝒢}^{\angle }=\left({g}\in \mathrm{V}⟼\left\{⟨{p},{t}⟩|\left(\left({p}\in {\mathrm{Base}}_{{g}}\wedge {t}\in \left({{\mathrm{Base}}_{{g}}}^{\left(0..^3\right)}\right)\right)\wedge \left(\left({t}\left(0\right)\ne {t}\left(1\right)\wedge {t}\left(2\right)\ne {t}\left(1\right)\wedge {p}\ne {t}\left(1\right)\right)\wedge \exists {x}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({t}\left(0\right)\mathrm{Itv}\left({g}\right){t}\left(2\right)\right)\wedge \left({x}={t}\left(1\right)\vee {x}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right){p}\right)\right)\right)\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cinag ${class}{\in }_{𝒢}^{\angle }$
1 vg ${setvar}{g}$
2 cvv ${class}\mathrm{V}$
3 vp ${setvar}{p}$
4 vt ${setvar}{t}$
5 3 cv ${setvar}{p}$
6 cbs ${class}\mathrm{Base}$
7 1 cv ${setvar}{g}$
8 7 6 cfv ${class}{\mathrm{Base}}_{{g}}$
9 5 8 wcel ${wff}{p}\in {\mathrm{Base}}_{{g}}$
10 4 cv ${setvar}{t}$
11 cmap ${class}{↑}_{𝑚}$
12 cc0 ${class}0$
13 cfzo ${class}..^$
14 c3 ${class}3$
15 12 14 13 co ${class}\left(0..^3\right)$
16 8 15 11 co ${class}\left({{\mathrm{Base}}_{{g}}}^{\left(0..^3\right)}\right)$
17 10 16 wcel ${wff}{t}\in \left({{\mathrm{Base}}_{{g}}}^{\left(0..^3\right)}\right)$
18 9 17 wa ${wff}\left({p}\in {\mathrm{Base}}_{{g}}\wedge {t}\in \left({{\mathrm{Base}}_{{g}}}^{\left(0..^3\right)}\right)\right)$
19 12 10 cfv ${class}{t}\left(0\right)$
20 c1 ${class}1$
21 20 10 cfv ${class}{t}\left(1\right)$
22 19 21 wne ${wff}{t}\left(0\right)\ne {t}\left(1\right)$
23 c2 ${class}2$
24 23 10 cfv ${class}{t}\left(2\right)$
25 24 21 wne ${wff}{t}\left(2\right)\ne {t}\left(1\right)$
26 5 21 wne ${wff}{p}\ne {t}\left(1\right)$
27 22 25 26 w3a ${wff}\left({t}\left(0\right)\ne {t}\left(1\right)\wedge {t}\left(2\right)\ne {t}\left(1\right)\wedge {p}\ne {t}\left(1\right)\right)$
28 vx ${setvar}{x}$
29 28 cv ${setvar}{x}$
30 citv ${class}\mathrm{Itv}$
31 7 30 cfv ${class}\mathrm{Itv}\left({g}\right)$
32 19 24 31 co ${class}\left({t}\left(0\right)\mathrm{Itv}\left({g}\right){t}\left(2\right)\right)$
33 29 32 wcel ${wff}{x}\in \left({t}\left(0\right)\mathrm{Itv}\left({g}\right){t}\left(2\right)\right)$
34 29 21 wceq ${wff}{x}={t}\left(1\right)$
35 chlg ${class}{hl}_{𝒢}$
36 7 35 cfv ${class}{hl}_{𝒢}\left({g}\right)$
37 21 36 cfv ${class}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right)$
38 29 5 37 wbr ${wff}{x}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right){p}$
39 34 38 wo ${wff}\left({x}={t}\left(1\right)\vee {x}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right){p}\right)$
40 33 39 wa ${wff}\left({x}\in \left({t}\left(0\right)\mathrm{Itv}\left({g}\right){t}\left(2\right)\right)\wedge \left({x}={t}\left(1\right)\vee {x}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right){p}\right)\right)$
41 40 28 8 wrex ${wff}\exists {x}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({t}\left(0\right)\mathrm{Itv}\left({g}\right){t}\left(2\right)\right)\wedge \left({x}={t}\left(1\right)\vee {x}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right){p}\right)\right)$
42 27 41 wa ${wff}\left(\left({t}\left(0\right)\ne {t}\left(1\right)\wedge {t}\left(2\right)\ne {t}\left(1\right)\wedge {p}\ne {t}\left(1\right)\right)\wedge \exists {x}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({t}\left(0\right)\mathrm{Itv}\left({g}\right){t}\left(2\right)\right)\wedge \left({x}={t}\left(1\right)\vee {x}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right){p}\right)\right)\right)$
43 18 42 wa ${wff}\left(\left({p}\in {\mathrm{Base}}_{{g}}\wedge {t}\in \left({{\mathrm{Base}}_{{g}}}^{\left(0..^3\right)}\right)\right)\wedge \left(\left({t}\left(0\right)\ne {t}\left(1\right)\wedge {t}\left(2\right)\ne {t}\left(1\right)\wedge {p}\ne {t}\left(1\right)\right)\wedge \exists {x}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({t}\left(0\right)\mathrm{Itv}\left({g}\right){t}\left(2\right)\right)\wedge \left({x}={t}\left(1\right)\vee {x}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right){p}\right)\right)\right)\right)$
44 43 3 4 copab ${class}\left\{⟨{p},{t}⟩|\left(\left({p}\in {\mathrm{Base}}_{{g}}\wedge {t}\in \left({{\mathrm{Base}}_{{g}}}^{\left(0..^3\right)}\right)\right)\wedge \left(\left({t}\left(0\right)\ne {t}\left(1\right)\wedge {t}\left(2\right)\ne {t}\left(1\right)\wedge {p}\ne {t}\left(1\right)\right)\wedge \exists {x}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({t}\left(0\right)\mathrm{Itv}\left({g}\right){t}\left(2\right)\right)\wedge \left({x}={t}\left(1\right)\vee {x}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right){p}\right)\right)\right)\right)\right\}$
45 1 2 44 cmpt ${class}\left({g}\in \mathrm{V}⟼\left\{⟨{p},{t}⟩|\left(\left({p}\in {\mathrm{Base}}_{{g}}\wedge {t}\in \left({{\mathrm{Base}}_{{g}}}^{\left(0..^3\right)}\right)\right)\wedge \left(\left({t}\left(0\right)\ne {t}\left(1\right)\wedge {t}\left(2\right)\ne {t}\left(1\right)\wedge {p}\ne {t}\left(1\right)\right)\wedge \exists {x}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({t}\left(0\right)\mathrm{Itv}\left({g}\right){t}\left(2\right)\right)\wedge \left({x}={t}\left(1\right)\vee {x}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right){p}\right)\right)\right)\right)\right\}\right)$
46 0 45 wceq ${wff}{\in }_{𝒢}^{\angle }=\left({g}\in \mathrm{V}⟼\left\{⟨{p},{t}⟩|\left(\left({p}\in {\mathrm{Base}}_{{g}}\wedge {t}\in \left({{\mathrm{Base}}_{{g}}}^{\left(0..^3\right)}\right)\right)\wedge \left(\left({t}\left(0\right)\ne {t}\left(1\right)\wedge {t}\left(2\right)\ne {t}\left(1\right)\wedge {p}\ne {t}\left(1\right)\right)\wedge \exists {x}\in {\mathrm{Base}}_{{g}}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({t}\left(0\right)\mathrm{Itv}\left({g}\right){t}\left(2\right)\right)\wedge \left({x}={t}\left(1\right)\vee {x}{hl}_{𝒢}\left({g}\right)\left({t}\left(1\right)\right){p}\right)\right)\right)\right)\right\}\right)$