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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ⚬ 𝐴 ) ⚬ 𝐵 ) = 𝐴 )