Proof of Theorem gsummatr01lem4
Step | Hyp | Ref
| Expression |
1 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))) |
2 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑛 → (𝑖 = 𝐾 ↔ 𝑛 = 𝐾)) |
3 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛)) → (𝑖 = 𝐾 ↔ 𝑛 = 𝐾)) |
4 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑄‘𝑛) → (𝑗 = 𝐿 ↔ (𝑄‘𝑛) = 𝐿)) |
5 | 4 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛)) → (𝑗 = 𝐿 ↔ (𝑄‘𝑛) = 𝐿)) |
6 | 5 | ifbid 4058 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛)) → if(𝑗 = 𝐿, 0 , 𝐵) = if((𝑄‘𝑛) = 𝐿, 0 , 𝐵)) |
7 | | oveq12 6558 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛)) → (𝑖𝐴𝑗) = (𝑛𝐴(𝑄‘𝑛))) |
8 | 3, 6, 7 | ifbieq12d 4063 |
. . . . . . . 8
⊢ ((𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛)) → if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)) = if(𝑛 = 𝐾, if((𝑄‘𝑛) = 𝐿, 0 , 𝐵), (𝑛𝐴(𝑄‘𝑛)))) |
9 | | eldifsni 4261 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝑁 ∖ {𝐾}) → 𝑛 ≠ 𝐾) |
10 | 9 | neneqd 2787 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑁 ∖ {𝐾}) → ¬ 𝑛 = 𝐾) |
11 | 10 | iffalsed 4047 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑁 ∖ {𝐾}) → if(𝑛 = 𝐾, if((𝑄‘𝑛) = 𝐿, 0 , 𝐵), (𝑛𝐴(𝑄‘𝑛))) = (𝑛𝐴(𝑄‘𝑛))) |
12 | 11 | adantl 481 |
. . . . . . . 8
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → if(𝑛 = 𝐾, if((𝑄‘𝑛) = 𝐿, 0 , 𝐵), (𝑛𝐴(𝑄‘𝑛))) = (𝑛𝐴(𝑄‘𝑛))) |
13 | 8, 12 | sylan9eqr 2666 |
. . . . . . 7
⊢ (((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) ∧ (𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛))) → if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)) = (𝑛𝐴(𝑄‘𝑛))) |
14 | | eldifi 3694 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑁 ∖ {𝐾}) → 𝑛 ∈ 𝑁) |
15 | 14 | adantl 481 |
. . . . . . 7
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝑛 ∈ 𝑁) |
16 | | gsummatr01.p |
. . . . . . . . 9
⊢ 𝑃 =
(Base‘(SymGrp‘𝑁)) |
17 | | gsummatr01.r |
. . . . . . . . 9
⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} |
18 | 16, 17 | gsummatr01lem1 20280 |
. . . . . . . 8
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ 𝑁) → (𝑄‘𝑛) ∈ 𝑁) |
19 | 14, 18 | sylan2 490 |
. . . . . . 7
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄‘𝑛) ∈ 𝑁) |
20 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑛𝐴(𝑄‘𝑛)) ∈ V |
21 | 20 | a1i 11 |
. . . . . . 7
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛𝐴(𝑄‘𝑛)) ∈ V) |
22 | 1, 13, 15, 19, 21 | ovmpt2d 6686 |
. . . . . 6
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛))) |
23 | 22 | ex 449 |
. . . . 5
⊢ (𝑄 ∈ 𝑅 → (𝑛 ∈ (𝑁 ∖ {𝐾}) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛)))) |
24 | 23 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅) → (𝑛 ∈ (𝑁 ∖ {𝐾}) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛)))) |
25 | 24 | 3ad2ant3 1077 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) → (𝑛 ∈ (𝑁 ∖ {𝐾}) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛)))) |
26 | 25 | imp 444 |
. 2
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛))) |
27 | | eqidd 2611 |
. . 3
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗)) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))) |
28 | 7 | adantl 481 |
. . 3
⊢
(((((𝐺 ∈ CMnd
∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) ∧ (𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛))) → (𝑖𝐴𝑗) = (𝑛𝐴(𝑄‘𝑛))) |
29 | | eqidd 2611 |
. . 3
⊢
(((((𝐺 ∈ CMnd
∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) ∧ 𝑖 = 𝑛) → (𝑁 ∖ {𝐿}) = (𝑁 ∖ {𝐿})) |
30 | | simpr 476 |
. . 3
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝑛 ∈ (𝑁 ∖ {𝐾})) |
31 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑄 → (𝑟‘𝐾) = (𝑄‘𝐾)) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑄 → ((𝑟‘𝐾) = 𝐿 ↔ (𝑄‘𝐾) = 𝐿)) |
33 | 32, 17 | elrab2 3333 |
. . . . . . . . 9
⊢ (𝑄 ∈ 𝑅 ↔ (𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿)) |
34 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) → 𝑄 ∈ 𝑃) |
35 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
36 | 35, 16 | symgfv 17630 |
. . . . . . . . . . . 12
⊢ ((𝑄 ∈ 𝑃 ∧ 𝑛 ∈ 𝑁) → (𝑄‘𝑛) ∈ 𝑁) |
37 | 34, 14, 36 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄‘𝑛) ∈ 𝑁) |
38 | 34 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝑄 ∈ 𝑃) |
39 | | simplrr 797 |
. . . . . . . . . . . . 13
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝐾 ∈ 𝑁) |
40 | 14 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝑛 ∈ 𝑁) |
41 | 38, 39, 40 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄 ∈ 𝑃 ∧ 𝐾 ∈ 𝑁 ∧ 𝑛 ∈ 𝑁)) |
42 | | simpllr 795 |
. . . . . . . . . . . 12
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄‘𝐾) = 𝐿) |
43 | 9 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝑛 ≠ 𝐾) |
44 | 35, 16 | symgfvne 17631 |
. . . . . . . . . . . 12
⊢ ((𝑄 ∈ 𝑃 ∧ 𝐾 ∈ 𝑁 ∧ 𝑛 ∈ 𝑁) → ((𝑄‘𝐾) = 𝐿 → (𝑛 ≠ 𝐾 → (𝑄‘𝑛) ≠ 𝐿))) |
45 | 41, 42, 43, 44 | syl3c 64 |
. . . . . . . . . . 11
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄‘𝑛) ≠ 𝐿) |
46 | 37, 45 | jca 553 |
. . . . . . . . . 10
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿)) |
47 | 46 | exp42 637 |
. . . . . . . . 9
⊢ ((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) → (𝐿 ∈ 𝑁 → (𝐾 ∈ 𝑁 → (𝑛 ∈ (𝑁 ∖ {𝐾}) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿))))) |
48 | 33, 47 | sylbi 206 |
. . . . . . . 8
⊢ (𝑄 ∈ 𝑅 → (𝐿 ∈ 𝑁 → (𝐾 ∈ 𝑁 → (𝑛 ∈ (𝑁 ∖ {𝐾}) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿))))) |
49 | 48 | com13 86 |
. . . . . . 7
⊢ (𝐾 ∈ 𝑁 → (𝐿 ∈ 𝑁 → (𝑄 ∈ 𝑅 → (𝑛 ∈ (𝑁 ∖ {𝐾}) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿))))) |
50 | 49 | 3imp 1249 |
. . . . . 6
⊢ ((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅) → (𝑛 ∈ (𝑁 ∖ {𝐾}) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿))) |
51 | 50 | 3ad2ant3 1077 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) → (𝑛 ∈ (𝑁 ∖ {𝐾}) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿))) |
52 | 51 | imp 444 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿)) |
53 | | eldifsn 4260 |
. . . 4
⊢ ((𝑄‘𝑛) ∈ (𝑁 ∖ {𝐿}) ↔ ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿)) |
54 | 52, 53 | sylibr 223 |
. . 3
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄‘𝑛) ∈ (𝑁 ∖ {𝐿})) |
55 | 20 | a1i 11 |
. . 3
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛𝐴(𝑄‘𝑛)) ∈ V) |
56 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑖(𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) |
57 | | nfra1 2925 |
. . . . . 6
⊢
Ⅎ𝑖∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 |
58 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑖𝑆 |
59 | 58 | nfel2 2767 |
. . . . . 6
⊢
Ⅎ𝑖 𝐵 ∈ 𝑆 |
60 | 57, 59 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑖(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) |
61 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑖(𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅) |
62 | 56, 60, 61 | nf3an 1819 |
. . . 4
⊢
Ⅎ𝑖((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) |
63 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑖(𝑁 ∖ {𝐾}) |
64 | 63 | nfel2 2767 |
. . . 4
⊢
Ⅎ𝑖 𝑛 ∈ (𝑁 ∖ {𝐾}) |
65 | 62, 64 | nfan 1816 |
. . 3
⊢
Ⅎ𝑖(((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) |
66 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑗(𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) |
67 | | nfra2 2930 |
. . . . . 6
⊢
Ⅎ𝑗∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 |
68 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑗𝑆 |
69 | 68 | nfel2 2767 |
. . . . . 6
⊢
Ⅎ𝑗 𝐵 ∈ 𝑆 |
70 | 67, 69 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑗(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) |
71 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑗(𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅) |
72 | 66, 70, 71 | nf3an 1819 |
. . . 4
⊢
Ⅎ𝑗((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) |
73 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑗(𝑁 ∖ {𝐾}) |
74 | 73 | nfel2 2767 |
. . . 4
⊢
Ⅎ𝑗 𝑛 ∈ (𝑁 ∖ {𝐾}) |
75 | 72, 74 | nfan 1816 |
. . 3
⊢
Ⅎ𝑗(((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) |
76 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑗𝑛 |
77 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑖(𝑄‘𝑛) |
78 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑖(𝑛𝐴(𝑄‘𝑛)) |
79 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑗(𝑛𝐴(𝑄‘𝑛)) |
80 | 27, 28, 29, 30, 54, 55, 65, 75, 76, 77, 78, 79 | ovmpt2dxf 6684 |
. 2
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛))) |
81 | 26, 80 | eqtr4d 2647 |
1
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))(𝑄‘𝑛))) |