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

Definition df-leag 25532
 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 25527 . 2 class
2 vg . . 3 setvar 𝑔
3 cvv 3173 . . 3 class V
4 va . . . . . . . 8 setvar 𝑎
54cv 1474 . . . . . . 7 class 𝑎
62cv 1474 . . . . . . . . 9 class 𝑔
7 cbs 15695 . . . . . . . . 9 class Base
86, 7cfv 5804 . . . . . . . 8 class (Base‘𝑔)
9 cc0 9815 . . . . . . . . 9 class 0
10 c3 10948 . . . . . . . . 9 class 3
11 cfzo 12334 . . . . . . . . 9 class ..^
129, 10, 11co 6549 . . . . . . . 8 class (0..^3)
13 cmap 7744 . . . . . . . 8 class 𝑚
148, 12, 13co 6549 . . . . . . 7 class ((Base‘𝑔) ↑𝑚 (0..^3))
155, 14wcel 1977 . . . . . 6 wff 𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))
16 vb . . . . . . . 8 setvar 𝑏
1716cv 1474 . . . . . . 7 class 𝑏
1817, 14wcel 1977 . . . . . 6 wff 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))
1915, 18wa 383 . . . . 5 wff (𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)))
20 vx . . . . . . . . 9 setvar 𝑥
2120cv 1474 . . . . . . . 8 class 𝑥
229, 17cfv 5804 . . . . . . . . 9 class (𝑏‘0)
23 c1 9816 . . . . . . . . . 10 class 1
2423, 17cfv 5804 . . . . . . . . 9 class (𝑏‘1)
25 c2 10947 . . . . . . . . . 10 class 2
2625, 17cfv 5804 . . . . . . . . 9 class (𝑏‘2)
2722, 24, 26cs3 13438 . . . . . . . 8 class ⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩
28 cinag 25526 . . . . . . . . 9 class inA
296, 28cfv 5804 . . . . . . . 8 class (inA‘𝑔)
3021, 27, 29wbr 4583 . . . . . . 7 wff 𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩
319, 5cfv 5804 . . . . . . . . 9 class (𝑎‘0)
3223, 5cfv 5804 . . . . . . . . 9 class (𝑎‘1)
3325, 5cfv 5804 . . . . . . . . 9 class (𝑎‘2)
3431, 32, 33cs3 13438 . . . . . . . 8 class ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩
3522, 24, 21cs3 13438 . . . . . . . 8 class ⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩
36 ccgra 25499 . . . . . . . . 9 class cgrA
376, 36cfv 5804 . . . . . . . 8 class (cgrA‘𝑔)
3834, 35, 37wbr 4583 . . . . . . 7 wff ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩
3930, 38wa 383 . . . . . 6 wff (𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩)
4039, 20, 8wrex 2897 . . . . 5 wff 𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩)
4119, 40wa 383 . . . 4 wff ((𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))
4241, 4, 16copab 4642 . . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))}
432, 3, 42cmpt 4643 . 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑𝑚 (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))})
441, 43wceq 1475 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  25533
 Copyright terms: Public domain W3C validator