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 
|- P = ( Base ` ( SymGrp ` N ) )
symgmatr01.0 
|- .0. = ( 0g ` R )
symgmatr01.1 
|- .1. = ( 1r ` R )
Assertion symgmatr01 
|- ( ( K e. N /\ L e. N ) -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> E. k e. N ( k ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` k ) ) = .0. ) )

Proof

Step Hyp Ref Expression
1 symgmatr01.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 symgmatr01.0 
 |-  .0. = ( 0g ` R )
3 symgmatr01.1 
 |-  .1. = ( 1r ` R )
4 1 symgmatr01lem 
 |-  ( ( K e. N /\ L e. N ) -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> E. k e. N if ( k = K , if ( ( Q ` k ) = L , .1. , .0. ) , ( k M ( Q ` k ) ) ) = .0. ) )
5 4 imp 
 |-  ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> E. k e. N if ( k = K , if ( ( Q ` k ) = L , .1. , .0. ) , ( k M ( Q ` k ) ) ) = .0. )
6 eqidd 
 |-  ( ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) /\ k e. N ) -> ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) )
7 eqeq1 
 |-  ( i = k -> ( i = K <-> k = K ) )
8 7 adantr 
 |-  ( ( i = k /\ j = ( Q ` k ) ) -> ( i = K <-> k = K ) )
9 eqeq1 
 |-  ( j = ( Q ` k ) -> ( j = L <-> ( Q ` k ) = L ) )
10 9 adantl 
 |-  ( ( i = k /\ j = ( Q ` k ) ) -> ( j = L <-> ( Q ` k ) = L ) )
11 10 ifbid 
 |-  ( ( i = k /\ j = ( Q ` k ) ) -> if ( j = L , .1. , .0. ) = if ( ( Q ` k ) = L , .1. , .0. ) )
12 oveq12 
 |-  ( ( i = k /\ j = ( Q ` k ) ) -> ( i M j ) = ( k M ( Q ` k ) ) )
13 8 11 12 ifbieq12d 
 |-  ( ( i = k /\ j = ( Q ` k ) ) -> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) = if ( k = K , if ( ( Q ` k ) = L , .1. , .0. ) , ( k M ( Q ` k ) ) ) )
14 13 adantl 
 |-  ( ( ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) /\ k e. N ) /\ ( i = k /\ j = ( Q ` k ) ) ) -> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) = if ( k = K , if ( ( Q ` k ) = L , .1. , .0. ) , ( k M ( Q ` k ) ) ) )
15 simpr 
 |-  ( ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) /\ k e. N ) -> k e. N )
16 eldifi 
 |-  ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> Q e. P )
17 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
18 17 1 symgfv 
 |-  ( ( Q e. P /\ k e. N ) -> ( Q ` k ) e. N )
19 18 ex 
 |-  ( Q e. P -> ( k e. N -> ( Q ` k ) e. N ) )
20 16 19 syl 
 |-  ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> ( k e. N -> ( Q ` k ) e. N ) )
21 20 adantl 
 |-  ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> ( k e. N -> ( Q ` k ) e. N ) )
22 21 imp 
 |-  ( ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) /\ k e. N ) -> ( Q ` k ) e. N )
23 3 fvexi 
 |-  .1. e. _V
24 2 fvexi 
 |-  .0. e. _V
25 23 24 ifex 
 |-  if ( ( Q ` k ) = L , .1. , .0. ) e. _V
26 ovex 
 |-  ( k M ( Q ` k ) ) e. _V
27 25 26 ifex 
 |-  if ( k = K , if ( ( Q ` k ) = L , .1. , .0. ) , ( k M ( Q ` k ) ) ) e. _V
28 27 a1i 
 |-  ( ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) /\ k e. N ) -> if ( k = K , if ( ( Q ` k ) = L , .1. , .0. ) , ( k M ( Q ` k ) ) ) e. _V )
29 6 14 15 22 28 ovmpod 
 |-  ( ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) /\ k e. N ) -> ( k ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` k ) ) = if ( k = K , if ( ( Q ` k ) = L , .1. , .0. ) , ( k M ( Q ` k ) ) ) )
30 29 eqeq1d 
 |-  ( ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) /\ k e. N ) -> ( ( k ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` k ) ) = .0. <-> if ( k = K , if ( ( Q ` k ) = L , .1. , .0. ) , ( k M ( Q ` k ) ) ) = .0. ) )
31 30 rexbidva 
 |-  ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> ( E. k e. N ( k ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` k ) ) = .0. <-> E. k e. N if ( k = K , if ( ( Q ` k ) = L , .1. , .0. ) , ( k M ( Q ` k ) ) ) = .0. ) )
32 5 31 mpbird 
 |-  ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> E. k e. N ( k ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` k ) ) = .0. )
33 32 ex 
 |-  ( ( K e. N /\ L e. N ) -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> E. k e. N ( k ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` k ) ) = .0. ) )