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 ) )