Theorem symgmatr01lem

Description: Lemma for symgmatr01 . (Contributed by AV, 3-Jan-2019)

	Ref	Expression
Hypothesis	symgmatr01.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
Assertion	symgmatr01lem	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → ∃ 𝑘 ∈ 𝑁 if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		symgmatr01.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		simpll	⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → 𝐾 ∈ 𝑁 )
3		eqeq1	⊢ ( 𝑘 = 𝐾 → ( 𝑘 = 𝐾 ↔ 𝐾 = 𝐾 ) )
4		fveq2	⊢ ( 𝑘 = 𝐾 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 𝐾 ) )
5	4	eqeq1d	⊢ ( 𝑘 = 𝐾 → ( ( 𝑄 ‘ 𝑘 ) = 𝐿 ↔ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
6	5	ifbid	⊢ ( 𝑘 = 𝐾 → if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 𝐴 , 𝐵 ) = if ( ( 𝑄 ‘ 𝐾 ) = 𝐿 , 𝐴 , 𝐵 ) )
7		id	⊢ ( 𝑘 = 𝐾 → 𝑘 = 𝐾 )
8	7 4	oveq12d	⊢ ( 𝑘 = 𝐾 → ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) = ( 𝐾 𝑀 ( 𝑄 ‘ 𝐾 ) ) )
9	3 6 8	ifbieq12d	⊢ ( 𝑘 = 𝐾 → if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) = if ( 𝐾 = 𝐾 , if ( ( 𝑄 ‘ 𝐾 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝐾 𝑀 ( 𝑄 ‘ 𝐾 ) ) ) )
10	9	eqeq1d	⊢ ( 𝑘 = 𝐾 → ( if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) = 𝐵 ↔ if ( 𝐾 = 𝐾 , if ( ( 𝑄 ‘ 𝐾 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝐾 𝑀 ( 𝑄 ‘ 𝐾 ) ) ) = 𝐵 ) )
11	10	adantl	⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) ∧ 𝑘 = 𝐾 ) → ( if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) = 𝐵 ↔ if ( 𝐾 = 𝐾 , if ( ( 𝑄 ‘ 𝐾 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝐾 𝑀 ( 𝑄 ‘ 𝐾 ) ) ) = 𝐵 ) )
12		eqidd	⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → 𝐾 = 𝐾 )
13	12	iftrued	⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → if ( 𝐾 = 𝐾 , if ( ( 𝑄 ‘ 𝐾 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝐾 𝑀 ( 𝑄 ‘ 𝐾 ) ) ) = if ( ( 𝑄 ‘ 𝐾 ) = 𝐿 , 𝐴 , 𝐵 ) )
14		eldif	⊢ ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ↔ ( 𝑄 ∈ 𝑃 ∧ ¬ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) )
15		ianor	⊢ ( ¬ ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ↔ ( ¬ 𝑄 ∈ 𝑃 ∨ ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
16		fveq1	⊢ ( 𝑞 = 𝑄 → ( 𝑞 ‘ 𝐾 ) = ( 𝑄 ‘ 𝐾 ) )
17	16	eqeq1d	⊢ ( 𝑞 = 𝑄 → ( ( 𝑞 ‘ 𝐾 ) = 𝐿 ↔ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
18	17	elrab	⊢ ( 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ↔ ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
19	15 18	xchnxbir	⊢ ( ¬ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ↔ ( ¬ 𝑄 ∈ 𝑃 ∨ ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
20		pm2.21	⊢ ( ¬ 𝑄 ∈ 𝑃 → ( 𝑄 ∈ 𝑃 → ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
21		ax-1	⊢ ( ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 → ( 𝑄 ∈ 𝑃 → ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
22	20 21	jaoi	⊢ ( ( ¬ 𝑄 ∈ 𝑃 ∨ ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) → ( 𝑄 ∈ 𝑃 → ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
23	19 22	sylbi	⊢ ( ¬ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } → ( 𝑄 ∈ 𝑃 → ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
24	23	impcom	⊢ ( ( 𝑄 ∈ 𝑃 ∧ ¬ 𝑄 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 )
25	14 24	sylbi	⊢ ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 )
26	25	adantl	⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → ¬ ( 𝑄 ‘ 𝐾 ) = 𝐿 )
27	26	iffalsed	⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → if ( ( 𝑄 ‘ 𝐾 ) = 𝐿 , 𝐴 , 𝐵 ) = 𝐵 )
28	13 27	eqtrd	⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → if ( 𝐾 = 𝐾 , if ( ( 𝑄 ‘ 𝐾 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝐾 𝑀 ( 𝑄 ‘ 𝐾 ) ) ) = 𝐵 )
29	2 11 28	rspcedvd	⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → ∃ 𝑘 ∈ 𝑁 if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) = 𝐵 )
30	29	ex	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → ∃ 𝑘 ∈ 𝑁 if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 𝐴 , 𝐵 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) = 𝐵 ) )