Metamath Proof Explorer

Theorem gsummatr01lem4

Description: Lemma 2 for gsummatr01 . (Contributed by AV, 8-Jan-2019)

Ref Expression
Hypotheses gsummatr01.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
gsummatr01.r ⊢ 𝑅 = { 𝑟 ∈ 𝑃 ∣ ( 𝑟 ‘ 𝐾 ) = 𝐿 }
gsummatr01.0 ⊢ 0 = ( 0g ‘ 𝐺 )
gsummatr01.s ⊢ 𝑆 = ( Base ‘ 𝐺 )
Assertion gsummatr01lem4 ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝐴 𝑗 ) ) ( 𝑄 ‘ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 gsummatr01.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 gsummatr01.r ⊢ 𝑅 = { 𝑟 ∈ 𝑃 ∣ ( 𝑟 ‘ 𝐾 ) = 𝐿 }
3 gsummatr01.0 ⊢ 0 = ( 0g ‘ 𝐺 )
4 gsummatr01.s ⊢ 𝑆 = ( Base ‘ 𝐺 )
5 eqidd ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) )
6 eqeq1 ⊢ ( 𝑖 = 𝑛 → ( 𝑖 = 𝐾 ↔ 𝑛 = 𝐾 ) )
7 6 adantr ⊢ ( ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) → ( 𝑖 = 𝐾 ↔ 𝑛 = 𝐾 ) )
8 eqeq1 ⊢ ( 𝑗 = ( 𝑄 ‘ 𝑛 ) → ( 𝑗 = 𝐿 ↔ ( 𝑄 ‘ 𝑛 ) = 𝐿 ) )
9 8 adantl ⊢ ( ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) → ( 𝑗 = 𝐿 ↔ ( 𝑄 ‘ 𝑛 ) = 𝐿 ) )
10 9 ifbid ⊢ ( ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) → if ( 𝑗 = 𝐿 , 0 , 𝐵 ) = if ( ( 𝑄 ‘ 𝑛 ) = 𝐿 , 0 , 𝐵 ) )
11 oveq12 ⊢ ( ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) → ( 𝑖 𝐴 𝑗 ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
12 7 10 11 ifbieq12d ⊢ ( ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = if ( 𝑛 = 𝐾 , if ( ( 𝑄 ‘ 𝑛 ) = 𝐿 , 0 , 𝐵 ) , ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ) )
13 eldifsni ⊢ ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → 𝑛 ≠ 𝐾 )
14 13 neneqd ⊢ ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ¬ 𝑛 = 𝐾 )
15 14 iffalsed ⊢ ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → if ( 𝑛 = 𝐾 , if ( ( 𝑄 ‘ 𝑛 ) = 𝐿 , 0 , 𝐵 ) , ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
16 15 adantl ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → if ( 𝑛 = 𝐾 , if ( ( 𝑄 ‘ 𝑛 ) = 𝐿 , 0 , 𝐵 ) , ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
17 12 16 sylan9eqr ⊢ ( ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
18 eldifi ⊢ ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → 𝑛 ∈ 𝑁 )
19 18 adantl ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → 𝑛 ∈ 𝑁 )
20 1 2 gsummatr01lem1 ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 )
21 18 20 sylan2 ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 )
22 ovexd ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ V )
23 5 17 19 21 22 ovmpod ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
24 23 ex ⊢ ( 𝑄 ∈ 𝑅 → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ) )
25 24 3ad2ant3 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ) )
26 25 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ) )
27 26 imp ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
28 eqidd ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝐴 𝑗 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝐴 𝑗 ) ) )
29 11 adantl ⊢ ( ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) ) → ( 𝑖 𝐴 𝑗 ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
30 eqidd ⊢ ( ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ 𝑖 = 𝑛 ) → ( 𝑁 ∖ { 𝐿 } ) = ( 𝑁 ∖ { 𝐿 } ) )
31 simpr ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) )
32 fveq1 ⊢ ( 𝑟 = 𝑄 → ( 𝑟 ‘ 𝐾 ) = ( 𝑄 ‘ 𝐾 ) )
33 32 eqeq1d ⊢ ( 𝑟 = 𝑄 → ( ( 𝑟 ‘ 𝐾 ) = 𝐿 ↔ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
34 33 2 elrab2 ⊢ ( 𝑄 ∈ 𝑅 ↔ ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
35 simpll ⊢ ( ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) → 𝑄 ∈ 𝑃 )
36 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
37 36 1 symgfv ⊢ ( ( 𝑄 ∈ 𝑃 ∧ 𝑛 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 )
38 35 18 37 syl2an ⊢ ( ( ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 )
39 35 adantr ⊢ ( ( ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → 𝑄 ∈ 𝑃 )
40 simplrr ⊢ ( ( ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → 𝐾 ∈ 𝑁 )
41 18 adantl ⊢ ( ( ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → 𝑛 ∈ 𝑁 )
42 39 40 41 3jca ⊢ ( ( ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ∈ 𝑃 ∧ 𝐾 ∈ 𝑁 ∧ 𝑛 ∈ 𝑁 ) )
43 simpllr ⊢ ( ( ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ‘ 𝐾 ) = 𝐿 )
44 13 adantl ⊢ ( ( ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → 𝑛 ≠ 𝐾 )
45 36 1 symgfvne ⊢ ( ( 𝑄 ∈ 𝑃 ∧ 𝐾 ∈ 𝑁 ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑄 ‘ 𝐾 ) = 𝐿 → ( 𝑛 ≠ 𝐾 → ( 𝑄 ‘ 𝑛 ) ≠ 𝐿 ) ) )
46 42 43 44 45 syl3c ⊢ ( ( ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ‘ 𝑛 ) ≠ 𝐿 )
47 38 46 jca ⊢ ( ( ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) ∧ ( 𝐿 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑛 ) ≠ 𝐿 ) )
48 47 exp42 ⊢ ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) → ( 𝐿 ∈ 𝑁 → ( 𝐾 ∈ 𝑁 → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑛 ) ≠ 𝐿 ) ) ) ) )
49 34 48 sylbi ⊢ ( 𝑄 ∈ 𝑅 → ( 𝐿 ∈ 𝑁 → ( 𝐾 ∈ 𝑁 → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑛 ) ≠ 𝐿 ) ) ) ) )
50 49 3imp31 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑛 ) ≠ 𝐿 ) ) )
51 50 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑛 ) ≠ 𝐿 ) ) )
52 51 imp ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑛 ) ≠ 𝐿 ) )
53 eldifsn ⊢ ( ( 𝑄 ‘ 𝑛 ) ∈ ( 𝑁 ∖ { 𝐿 } ) ↔ ( ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 ∧ ( 𝑄 ‘ 𝑛 ) ≠ 𝐿 ) )
54 52 53 sylibr ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ‘ 𝑛 ) ∈ ( 𝑁 ∖ { 𝐿 } ) )
55 ovexd ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ V )
56 nfv ⊢ Ⅎ 𝑖 ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin )
57 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆
58 nfcv ⊢ Ⅎ 𝑖 𝑆
59 58 nfel2 ⊢ Ⅎ 𝑖 𝐵 ∈ 𝑆
60 57 59 nfan ⊢ Ⅎ 𝑖 ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 )
61 nfv ⊢ Ⅎ 𝑖 ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 )
62 56 60 61 nf3an ⊢ Ⅎ 𝑖 ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) )
63 nfcv ⊢ Ⅎ 𝑖 ( 𝑁 ∖ { 𝐾 } )
64 63 nfel2 ⊢ Ⅎ 𝑖 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } )
65 62 64 nfan ⊢ Ⅎ 𝑖 ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) )
66 nfv ⊢ Ⅎ 𝑗 ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin )
67 nfra2w ⊢ Ⅎ 𝑗 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆
68 nfcv ⊢ Ⅎ 𝑗 𝑆
69 68 nfel2 ⊢ Ⅎ 𝑗 𝐵 ∈ 𝑆
70 67 69 nfan ⊢ Ⅎ 𝑗 ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 )
71 nfv ⊢ Ⅎ 𝑗 ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 )
72 66 70 71 nf3an ⊢ Ⅎ 𝑗 ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) )
73 nfcv ⊢ Ⅎ 𝑗 ( 𝑁 ∖ { 𝐾 } )
74 73 nfel2 ⊢ Ⅎ 𝑗 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } )
75 72 74 nfan ⊢ Ⅎ 𝑗 ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) )
76 nfcv ⊢ Ⅎ 𝑗 𝑛
77 nfcv ⊢ Ⅎ 𝑖 ( 𝑄 ‘ 𝑛 )
78 nfcv ⊢ Ⅎ 𝑖 ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) )
79 nfcv ⊢ Ⅎ 𝑗 ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) )
80 28 29 30 31 54 55 65 75 76 77 78 79 ovmpodxf ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝐴 𝑗 ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
81 27 80 eqtr4d ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝐴 𝑗 ) ) ( 𝑄 ‘ 𝑛 ) ) )