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 26559
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‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (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 26549 . 2 class
2 vg . . 3 setvar 𝑔
3 cvv 3492 . . 3 class V
4 va . . . . . . . 8 setvar 𝑎
54cv 1527 . . . . . . 7 class 𝑎
62cv 1527 . . . . . . . . 9 class 𝑔
7 cbs 16471 . . . . . . . . 9 class Base
86, 7cfv 6348 . . . . . . . 8 class (Base‘𝑔)
9 cc0 10525 . . . . . . . . 9 class 0
10 c3 11681 . . . . . . . . 9 class 3
11 cfzo 13021 . . . . . . . . 9 class ..^
129, 10, 11co 7145 . . . . . . . 8 class (0..^3)
13 cmap 8395 . . . . . . . 8 class m
148, 12, 13co 7145 . . . . . . 7 class ((Base‘𝑔) ↑m (0..^3))
155, 14wcel 2105 . . . . . 6 wff 𝑎 ∈ ((Base‘𝑔) ↑m (0..^3))
16 vb . . . . . . . 8 setvar 𝑏
1716cv 1527 . . . . . . 7 class 𝑏
1817, 14wcel 2105 . . . . . 6 wff 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))
1915, 18wa 396 . . . . 5 wff (𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3)))
20 vx . . . . . . . . 9 setvar 𝑥
2120cv 1527 . . . . . . . 8 class 𝑥
229, 17cfv 6348 . . . . . . . . 9 class (𝑏‘0)
23 c1 10526 . . . . . . . . . 10 class 1
2423, 17cfv 6348 . . . . . . . . 9 class (𝑏‘1)
25 c2 11680 . . . . . . . . . 10 class 2
2625, 17cfv 6348 . . . . . . . . 9 class (𝑏‘2)
2722, 24, 26cs3 14192 . . . . . . . 8 class ⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩
28 cinag 26548 . . . . . . . . 9 class inA
296, 28cfv 6348 . . . . . . . 8 class (inA‘𝑔)
3021, 27, 29wbr 5057 . . . . . . 7 wff 𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩
319, 5cfv 6348 . . . . . . . . 9 class (𝑎‘0)
3223, 5cfv 6348 . . . . . . . . 9 class (𝑎‘1)
3325, 5cfv 6348 . . . . . . . . 9 class (𝑎‘2)
3431, 32, 33cs3 14192 . . . . . . . 8 class ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩
3522, 24, 21cs3 14192 . . . . . . . 8 class ⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩
36 ccgra 26520 . . . . . . . . 9 class cgrA
376, 36cfv 6348 . . . . . . . 8 class (cgrA‘𝑔)
3834, 35, 37wbr 5057 . . . . . . 7 wff ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩
3930, 38wa 396 . . . . . 6 wff (𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩)
4039, 20, 8wrex 3136 . . . . 5 wff 𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩)
4119, 40wa 396 . . . 4 wff ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))
4241, 4, 16copab 5119 . . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))}
432, 3, 42cmpt 5137 . 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))})
441, 43wceq 1528 1 wff = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (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  26560
  Copyright terms: Public domain W3C validator