Metamath Proof Explorer

Theorem angmgmval

Description: Explicit the value of the angle addition magma for a given geometry G . (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses angmgmval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
angmgmval.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
angmgmval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
angmgmval.d ⊢ − = ( dist ‘ 𝐺 )
angmgmval.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
angmgmval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
angmgmval.o ⊢ + = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
angmgmval.j ⊢ 𝐽 = ( AngMgm ‘ 𝐺 )
angmgmval.s ⊢ ≤ = ( ≤∠ ‘ 𝐺 )
Assertion angmgmval ( 𝐺 ∈ 𝑉 → 𝐽 = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } /s ∼ ) )

Proof

Step Hyp Ref Expression
1 angmgmval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 angmgmval.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3 angmgmval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 angmgmval.d ⊢ − = ( dist ‘ 𝐺 )
5 angmgmval.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
6 angmgmval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
7 angmgmval.o ⊢ + = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
8 angmgmval.j ⊢ 𝐽 = ( AngMgm ‘ 𝐺 )
9 angmgmval.s ⊢ ≤ = ( ≤∠ ‘ 𝐺 )
10 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 ‘ 𝑔 ) ) )
11 fvexd ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) ∈ V )
12 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
13 12 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
14 eqid ⊢ { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } = { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
15 ovexd ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) → ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∈ V )
16 14 15 rabexd ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) → { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } ∈ V )
17 oveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ↑m ( 0 ..^ 3 ) ) = ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
18 17 adantl ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) → ( 𝑝 ↑m ( 0 ..^ 3 ) ) = ( 𝑃 ↑m ( 0 ..^ 3 ) ) )
19 18 rabeqdv ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) → { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } )
20 19 2 eqtr4di ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) → { 𝑑 ∈ ( 𝑝 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) } = 𝐴 )
21 opeq2 ⊢ ( 𝑎 = 𝐴 → ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ )
22 21 adantl ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ )
23 simpr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → 𝑎 = 𝐴 )
24 fveq2 ⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) )
25 24 ad2antrr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) )
26 25 6 eqtr4di ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( LineG ‘ 𝑔 ) = 𝐿 )
27 26 oveqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) = ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) )
28 27 eleq2d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ↔ ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ) )
29 eqidd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 0 ) )
30 eqidd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( 𝑓 ‘ 1 ) = ( 𝑓 ‘ 1 ) )
31 simplr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → 𝑝 = 𝑃 )
32 fveq2 ⊢ ( 𝑔 = 𝐺 → ( cgrA ‘ 𝑔 ) = ( cgrA ‘ 𝐺 ) )
33 32 5 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( cgrA ‘ 𝑔 ) = ∼ )
34 33 ad2antrr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( cgrA ‘ 𝑔 ) = ∼ )
35 34 breqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ↔ ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ) )
36 fveq2 ⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = ( dist ‘ 𝐺 ) )
37 36 4 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = − )
38 37 ad2antrr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( dist ‘ 𝑔 ) = − )
39 38 oveqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑠 ) = ( ( 𝑓 ‘ 1 ) − 𝑠 ) )
40 38 oveqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) )
41 39 40 eqeq12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑠 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) )
42 35 41 anbi12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑠 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ↔ ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) )
43 31 42 riotaeqbidv ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ℩ 𝑠 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑠 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) = ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) )
44 29 30 43 s3eqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑝 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ( cgrA ‘ 𝑔 ) 𝑒 ∧ ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑠 ) = ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ) ”⟩ = ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ )
45 eqidd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( 𝑒 ‘ 0 ) = ( 𝑒 ‘ 0 ) )
46 eqidd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( 𝑒 ‘ 1 ) = ( 𝑒 ‘ 1 ) )
47 34 breqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ↔ ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ) )
48 38 oveqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑠 ) = ( ( 𝑒 ‘ 1 ) − 𝑠 ) )
49 38 oveqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) )
50 48 49 eqeq12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑠 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ↔ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ) )
51 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = ( Itv ‘ 𝐺 ) )
52 51 3 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = 𝐼 )
53 52 ad2antrr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( Itv ‘ 𝑔 ) = 𝐼 )
54 53 oveqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( 𝑠 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) = ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) )
55 27 54 ineq12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) = ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) )
56 55 neeq1d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ↔ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) )
57 47 50 56 3anbi123d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑠 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ↔ ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) )
58 31 57 riotaeqbidv ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( ℩ 𝑠 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑠 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) = ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) )
59 45 46 58 s3eqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑝 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ( cgrA ‘ 𝑔 ) 𝑓 ∧ ( ( 𝑒 ‘ 1 ) ( dist ‘ 𝑔 ) 𝑠 ) = ( ( 𝑓 ‘ 1 ) ( dist ‘ 𝑔 ) ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) ( LineG ‘ 𝑔 ) ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 ( Itv ‘ 𝑔 ) ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ = ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ )
60 28 44 59 ifbieq12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → 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 ) ) ) ≠ ∅ ) ) ”⟩ ) = if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) )
61 23 23 60 mpoeq123dv ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ 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 ) ) ) ≠ ∅ ) ) ”⟩ ) ) = ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) )
62 61 7 eqtr4di ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( 𝑒 ∈ 𝑎 , 𝑓 ∈ 𝑎 ↦ 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 ) ) ) ≠ ∅ ) ) ”⟩ ) ) = + )
63 62 opeq2d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ⟨ ( +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 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ⟩ = ⟨ ( +g ‘ ndx ) , + ⟩ )
64 fveq2 ⊢ ( 𝑔 = 𝐺 → ( ≤∠ ‘ 𝑔 ) = ( ≤∠ ‘ 𝐺 ) )
65 64 9 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( ≤∠ ‘ 𝑔 ) = ≤ )
66 65 opeq2d ⊢ ( 𝑔 = 𝐺 → ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝑔 ) ⟩ = ⟨ ( le ‘ ndx ) , ≤ ⟩ )
67 66 ad2antrr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝑔 ) ⟩ = ⟨ ( le ‘ ndx ) , ≤ ⟩ )
68 22 63 67 tpeq123d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → { ⟨ ( 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 ) , ( ≤∠ ‘ 𝑔 ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } )
69 68 34 oveq12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) ∧ 𝑎 = 𝐴 ) → ( { ⟨ ( 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 ‘ 𝑔 ) ) = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } /s ∼ ) )
70 16 20 69 csbied2 ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑝 = 𝑃 ) → ⦋ { 𝑑 ∈ ( 𝑝 ↑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 ‘ 𝑔 ) ) = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } /s ∼ ) )
71 11 13 70 csbied2 ⊢ ( 𝑔 = 𝐺 → ⦋ ( 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 ‘ 𝑔 ) ) = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } /s ∼ ) )
72 elex ⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V )
73 ovexd ⊢ ( 𝐺 ∈ 𝑉 → ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } /s ∼ ) ∈ V )
74 10 71 72 73 fvmptd3 ⊢ ( 𝐺 ∈ 𝑉 → ( AngMgm ‘ 𝐺 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } /s ∼ ) )
75 8 74 eqtrid ⊢ ( 𝐺 ∈ 𝑉 → 𝐽 = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } /s ∼ ) )