Proof of Theorem gsummatr01lem4
Step | Hyp | Ref
| Expression |
1 | | eqidd 2740 |
. . . . . . 7
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))) |
2 | | eqeq1 2743 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑛 → (𝑖 = 𝐾 ↔ 𝑛 = 𝐾)) |
3 | 2 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛)) → (𝑖 = 𝐾 ↔ 𝑛 = 𝐾)) |
4 | | eqeq1 2743 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑄‘𝑛) → (𝑗 = 𝐿 ↔ (𝑄‘𝑛) = 𝐿)) |
5 | 4 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛)) → (𝑗 = 𝐿 ↔ (𝑄‘𝑛) = 𝐿)) |
6 | 5 | ifbid 4479 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛)) → if(𝑗 = 𝐿, 0 , 𝐵) = if((𝑄‘𝑛) = 𝐿, 0 , 𝐵)) |
7 | | oveq12 7244 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛)) → (𝑖𝐴𝑗) = (𝑛𝐴(𝑄‘𝑛))) |
8 | 3, 6, 7 | ifbieq12d 4484 |
. . . . . . . 8
⊢ ((𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛)) → if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)) = if(𝑛 = 𝐾, if((𝑄‘𝑛) = 𝐿, 0 , 𝐵), (𝑛𝐴(𝑄‘𝑛)))) |
9 | | eldifsni 4720 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝑁 ∖ {𝐾}) → 𝑛 ≠ 𝐾) |
10 | 9 | neneqd 2948 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑁 ∖ {𝐾}) → ¬ 𝑛 = 𝐾) |
11 | 10 | iffalsed 4467 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑁 ∖ {𝐾}) → if(𝑛 = 𝐾, if((𝑄‘𝑛) = 𝐿, 0 , 𝐵), (𝑛𝐴(𝑄‘𝑛))) = (𝑛𝐴(𝑄‘𝑛))) |
12 | 11 | adantl 485 |
. . . . . . . 8
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → if(𝑛 = 𝐾, if((𝑄‘𝑛) = 𝐿, 0 , 𝐵), (𝑛𝐴(𝑄‘𝑛))) = (𝑛𝐴(𝑄‘𝑛))) |
13 | 8, 12 | sylan9eqr 2802 |
. . . . . . 7
⊢ (((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) ∧ (𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛))) → if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)) = (𝑛𝐴(𝑄‘𝑛))) |
14 | | eldifi 4058 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑁 ∖ {𝐾}) → 𝑛 ∈ 𝑁) |
15 | 14 | adantl 485 |
. . . . . . 7
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝑛 ∈ 𝑁) |
16 | | gsummatr01.p |
. . . . . . . . 9
⊢ 𝑃 =
(Base‘(SymGrp‘𝑁)) |
17 | | gsummatr01.r |
. . . . . . . . 9
⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} |
18 | 16, 17 | gsummatr01lem1 21584 |
. . . . . . . 8
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ 𝑁) → (𝑄‘𝑛) ∈ 𝑁) |
19 | 14, 18 | sylan2 596 |
. . . . . . 7
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄‘𝑛) ∈ 𝑁) |
20 | | ovexd 7270 |
. . . . . . 7
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛𝐴(𝑄‘𝑛)) ∈ V) |
21 | 1, 13, 15, 19, 20 | ovmpod 7383 |
. . . . . 6
⊢ ((𝑄 ∈ 𝑅 ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛))) |
22 | 21 | ex 416 |
. . . . 5
⊢ (𝑄 ∈ 𝑅 → (𝑛 ∈ (𝑁 ∖ {𝐾}) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛)))) |
23 | 22 | 3ad2ant3 1137 |
. . . 4
⊢ ((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅) → (𝑛 ∈ (𝑁 ∖ {𝐾}) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛)))) |
24 | 23 | 3ad2ant3 1137 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) → (𝑛 ∈ (𝑁 ∖ {𝐾}) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛)))) |
25 | 24 | imp 410 |
. 2
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛))) |
26 | | eqidd 2740 |
. . 3
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗)) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))) |
27 | 7 | adantl 485 |
. . 3
⊢
(((((𝐺 ∈ CMnd
∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) ∧ (𝑖 = 𝑛 ∧ 𝑗 = (𝑄‘𝑛))) → (𝑖𝐴𝑗) = (𝑛𝐴(𝑄‘𝑛))) |
28 | | eqidd 2740 |
. . 3
⊢
(((((𝐺 ∈ CMnd
∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) ∧ 𝑖 = 𝑛) → (𝑁 ∖ {𝐿}) = (𝑁 ∖ {𝐿})) |
29 | | simpr 488 |
. . 3
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝑛 ∈ (𝑁 ∖ {𝐾})) |
30 | | fveq1 6738 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑄 → (𝑟‘𝐾) = (𝑄‘𝐾)) |
31 | 30 | eqeq1d 2741 |
. . . . . . . . 9
⊢ (𝑟 = 𝑄 → ((𝑟‘𝐾) = 𝐿 ↔ (𝑄‘𝐾) = 𝐿)) |
32 | 31, 17 | elrab2 3620 |
. . . . . . . 8
⊢ (𝑄 ∈ 𝑅 ↔ (𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿)) |
33 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) → 𝑄 ∈ 𝑃) |
34 | | eqid 2739 |
. . . . . . . . . . . 12
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
35 | 34, 16 | symgfv 18805 |
. . . . . . . . . . 11
⊢ ((𝑄 ∈ 𝑃 ∧ 𝑛 ∈ 𝑁) → (𝑄‘𝑛) ∈ 𝑁) |
36 | 33, 14, 35 | syl2an 599 |
. . . . . . . . . 10
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄‘𝑛) ∈ 𝑁) |
37 | 33 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝑄 ∈ 𝑃) |
38 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝐾 ∈ 𝑁) |
39 | 14 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝑛 ∈ 𝑁) |
40 | 37, 38, 39 | 3jca 1130 |
. . . . . . . . . . 11
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄 ∈ 𝑃 ∧ 𝐾 ∈ 𝑁 ∧ 𝑛 ∈ 𝑁)) |
41 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄‘𝐾) = 𝐿) |
42 | 9 | adantl 485 |
. . . . . . . . . . 11
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → 𝑛 ≠ 𝐾) |
43 | 34, 16 | symgfvne 18806 |
. . . . . . . . . . 11
⊢ ((𝑄 ∈ 𝑃 ∧ 𝐾 ∈ 𝑁 ∧ 𝑛 ∈ 𝑁) → ((𝑄‘𝐾) = 𝐿 → (𝑛 ≠ 𝐾 → (𝑄‘𝑛) ≠ 𝐿))) |
44 | 40, 41, 42, 43 | syl3c 66 |
. . . . . . . . . 10
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄‘𝑛) ≠ 𝐿) |
45 | 36, 44 | jca 515 |
. . . . . . . . 9
⊢ ((((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) ∧ (𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿)) |
46 | 45 | exp42 439 |
. . . . . . . 8
⊢ ((𝑄 ∈ 𝑃 ∧ (𝑄‘𝐾) = 𝐿) → (𝐿 ∈ 𝑁 → (𝐾 ∈ 𝑁 → (𝑛 ∈ (𝑁 ∖ {𝐾}) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿))))) |
47 | 32, 46 | sylbi 220 |
. . . . . . 7
⊢ (𝑄 ∈ 𝑅 → (𝐿 ∈ 𝑁 → (𝐾 ∈ 𝑁 → (𝑛 ∈ (𝑁 ∖ {𝐾}) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿))))) |
48 | 47 | 3imp31 1114 |
. . . . . 6
⊢ ((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅) → (𝑛 ∈ (𝑁 ∖ {𝐾}) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿))) |
49 | 48 | 3ad2ant3 1137 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) → (𝑛 ∈ (𝑁 ∖ {𝐾}) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿))) |
50 | 49 | imp 410 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿)) |
51 | | eldifsn 4717 |
. . . 4
⊢ ((𝑄‘𝑛) ∈ (𝑁 ∖ {𝐿}) ↔ ((𝑄‘𝑛) ∈ 𝑁 ∧ (𝑄‘𝑛) ≠ 𝐿)) |
52 | 50, 51 | sylibr 237 |
. . 3
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑄‘𝑛) ∈ (𝑁 ∖ {𝐿})) |
53 | | ovexd 7270 |
. . 3
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛𝐴(𝑄‘𝑛)) ∈ V) |
54 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑖(𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) |
55 | | nfra1 3143 |
. . . . . 6
⊢
Ⅎ𝑖∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 |
56 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑖𝑆 |
57 | 56 | nfel2 2925 |
. . . . . 6
⊢
Ⅎ𝑖 𝐵 ∈ 𝑆 |
58 | 55, 57 | nfan 1907 |
. . . . 5
⊢
Ⅎ𝑖(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) |
59 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑖(𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅) |
60 | 54, 58, 59 | nf3an 1909 |
. . . 4
⊢
Ⅎ𝑖((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) |
61 | | nfcv 2907 |
. . . . 5
⊢
Ⅎ𝑖(𝑁 ∖ {𝐾}) |
62 | 61 | nfel2 2925 |
. . . 4
⊢
Ⅎ𝑖 𝑛 ∈ (𝑁 ∖ {𝐾}) |
63 | 60, 62 | nfan 1907 |
. . 3
⊢
Ⅎ𝑖(((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) |
64 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑗(𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) |
65 | | nfra2w 3152 |
. . . . . 6
⊢
Ⅎ𝑗∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 |
66 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑗𝑆 |
67 | 66 | nfel2 2925 |
. . . . . 6
⊢
Ⅎ𝑗 𝐵 ∈ 𝑆 |
68 | 65, 67 | nfan 1907 |
. . . . 5
⊢
Ⅎ𝑗(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) |
69 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑗(𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅) |
70 | 64, 68, 69 | nf3an 1909 |
. . . 4
⊢
Ⅎ𝑗((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) |
71 | | nfcv 2907 |
. . . . 5
⊢
Ⅎ𝑗(𝑁 ∖ {𝐾}) |
72 | 71 | nfel2 2925 |
. . . 4
⊢
Ⅎ𝑗 𝑛 ∈ (𝑁 ∖ {𝐾}) |
73 | 70, 72 | nfan 1907 |
. . 3
⊢
Ⅎ𝑗(((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) |
74 | | nfcv 2907 |
. . 3
⊢
Ⅎ𝑗𝑛 |
75 | | nfcv 2907 |
. . 3
⊢
Ⅎ𝑖(𝑄‘𝑛) |
76 | | nfcv 2907 |
. . 3
⊢
Ⅎ𝑖(𝑛𝐴(𝑄‘𝑛)) |
77 | | nfcv 2907 |
. . 3
⊢
Ⅎ𝑗(𝑛𝐴(𝑄‘𝑛)) |
78 | 26, 27, 28, 29, 52, 53, 63, 73, 74, 75, 76, 77 | ovmpodxf 7381 |
. 2
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))(𝑄‘𝑛)) = (𝑛𝐴(𝑄‘𝑛))) |
79 | 25, 78 | eqtr4d 2782 |
1
⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧
(∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))(𝑄‘𝑛))) |