Metamath Proof Explorer

Theorem symgmatr01

Description: Applying a permutation that does not fix a certain element of a set to a second element to an index of a matrix a row with 0's and a 1. (Contributed by AV, 3-Jan-2019)

Ref Expression
Hypotheses symgmatr01.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
symgmatr01.0 ⊢ 0 = ( 0g ‘ 𝑅 )
symgmatr01.1 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion symgmatr01 ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → ∃ 𝑘 ∈ 𝑁 ( 𝑘 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄 ‘ 𝑘 ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 symgmatr01.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 symgmatr01.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 symgmatr01.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 1 symgmatr01lem ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → ∃ 𝑘 ∈ 𝑁 if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) = 0 ) )
5 4 imp ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → ∃ 𝑘 ∈ 𝑁 if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) = 0 )
6 eqidd ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
7 eqeq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 = 𝐾 ↔ 𝑘 = 𝐾 ) )
8 7 adantr ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = ( 𝑄 ‘ 𝑘 ) ) → ( 𝑖 = 𝐾 ↔ 𝑘 = 𝐾 ) )
9 eqeq1 ⊢ ( 𝑗 = ( 𝑄 ‘ 𝑘 ) → ( 𝑗 = 𝐿 ↔ ( 𝑄 ‘ 𝑘 ) = 𝐿 ) )
10 9 adantl ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = ( 𝑄 ‘ 𝑘 ) ) → ( 𝑗 = 𝐿 ↔ ( 𝑄 ‘ 𝑘 ) = 𝐿 ) )
11 10 ifbid ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = ( 𝑄 ‘ 𝑘 ) ) → if ( 𝑗 = 𝐿 , 1 , 0 ) = if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) )
12 oveq12 ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = ( 𝑄 ‘ 𝑘 ) ) → ( 𝑖 𝑀 𝑗 ) = ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) )
13 8 11 12 ifbieq12d ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = ( 𝑄 ‘ 𝑘 ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) = if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) )
14 13 adantl ⊢ ( ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) ∧ 𝑘 ∈ 𝑁 ) ∧ ( 𝑖 = 𝑘 ∧ 𝑗 = ( 𝑄 ‘ 𝑘 ) ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) = if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) )
15 simpr ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
16 eldifi ⊢ ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → 𝑄 ∈ 𝑃 )
17 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
18 17 1 symgfv ⊢ ( ( 𝑄 ∈ 𝑃 ∧ 𝑘 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑘 ) ∈ 𝑁 )
19 18 ex ⊢ ( 𝑄 ∈ 𝑃 → ( 𝑘 ∈ 𝑁 → ( 𝑄 ‘ 𝑘 ) ∈ 𝑁 ) )
20 16 19 syl ⊢ ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → ( 𝑘 ∈ 𝑁 → ( 𝑄 ‘ 𝑘 ) ∈ 𝑁 ) )
21 20 adantl ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → ( 𝑘 ∈ 𝑁 → ( 𝑄 ‘ 𝑘 ) ∈ 𝑁 ) )
22 21 imp ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑘 ) ∈ 𝑁 )
23 3 fvexi ⊢ 1 ∈ V
24 2 fvexi ⊢ 0 ∈ V
25 23 24 ifex ⊢ if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) ∈ V
26 ovex ⊢ ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ∈ V
27 25 26 ifex ⊢ if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) ∈ V
28 27 a1i ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) ∧ 𝑘 ∈ 𝑁 ) → if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) ∈ V )
29 6 14 15 22 28 ovmpod ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄 ‘ 𝑘 ) ) = if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) )
30 29 eqeq1d ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑘 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄 ‘ 𝑘 ) ) = 0 ↔ if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) = 0 ) )
31 30 rexbidva ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → ( ∃ 𝑘 ∈ 𝑁 ( 𝑘 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄 ‘ 𝑘 ) ) = 0 ↔ ∃ 𝑘 ∈ 𝑁 if ( 𝑘 = 𝐾 , if ( ( 𝑄 ‘ 𝑘 ) = 𝐿 , 1 , 0 ) , ( 𝑘 𝑀 ( 𝑄 ‘ 𝑘 ) ) ) = 0 ) )
32 5 31 mpbird ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) ) → ∃ 𝑘 ∈ 𝑁 ( 𝑘 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄 ‘ 𝑘 ) ) = 0 )
33 32 ex ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐿 } ) → ∃ 𝑘 ∈ 𝑁 ( 𝑘 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄 ‘ 𝑘 ) ) = 0 ) )