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