Metamath Proof Explorer

Theorem symgmatr01lem

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

Ref Expression
Hypothesis symgmatr01.p 
|- P = ( Base ` ( SymGrp ` N ) )
Assertion 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 , A , B ) , ( k M ( Q ` k ) ) ) = B ) )

Proof

Step Hyp Ref Expression
1 symgmatr01.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 simpll 
 |-  ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> K e. N )
3 eqeq1 
 |-  ( k = K -> ( k = K <-> K = K ) )
4 fveq2 
 |-  ( k = K -> ( Q ` k ) = ( Q ` K ) )
5 4 eqeq1d 
 |-  ( k = K -> ( ( Q ` k ) = L <-> ( Q ` K ) = L ) )
6 5 ifbid 
 |-  ( k = K -> if ( ( Q ` k ) = L , A , B ) = if ( ( Q ` K ) = L , A , B ) )
7 id 
 |-  ( k = K -> k = K )
8 7 4 oveq12d 
 |-  ( k = K -> ( k M ( Q ` k ) ) = ( K M ( Q ` K ) ) )
9 3 6 8 ifbieq12d 
 |-  ( k = K -> if ( k = K , if ( ( Q ` k ) = L , A , B ) , ( k M ( Q ` k ) ) ) = if ( K = K , if ( ( Q ` K ) = L , A , B ) , ( K M ( Q ` K ) ) ) )
10 9 eqeq1d 
 |-  ( k = K -> ( if ( k = K , if ( ( Q ` k ) = L , A , B ) , ( k M ( Q ` k ) ) ) = B <-> if ( K = K , if ( ( Q ` K ) = L , A , B ) , ( K M ( Q ` K ) ) ) = B ) )
11 10 adantl 
 |-  ( ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) /\ k = K ) -> ( if ( k = K , if ( ( Q ` k ) = L , A , B ) , ( k M ( Q ` k ) ) ) = B <-> if ( K = K , if ( ( Q ` K ) = L , A , B ) , ( K M ( Q ` K ) ) ) = B ) )
12 eqidd 
 |-  ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> K = K )
13 12 iftrued 
 |-  ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> if ( K = K , if ( ( Q ` K ) = L , A , B ) , ( K M ( Q ` K ) ) ) = if ( ( Q ` K ) = L , A , B ) )
14 eldif 
 |-  ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) <-> ( Q e. P /\ -. Q e. { q e. P | ( q ` K ) = L } ) )
15 ianor 
 |-  ( -. ( Q e. P /\ ( Q ` K ) = L ) <-> ( -. Q e. P \/ -. ( Q ` K ) = L ) )
16 fveq1 
 |-  ( q = Q -> ( q ` K ) = ( Q ` K ) )
17 16 eqeq1d 
 |-  ( q = Q -> ( ( q ` K ) = L <-> ( Q ` K ) = L ) )
18 17 elrab 
 |-  ( Q e. { q e. P | ( q ` K ) = L } <-> ( Q e. P /\ ( Q ` K ) = L ) )
19 15 18 xchnxbir 
 |-  ( -. Q e. { q e. P | ( q ` K ) = L } <-> ( -. Q e. P \/ -. ( Q ` K ) = L ) )
20 pm2.21 
 |-  ( -. Q e. P -> ( Q e. P -> -. ( Q ` K ) = L ) )
21 ax-1 
 |-  ( -. ( Q ` K ) = L -> ( Q e. P -> -. ( Q ` K ) = L ) )
22 20 21 jaoi 
 |-  ( ( -. Q e. P \/ -. ( Q ` K ) = L ) -> ( Q e. P -> -. ( Q ` K ) = L ) )
23 19 22 sylbi 
 |-  ( -. Q e. { q e. P | ( q ` K ) = L } -> ( Q e. P -> -. ( Q ` K ) = L ) )
24 23 impcom 
 |-  ( ( Q e. P /\ -. Q e. { q e. P | ( q ` K ) = L } ) -> -. ( Q ` K ) = L )
25 14 24 sylbi 
 |-  ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> -. ( Q ` K ) = L )
26 25 adantl 
 |-  ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> -. ( Q ` K ) = L )
27 26 iffalsed 
 |-  ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> if ( ( Q ` K ) = L , A , B ) = B )
28 13 27 eqtrd 
 |-  ( ( ( K e. N /\ L e. N ) /\ Q e. ( P \ { q e. P | ( q ` K ) = L } ) ) -> if ( K = K , if ( ( Q ` K ) = L , A , B ) , ( K M ( Q ` K ) ) ) = B )
29 2 11 28 rspcedvd 
 |-  ( ( ( 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 , A , B ) , ( k M ( Q ` k ) ) ) = B )
30 29 ex 
 |-  ( ( 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 , A , B ) , ( k M ( Q ` k ) ) ) = B ) )