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

Definition df-leag 26649
 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 26639 . 2 class
2 vg . . 3 setvar 𝑔
3 cvv 3480 . . 3 class V
4 va . . . . . . . 8 setvar 𝑎
54cv 1537 . . . . . . 7 class 𝑎
62cv 1537 . . . . . . . . 9 class 𝑔
7 cbs 16485 . . . . . . . . 9 class Base
86, 7cfv 6345 . . . . . . . 8 class (Base‘𝑔)
9 cc0 10537 . . . . . . . . 9 class 0
10 c3 11692 . . . . . . . . 9 class 3
11 cfzo 13039 . . . . . . . . 9 class ..^
129, 10, 11co 7151 . . . . . . . 8 class (0..^3)
13 cmap 8404 . . . . . . . 8 class m
148, 12, 13co 7151 . . . . . . 7 class ((Base‘𝑔) ↑m (0..^3))
155, 14wcel 2115 . . . . . 6 wff 𝑎 ∈ ((Base‘𝑔) ↑m (0..^3))
16 vb . . . . . . . 8 setvar 𝑏
1716cv 1537 . . . . . . 7 class 𝑏
1817, 14wcel 2115 . . . . . 6 wff 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))
1915, 18wa 399 . . . . 5 wff (𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3)))
20 vx . . . . . . . . 9 setvar 𝑥
2120cv 1537 . . . . . . . 8 class 𝑥
229, 17cfv 6345 . . . . . . . . 9 class (𝑏‘0)
23 c1 10538 . . . . . . . . . 10 class 1
2423, 17cfv 6345 . . . . . . . . 9 class (𝑏‘1)
25 c2 11691 . . . . . . . . . 10 class 2
2625, 17cfv 6345 . . . . . . . . 9 class (𝑏‘2)
2722, 24, 26cs3 14206 . . . . . . . 8 class ⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩
28 cinag 26638 . . . . . . . . 9 class inA
296, 28cfv 6345 . . . . . . . 8 class (inA‘𝑔)
3021, 27, 29wbr 5053 . . . . . . 7 wff 𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩
319, 5cfv 6345 . . . . . . . . 9 class (𝑎‘0)
3223, 5cfv 6345 . . . . . . . . 9 class (𝑎‘1)
3325, 5cfv 6345 . . . . . . . . 9 class (𝑎‘2)
3431, 32, 33cs3 14206 . . . . . . . 8 class ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩
3522, 24, 21cs3 14206 . . . . . . . 8 class ⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩
36 ccgra 26610 . . . . . . . . 9 class cgrA
376, 36cfv 6345 . . . . . . . 8 class (cgrA‘𝑔)
3834, 35, 37wbr 5053 . . . . . . 7 wff ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩
3930, 38wa 399 . . . . . 6 wff (𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩)
4039, 20, 8wrex 3134 . . . . 5 wff 𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩)
4119, 40wa 399 . . . 4 wff ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))
4241, 4, 16copab 5115 . . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))}
432, 3, 42cmpt 5133 . 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))})
441, 43wceq 1538 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  26650
 Copyright terms: Public domain W3C validator