Metamath Proof Explorer

Theorem angmgmlem

Description: Lemma for angmgm . (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 ‘ 𝐺 )
angmgmlem.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
angmgmlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
angmgmlem.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
Assertion angmgmlem ( 𝜑 → ( 𝐽 ∈ Mgm ∧ [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ∼ = ( 0g ‘ 𝐽 ) ) )

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 angmgmlem.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
10 angmgmlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11 angmgmlem.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
12 eqid ⊢ ( ≤∠ ‘ 𝐺 ) = ( ≤∠ ‘ 𝐺 )
13 1 2 3 4 5 6 7 8 12 angmgmval ⊢ ( 𝐺 ∈ TarskiG → 𝐽 = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } /s ∼ ) )
14 9 13 syl ⊢ ( 𝜑 → 𝐽 = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } /s ∼ ) )
15 ovex ⊢ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∈ V
16 2 15 rabex2 ⊢ 𝐴 ∈ V
17 1nn ⊢ 1 ∈ ℕ
18 basendx ⊢ ( Base ‘ ndx ) = 1
19 1lt2 ⊢ 1 < 2
20 2nn ⊢ 2 ∈ ℕ
21 plusgndx ⊢ ( +g ‘ ndx ) = 2
22 2lt10 ⊢ 2 < 1 0
23 10nn ⊢ 1 0 ∈ ℕ
24 plendx ⊢ ( le ‘ ndx ) = 1 0
25 17 18 19 20 21 22 23 24 strle3 ⊢ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } Struct ⟨ 1 , 1 0 ⟩
26 baseid ⊢ Base = Slot ( Base ‘ ndx )
27 snsstp1 ⊢ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ }
28 25 26 27 strfv ⊢ ( 𝐴 ∈ V → 𝐴 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } ) )
29 16 28 mp1i ⊢ ( 𝜑 → 𝐴 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } ) )
30 5 fvexi ⊢ ∼ ∈ V
31 30 a1i ⊢ ( 𝜑 → ∼ ∈ V )
32 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } ∈ V
33 32 a1i ⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } ∈ V )
34 1 2 5 9 cgrabasimass ⊢ ( 𝜑 → ( ∼ “ 𝐴 ) ⊆ 𝐴 )
35 14 29 31 33 34 qusin ⊢ ( 𝜑 → 𝐽 = ( { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } /s ( ∼ ∩ ( 𝐴 × 𝐴 ) ) ) )
36 16 16 mpoex ⊢ ( 𝑒 ∈ 𝐴 , 𝑓 ∈ 𝐴 ↦ if ( ( 𝑒 ‘ 0 ) ∈ ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) , ⟨“ ( 𝑓 ‘ 0 ) ( 𝑓 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑓 ‘ 2 ) ( 𝑓 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑒 ∧ ( ( 𝑓 ‘ 1 ) − 𝑠 ) = ( ( 𝑒 ‘ 1 ) − ( 𝑒 ‘ 0 ) ) ) ) ”⟩ , ⟨“ ( 𝑒 ‘ 0 ) ( 𝑒 ‘ 1 ) ( ℩ 𝑠 ∈ 𝑃 ( ⟨“ ( 𝑒 ‘ 2 ) ( 𝑒 ‘ 1 ) 𝑠 ”⟩ ∼ 𝑓 ∧ ( ( 𝑒 ‘ 1 ) − 𝑠 ) = ( ( 𝑓 ‘ 1 ) − ( 𝑓 ‘ 0 ) ) ∧ ( ( ( 𝑒 ‘ 1 ) 𝐿 ( 𝑒 ‘ 2 ) ) ∩ ( 𝑠 𝐼 ( 𝑒 ‘ 0 ) ) ) ≠ ∅ ) ) ”⟩ ) ) ∈ V
37 7 36 eqeltri ⊢ + ∈ V
38 plusgid ⊢ +g = Slot ( +g ‘ ndx )
39 snsstp2 ⊢ { ⟨ ( +g ‘ ndx ) , + ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ }
40 25 38 39 strfv ⊢ ( + ∈ V → + = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } ) )
41 37 40 ax-mp ⊢ + = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( le ‘ ndx ) , ( ≤∠ ‘ 𝐺 ) ⟩ } )
42 1 2 5 9 cgraer ⊢ ( 𝜑 → ( ∼ ∩ ( 𝐴 × 𝐴 ) ) Er 𝐴 )
43 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → 𝐺 ∈ TarskiG )
44 brinxp2 ⊢ ( 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑎 ∼ 𝑝 ) )
45 44 biimpi ⊢ ( 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑎 ∼ 𝑝 ) )
46 45 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑎 ∼ 𝑝 ) )
47 46 simplld ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → 𝑎 ∈ 𝐴 )
48 brinxp2 ⊢ ( 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ↔ ( ( 𝑏 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑏 ∼ 𝑞 ) )
49 48 bilani ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → ( ( 𝑏 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑏 ∼ 𝑞 ) )
50 49 simplld ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → 𝑏 ∈ 𝐴 )
51 1 2 3 4 5 6 43 7 47 50 angmgmaddcl ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → ( 𝑎 + 𝑏 ) ∈ 𝐴 )
52 46 simplrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → 𝑝 ∈ 𝐴 )
53 49 simplrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → 𝑞 ∈ 𝐴 )
54 1 2 3 4 5 6 43 7 52 53 angmgmaddcl ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → ( 𝑝 + 𝑞 ) ∈ 𝐴 )
55 46 simprd ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → 𝑎 ∼ 𝑝 )
56 49 simprd ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → 𝑏 ∼ 𝑞 )
57 1 2 3 4 5 6 43 7 52 53 47 50 55 56 angmgmaddcpbl ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → ( 𝑎 + 𝑏 ) ∼ ( 𝑝 + 𝑞 ) )
58 brinxp2 ⊢ ( ( 𝑎 + 𝑏 ) ( ∼ ∩ ( 𝐴 × 𝐴 ) ) ( 𝑝 + 𝑞 ) ↔ ( ( ( 𝑎 + 𝑏 ) ∈ 𝐴 ∧ ( 𝑝 + 𝑞 ) ∈ 𝐴 ) ∧ ( 𝑎 + 𝑏 ) ∼ ( 𝑝 + 𝑞 ) ) )
59 51 54 57 58 syl21anbrc ⊢ ( ( ( 𝜑 ∧ 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ) ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → ( 𝑎 + 𝑏 ) ( ∼ ∩ ( 𝐴 × 𝐴 ) ) ( 𝑝 + 𝑞 ) )
60 59 expl ⊢ ( 𝜑 → ( ( 𝑎 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑝 ∧ 𝑏 ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑞 ) → ( 𝑎 + 𝑏 ) ( ∼ ∩ ( 𝐴 × 𝐴 ) ) ( 𝑝 + 𝑞 ) ) )
61 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → 𝐺 ∈ TarskiG )
62 simp2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → 𝑖 ∈ 𝐴 )
63 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝐴 )
64 1 2 3 4 5 6 61 7 62 63 angmgmaddcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑖 + 𝑗 ) ∈ 𝐴 )
65 1 fvexi ⊢ 𝑃 ∈ V
66 65 a1i ⊢ ( 𝜑 → 𝑃 ∈ V )
67 11 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
68 11 eldifsnbd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
69 68 necomd ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
70 2 66 10 67 10 69 68 elcgrabasrd ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑋 ”⟩ ∈ 𝐴 )
71 9 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝐺 ∈ TarskiG )
72 70 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⟨“ 𝑋 𝑌 𝑋 ”⟩ ∈ 𝐴 )
73 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝑖 ∈ 𝐴 )
74 1 2 3 4 5 6 71 7 72 73 angmgmaddcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝑖 ) ∈ 𝐴 )
75 10 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝑋 ∈ 𝑃 )
76 11 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
77 1 2 3 4 5 6 71 7 75 76 73 angmgmaddlid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝑖 ) ∼ 𝑖 )
78 brinxp2 ⊢ ( ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝑖 ) ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑖 ↔ ( ( ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝑖 ) ∈ 𝐴 ∧ 𝑖 ∈ 𝐴 ) ∧ ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝑖 ) ∼ 𝑖 ) )
79 74 73 77 78 syl21anbrc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ + 𝑖 ) ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑖 )
80 1 2 3 4 5 6 71 7 73 72 angmgmaddcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑖 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∈ 𝐴 )
81 1 2 3 4 5 6 71 7 75 76 73 angmgmaddrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑖 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ 𝑖 )
82 brinxp2 ⊢ ( ( 𝑖 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑖 ↔ ( ( ( 𝑖 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∈ 𝐴 ∧ 𝑖 ∈ 𝐴 ) ∧ ( 𝑖 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ∼ 𝑖 ) )
83 80 73 81 82 syl21anbrc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑖 + ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ( ∼ ∩ ( 𝐴 × 𝐴 ) ) 𝑖 )
84 35 29 41 42 33 60 64 70 79 83 qusmgm ⊢ ( 𝜑 → ( 𝐽 ∈ Mgm ∧ [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ( ∼ ∩ ( 𝐴 × 𝐴 ) ) = ( 0g ‘ 𝐽 ) ) )
85 ecinxp ⊢ ( ( ( ∼ “ 𝐴 ) ⊆ 𝐴 ∧ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ∈ 𝐴 ) → [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ∼ = [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ( ∼ ∩ ( 𝐴 × 𝐴 ) ) )
86 34 70 85 syl2anc ⊢ ( 𝜑 → [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ∼ = [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ( ∼ ∩ ( 𝐴 × 𝐴 ) ) )
87 86 eqeq1d ⊢ ( 𝜑 → ( [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ∼ = ( 0g ‘ 𝐽 ) ↔ [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ( ∼ ∩ ( 𝐴 × 𝐴 ) ) = ( 0g ‘ 𝐽 ) ) )
88 87 anbi2d ⊢ ( 𝜑 → ( ( 𝐽 ∈ Mgm ∧ [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ∼ = ( 0g ‘ 𝐽 ) ) ↔ ( 𝐽 ∈ Mgm ∧ [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ( ∼ ∩ ( 𝐴 × 𝐴 ) ) = ( 0g ‘ 𝐽 ) ) ) )
89 84 88 mpbird ⊢ ( 𝜑 → ( 𝐽 ∈ Mgm ∧ [ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ] ∼ = ( 0g ‘ 𝐽 ) ) )