Metamath Proof Explorer


Theorem mgm2nsgrplem2

Description: Lemma 2 for mgm2nsgrp . (Contributed by AV, 27-Jan-2020)

Ref Expression
Hypotheses mgm2nsgrp.s 𝑆 = { 𝐴 , 𝐵 }
mgm2nsgrp.b ( Base ‘ 𝑀 ) = 𝑆
mgm2nsgrp.o ( +g𝑀 ) = ( 𝑥𝑆 , 𝑦𝑆 ↦ if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) )
mgm2nsgrp.p = ( +g𝑀 )
Assertion mgm2nsgrplem2 ( ( 𝐴𝑉𝐵𝑊 ) → ( ( 𝐴 𝐴 ) 𝐵 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s 𝑆 = { 𝐴 , 𝐵 }
2 mgm2nsgrp.b ( Base ‘ 𝑀 ) = 𝑆
3 mgm2nsgrp.o ( +g𝑀 ) = ( 𝑥𝑆 , 𝑦𝑆 ↦ if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) )
4 mgm2nsgrp.p = ( +g𝑀 )
5 prid1g ( 𝐴𝑉𝐴 ∈ { 𝐴 , 𝐵 } )
6 5 1 eleqtrrdi ( 𝐴𝑉𝐴𝑆 )
7 prid2g ( 𝐵𝑊𝐵 ∈ { 𝐴 , 𝐵 } )
8 7 1 eleqtrrdi ( 𝐵𝑊𝐵𝑆 )
9 4 3 eqtri = ( 𝑥𝑆 , 𝑦𝑆 ↦ if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) )
10 9 a1i ( ( 𝐴𝑆𝐵𝑆 ) → = ( 𝑥𝑆 , 𝑦𝑆 ↦ if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) ) )
11 ifeq1 ( 𝐵 = 𝐴 → if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐴 , 𝐴 ) )
12 ifid if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐴 , 𝐴 ) = 𝐴
13 11 12 eqtrdi ( 𝐵 = 𝐴 → if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 )
14 13 a1d ( 𝐵 = 𝐴 → ( 𝑦 = 𝐵 → if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 ) )
15 eqeq1 ( 𝑦 = 𝐵 → ( 𝑦 = 𝐴𝐵 = 𝐴 ) )
16 15 bicomd ( 𝑦 = 𝐵 → ( 𝐵 = 𝐴𝑦 = 𝐴 ) )
17 16 notbid ( 𝑦 = 𝐵 → ( ¬ 𝐵 = 𝐴 ↔ ¬ 𝑦 = 𝐴 ) )
18 17 biimpac ( ( ¬ 𝐵 = 𝐴𝑦 = 𝐵 ) → ¬ 𝑦 = 𝐴 )
19 18 intnand ( ( ¬ 𝐵 = 𝐴𝑦 = 𝐵 ) → ¬ ( 𝑥 = 𝐴𝑦 = 𝐴 ) )
20 19 iffalsed ( ( ¬ 𝐵 = 𝐴𝑦 = 𝐵 ) → if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 )
21 20 ex ( ¬ 𝐵 = 𝐴 → ( 𝑦 = 𝐵 → if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 ) )
22 14 21 pm2.61i ( 𝑦 = 𝐵 → if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 )
23 22 ad2antll ( ( ( 𝐴𝑆𝐵𝑆 ) ∧ ( 𝑥 = ( 𝐴 𝐴 ) ∧ 𝑦 = 𝐵 ) ) → if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 )
24 iftrue ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) → if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐵 )
25 24 adantl ( ( ( 𝐴𝑆𝐵𝑆 ) ∧ ( 𝑥 = 𝐴𝑦 = 𝐴 ) ) → if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐵 )
26 simpl ( ( 𝐴𝑆𝐵𝑆 ) → 𝐴𝑆 )
27 simpr ( ( 𝐴𝑆𝐵𝑆 ) → 𝐵𝑆 )
28 10 25 26 26 27 ovmpod ( ( 𝐴𝑆𝐵𝑆 ) → ( 𝐴 𝐴 ) = 𝐵 )
29 28 27 eqeltrd ( ( 𝐴𝑆𝐵𝑆 ) → ( 𝐴 𝐴 ) ∈ 𝑆 )
30 10 23 29 27 26 ovmpod ( ( 𝐴𝑆𝐵𝑆 ) → ( ( 𝐴 𝐴 ) 𝐵 ) = 𝐴 )
31 6 8 30 syl2an ( ( 𝐴𝑉𝐵𝑊 ) → ( ( 𝐴 𝐴 ) 𝐵 ) = 𝐴 )