Theorem mgm2nsgrplem3

Description: Lemma 3 for mgm2nsgrp . (Contributed by AV, 28-Jan-2020)

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

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		simprl	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = ( 𝐴 ⚬ 𝐵 ) ) ) → 𝑥 = 𝐴 )
12		simpr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = ( 𝐴 ⚬ 𝐵 ) ) → 𝑦 = ( 𝐴 ⚬ 𝐵 ) )
13		ifeq1	⊢ ( 𝐵 = 𝐴 → if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐴 , 𝐴 ) )
14		ifid	⊢ if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐴 , 𝐴 ) = 𝐴
15	13 14	eqtrdi	⊢ ( 𝐵 = 𝐴 → if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 )
16	15	a1d	⊢ ( 𝐵 = 𝐴 → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 ) )
17		eqeq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 = 𝐴 ↔ 𝐵 = 𝐴 ) )
18	17	biimpcd	⊢ ( 𝑦 = 𝐴 → ( 𝑦 = 𝐵 → 𝐵 = 𝐴 ) )
19	18	adantl	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) → ( 𝑦 = 𝐵 → 𝐵 = 𝐴 ) )
20	19	com12	⊢ ( 𝑦 = 𝐵 → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) → 𝐵 = 𝐴 ) )
21	20	adantl	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) → 𝐵 = 𝐴 ) )
22	21	con3d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ¬ 𝐵 = 𝐴 → ¬ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) ) )
23	22	impcom	⊢ ( ( ¬ 𝐵 = 𝐴 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ¬ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
24	23	iffalsed	⊢ ( ( ¬ 𝐵 = 𝐴 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 )
25	24	ex	⊢ ( ¬ 𝐵 = 𝐴 → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 ) )
26	16 25	pm2.61i	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 )
27	26	adantl	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐴 )
28		simpl	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
29		simpr	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐵 ∈ 𝑆 )
30	10 27 28 29 28	ovmpod	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ⚬ 𝐵 ) = 𝐴 )
31	12 30	sylan9eqr	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = ( 𝐴 ⚬ 𝐵 ) ) ) → 𝑦 = 𝐴 )
32	11 31	jca	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = ( 𝐴 ⚬ 𝐵 ) ) ) → ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
33	32	iftrued	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = ( 𝐴 ⚬ 𝐵 ) ) ) → if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) = 𝐵 )
34	30 28	eqeltrd	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ⚬ 𝐵 ) ∈ 𝑆 )
35	10 33 28 34 29	ovmpod	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ⚬ ( 𝐴 ⚬ 𝐵 ) ) = 𝐵 )
36	6 8 35	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⚬ ( 𝐴 ⚬ 𝐵 ) ) = 𝐵 )