MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-leag Structured version   Visualization version   GIF version

Definition df-leag 25450
Description: Definition of the geometrical "angle less than" relation. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.)
Assertion
Ref Expression
df-leag = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))})
Distinct variable group:   𝑎,𝑏,𝑔,𝑥

Detailed syntax breakdown of Definition df-leag
StepHypRef Expression
1 cleag 25445 . 2 class
2 vg . . 3 setvar 𝑔
3 cvv 3172 . . 3 class V
4 va . . . . . . . 8 setvar 𝑎
54cv 1473 . . . . . . 7 class 𝑎
62cv 1473 . . . . . . . . 9 class 𝑔
7 cbs 15641 . . . . . . . . 9 class Base
86, 7cfv 5790 . . . . . . . 8 class (Base‘𝑔)
9 cc0 9792 . . . . . . . . 9 class 0
10 c3 10918 . . . . . . . . 9 class 3
11 cfzo 12289 . . . . . . . . 9 class ..^
129, 10, 11co 6527 . . . . . . . 8 class (0..^3)
13 cmap 7721 . . . . . . . 8 class 𝑚
148, 12, 13co 6527 . . . . . . 7 class ((Base‘𝑔) ↑𝑚 (0..^3))
155, 14wcel 1976 . . . . . 6 wff 𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))
16 vb . . . . . . . 8 setvar 𝑏
1716cv 1473 . . . . . . 7 class 𝑏
1817, 14wcel 1976 . . . . . 6 wff 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))
1915, 18wa 382 . . . . 5 wff (𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)))
20 vx . . . . . . . . 9 setvar 𝑥
2120cv 1473 . . . . . . . 8 class 𝑥
229, 17cfv 5790 . . . . . . . . 9 class (𝑏‘0)
23 c1 9793 . . . . . . . . . 10 class 1
2423, 17cfv 5790 . . . . . . . . 9 class (𝑏‘1)
25 c2 10917 . . . . . . . . . 10 class 2
2625, 17cfv 5790 . . . . . . . . 9 class (𝑏‘2)
2722, 24, 26cs3 13384 . . . . . . . 8 class ⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩
28 cinag 25444 . . . . . . . . 9 class inA
296, 28cfv 5790 . . . . . . . 8 class (inA‘𝑔)
3021, 27, 29wbr 4577 . . . . . . 7 wff 𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩
319, 5cfv 5790 . . . . . . . . 9 class (𝑎‘0)
3223, 5cfv 5790 . . . . . . . . 9 class (𝑎‘1)
3325, 5cfv 5790 . . . . . . . . 9 class (𝑎‘2)
3431, 32, 33cs3 13384 . . . . . . . 8 class ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩
3522, 24, 21cs3 13384 . . . . . . . 8 class ⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩
36 ccgra 25417 . . . . . . . . 9 class cgrA
376, 36cfv 5790 . . . . . . . 8 class (cgrA‘𝑔)
3834, 35, 37wbr 4577 . . . . . . 7 wff ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩
3930, 38wa 382 . . . . . 6 wff (𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩)
4039, 20, 8wrex 2896 . . . . 5 wff 𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩)
4119, 40wa 382 . . . 4 wff ((𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))
4241, 4, 16copab 4636 . . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))}
432, 3, 42cmpt 4637 . 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))})
441, 43wceq 1474 1 wff = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))})
Colors of variables: wff setvar class
This definition is referenced by:  isleag  25451
  Copyright terms: Public domain W3C validator