Metamath Proof Explorer

Definition df-angmgm

Description: Definition of the angle addition magma. See following theorems for better readable properties. Because the textbook's definition of angle congruence does not consider orientation (cf. cgraswap ) , our notion of angle does not include reflex angles (angles larger than a straight angle). Therefore, like with NN0 , at this point, we can only build amagma , which is e.g.not isomorphic with the rotation group SO(2) . (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Assertion df-angmgm AngMgm = ( 𝑔 ∈ V ↦ ⦋ ( Base ‘ 𝑔 ) / 𝑝 ⦌ ⦋ { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } / 𝑎 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝑔 ) ⟩ } /s ( cgrA ‘ 𝑔 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cangmgm ⊢ AngMgm
1 vg ⊢ 𝑔
2 cvv ⊢ V
3 cbs ⊢ Base
4 1 cv ⊢ 𝑔
5 4 3 cfv ⊢ ( Base ‘ 𝑔 )
6 vp ⊢ 𝑝
7 vd ⊢ 𝑑
8 6 cv ⊢ 𝑝
9 cmap ⊢ ↑m
10 cc0 ⊢ 0
11 cfzo ⊢ ..^
12 c3 ⊢ 3
13 10 12 11 co ⊢ ( 0 ..^ 3 )
14 8 13 9 co ⊢ ( 𝑝 ↑m ( 0 ..^ 3 ) )
15 7 cv ⊢ 𝑑
16 10 15 cfv ⊢ ( 𝑑 ‘ 0 )
17 c1 ⊢ 1
18 17 15 cfv ⊢ ( 𝑑 ‘ 1 )
19 16 18 wne ⊢ ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 )
20 c2 ⊢ 2
21 20 15 cfv ⊢ ( 𝑑 ‘ 2 )
22 18 21 wne ⊢ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 )
23 19 22 wa ⊢ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) )
24 23 7 14 crab ⊢ { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
25 va ⊢ 𝑎
26 cnx ⊢ ndx
27 26 3 cfv ⊢ ( Base ‘ ndx )
28 25 cv ⊢ 𝑎
29 27 28 cop ⊢ ⟨ ( Base ‘ ndx ) , 𝑎 ⟩
30 cplusg ⊢ +g
31 26 30 cfv ⊢ ( +g ‘ ndx )
32 ve ⊢ 𝑒
33 vf ⊢ 𝑓
34 32 cv ⊢ 𝑒
35 10 34 cfv ⊢ ( 𝑒 ‘ 0 )
36 17 34 cfv ⊢ ( 𝑒 ‘ 1 )
37 clng ⊢ LineG
38 4 37 cfv ⊢ ( LineG ‘ 𝑔 )
39 20 34 cfv ⊢ ( 𝑒 ‘ 2 )
40 36 39 38 co ⊢ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) )
41 35 40 wcel ⊢ ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) )
42 33 cv ⊢ 𝑓
43 10 42 cfv ⊢ ( 𝑓 ‘ 0 )
44 17 42 cfv ⊢ ( 𝑓 ‘ 1 )
45 vz ⊢ 𝑧
46 20 42 cfv ⊢ ( 𝑓 ‘ 2 )
47 45 cv ⊢ 𝑧
48 46 44 47 cs3 ⊢ ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩
49 ccgra ⊢ cgrA
50 4 49 cfv ⊢ ( cgrA ‘ 𝑔 )
51 48 34 50 wbr ⊢ ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒
52 cds ⊢ dist
53 4 52 cfv ⊢ ( dist ‘ 𝑔 )
54 44 47 53 co ⊢ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 )
55 36 35 53 co ⊢ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) )
56 54 55 wceq ⊢ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) )
57 51 56 wa ⊢ ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) )
58 57 45 8 crio ⊢ ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) )
59 43 44 58 cs3 ⊢ ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩
60 39 36 47 cs3 ⊢ ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩
61 60 42 50 wbr ⊢ ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓
62 36 47 53 co ⊢ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 )
63 44 43 53 co ⊢ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) )
64 62 63 wceq ⊢ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) )
65 citv ⊢ Itv
66 4 65 cfv ⊢ ( Itv ‘ 𝑔 )
67 47 35 66 co ⊢ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) )
68 40 67 cin ⊢ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) )
69 c0 ⊢ ∅
70 68 69 wne ⊢ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅
71 61 64 70 w3a ⊢ ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ )
72 71 45 8 crio ⊢ ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) )
73 35 36 72 cs3 ⊢ ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩
74 41 59 73 cif ⊢ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ )
75 32 33 28 28 74 cmpo ⊢ ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
76 31 75 cop ⊢ ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩
77 cple ⊢ le
78 26 77 cfv ⊢ ( le ‘ ndx )
79 cleag ⊢ ≤∠
80 4 79 cfv ⊢ ( ≤∠ ‘ 𝑔 )
81 78 80 cop ⊢ ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝑔 ) ⟩
82 29 76 81 ctp ⊢ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝑔 ) ⟩ }
83 cqus ⊢ /s
84 82 50 83 co ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝑔 ) ⟩ } /s ( cgrA ‘ 𝑔 ) )
85 25 24 84 csb ⊢ ⦋ { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } / 𝑎 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝑔 ) ⟩ } /s ( cgrA ‘ 𝑔 ) )
86 6 5 85 csb ⊢ ⦋ ( Base ‘ 𝑔 ) / 𝑝 ⦌ ⦋ { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } / 𝑎 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝑔 ) ⟩ } /s ( cgrA ‘ 𝑔 ) )
87 1 2 86 cmpt ⊢ ( 𝑔 ∈ V ↦ ⦋ ( Base ‘ 𝑔 ) / 𝑝 ⦌ ⦋ { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } / 𝑎 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝑔 ) ⟩ } /s ( cgrA ‘ 𝑔 ) ) )
88 0 87 wceq ⊢ AngMgm = ( 𝑔 ∈ V ↦ ⦋ ( Base ‘ 𝑔 ) / 𝑝 ⦌ ⦋ { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } / 𝑎 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑧 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑧 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑧 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑧 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝑔 ) ⟩ } /s ( cgrA ‘ 𝑔 ) ) )