Metamath Proof Explorer

Theorem mdetunilem6

Description: Lemma for mdetuni . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses mdetuni.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetuni.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mdetuni.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mdetuni.0g ⊢ 0 = ( 0g ‘ 𝑅 )
mdetuni.1r ⊢ 1 = ( 1r ‘ 𝑅 )
mdetuni.pg ⊢ + = ( +g ‘ 𝑅 )
mdetuni.tg ⊢ · = ( .r ‘ 𝑅 )
mdetuni.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mdetuni.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mdetuni.ff ⊢ ( 𝜑 → 𝐷 : 𝐵 ⟶ 𝐾 )
mdetuni.al ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) )
mdetuni.li ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
mdetuni.sc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
mdetunilem6.ph ⊢ ( 𝜓 → 𝜑 )
mdetunilem6.ef ⊢ ( 𝜓 → ( 𝐸 ∈ 𝑁 ∧ 𝐹 ∈ 𝑁 ∧ 𝐸 ≠ 𝐹 ) )
mdetunilem6.gh ⊢ ( ( 𝜓 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐺 ∈ 𝐾 ∧ 𝐻 ∈ 𝐾 ) )
mdetunilem6.i ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐼 ∈ 𝐾 )
Assertion mdetunilem6 ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdetuni.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mdetuni.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 mdetuni.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 mdetuni.0g ⊢ 0 = ( 0g ‘ 𝑅 )
5 mdetuni.1r ⊢ 1 = ( 1r ‘ 𝑅 )
6 mdetuni.pg ⊢ + = ( +g ‘ 𝑅 )
7 mdetuni.tg ⊢ · = ( .r ‘ 𝑅 )
8 mdetuni.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
9 mdetuni.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 mdetuni.ff ⊢ ( 𝜑 → 𝐷 : 𝐵 ⟶ 𝐾 )
11 mdetuni.al ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) )
12 mdetuni.li ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
13 mdetuni.sc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
14 mdetunilem6.ph ⊢ ( 𝜓 → 𝜑 )
15 mdetunilem6.ef ⊢ ( 𝜓 → ( 𝐸 ∈ 𝑁 ∧ 𝐹 ∈ 𝑁 ∧ 𝐸 ≠ 𝐹 ) )
16 mdetunilem6.gh ⊢ ( ( 𝜓 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐺 ∈ 𝐾 ∧ 𝐻 ∈ 𝐾 ) )
17 mdetunilem6.i ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐼 ∈ 𝐾 )
18 15 simp1d ⊢ ( 𝜓 → 𝐸 ∈ 𝑁 )
19 16 simprd ⊢ ( ( 𝜓 ∧ 𝑏 ∈ 𝑁 ) → 𝐻 ∈ 𝐾 )
20 19 3adant2 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐻 ∈ 𝐾 )
21 16 simpld ⊢ ( ( 𝜓 ∧ 𝑏 ∈ 𝑁 ) → 𝐺 ∈ 𝐾 )
22 21 3adant2 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐺 ∈ 𝐾 )
23 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
24 14 9 23 3syl ⊢ ( 𝜓 → 𝑅 ∈ Grp )
25 24 adantr ⊢ ( ( 𝜓 ∧ 𝑏 ∈ 𝑁 ) → 𝑅 ∈ Grp )
26 3 6 grpcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐻 ∈ 𝐾 ∧ 𝐺 ∈ 𝐾 ) → ( 𝐻 + 𝐺 ) ∈ 𝐾 )
27 25 19 21 26 syl3anc ⊢ ( ( 𝜓 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐻 + 𝐺 ) ∈ 𝐾 )
28 27 3adant2 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐻 + 𝐺 ) ∈ 𝐾 )
29 28 17 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ∈ 𝐾 )
30 20 22 29 3jca ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐻 ∈ 𝐾 ∧ 𝐺 ∈ 𝐾 ∧ if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ∈ 𝐾 ) )
31 1 2 3 4 5 6 7 8 9 10 11 12 13 14 18 30 mdetunilem5 ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) ) ) )
32 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 27 17 mdetunilem2 ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) ) = 0 )
33 15 simp2d ⊢ ( 𝜓 → 𝐹 ∈ 𝑁 )
34 20 17 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ∈ 𝐾 )
35 20 22 34 3jca ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐻 ∈ 𝐾 ∧ 𝐺 ∈ 𝐾 ∧ if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ∈ 𝐾 ) )
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 33 35 mdetunilem5 ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) ) )
37 15 simp3d ⊢ ( 𝜓 → 𝐸 ≠ 𝐹 )
38 37 necomd ⊢ ( 𝜓 → 𝐹 ≠ 𝐸 )
39 33 18 38 3jca ⊢ ( 𝜓 → ( 𝐹 ∈ 𝑁 ∧ 𝐸 ∈ 𝑁 ∧ 𝐹 ≠ 𝐸 ) )
40 1 2 3 4 5 6 7 8 9 10 11 12 13 14 39 19 17 mdetunilem2 ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) = 0 )
41 40 oveq1d ⊢ ( 𝜓 → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) ) = ( 0 + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) ) )
42 37 neneqd ⊢ ( 𝜓 → ¬ 𝐸 = 𝐹 )
43 eqtr2 ⊢ ( ( 𝑎 = 𝐸 ∧ 𝑎 = 𝐹 ) → 𝐸 = 𝐹 )
44 42 43 nsyl ⊢ ( 𝜓 → ¬ ( 𝑎 = 𝐸 ∧ 𝑎 = 𝐹 ) )
45 44 3ad2ant1 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ¬ ( 𝑎 = 𝐸 ∧ 𝑎 = 𝐹 ) )
46 ifcomnan ⊢ ( ¬ ( 𝑎 = 𝐸 ∧ 𝑎 = 𝐹 ) → if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) = if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) )
47 45 46 syl ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) = if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) )
48 47 mpoeq3dva ⊢ ( 𝜓 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) )
49 48 fveq2d ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) )
50 14 10 syl ⊢ ( 𝜓 → 𝐷 : 𝐵 ⟶ 𝐾 )
51 14 8 syl ⊢ ( 𝜓 → 𝑁 ∈ Fin )
52 22 17 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ∈ 𝐾 )
53 20 52 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ∈ 𝐾 )
54 1 3 2 51 24 53 matbas2d ⊢ ( 𝜓 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ∈ 𝐵 )
55 50 54 ffvelrnd ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) ∈ 𝐾 )
56 49 55 eqeltrrd ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) ∈ 𝐾 )
57 3 6 4 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) ∈ 𝐾 ) → ( 0 + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) )
58 24 56 57 syl2anc ⊢ ( 𝜓 → ( 0 + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) )
59 36 41 58 3eqtrd ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) )
60 ifcomnan ⊢ ( ¬ ( 𝑎 = 𝐸 ∧ 𝑎 = 𝐹 ) → if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) = if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) )
61 45 60 syl ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) = if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) )
62 61 mpoeq3dva ⊢ ( 𝜓 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) )
63 62 fveq2d ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐻 , 𝐼 ) ) ) ) )
64 59 63 49 3eqtr4d ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) )
65 22 17 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ∈ 𝐾 )
66 20 22 65 3jca ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐻 ∈ 𝐾 ∧ 𝐺 ∈ 𝐾 ∧ if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ∈ 𝐾 ) )
67 1 2 3 4 5 6 7 8 9 10 11 12 13 14 33 66 mdetunilem5 ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) ) )
68 1 2 3 4 5 6 7 8 9 10 11 12 13 14 39 21 17 mdetunilem2 ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) = 0 )
69 68 oveq2d ⊢ ( 𝜓 → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐺 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) + 0 ) )
70 ifcomnan ⊢ ( ¬ ( 𝑎 = 𝐸 ∧ 𝑎 = 𝐹 ) → if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) = if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) )
71 45 70 syl ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) = if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) )
72 71 mpoeq3dva ⊢ ( 𝜓 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) )
73 72 fveq2d ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) )
74 20 17 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ∈ 𝐾 )
75 22 74 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ∈ 𝐾 )
76 1 3 2 51 24 75 matbas2d ⊢ ( 𝜓 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ∈ 𝐵 )
77 50 76 ffvelrnd ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) ∈ 𝐾 )
78 73 77 eqeltrrd ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) ∈ 𝐾 )
79 3 6 4 grprid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) + 0 ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) )
80 24 78 79 syl2anc ⊢ ( 𝜓 → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) + 0 ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) )
81 67 69 80 3eqtrd ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , 𝐻 , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) )
82 ifcomnan ⊢ ( ¬ ( 𝑎 = 𝐸 ∧ 𝑎 = 𝐹 ) → if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) = if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) )
83 45 82 syl ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) = if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) )
84 83 mpoeq3dva ⊢ ( 𝜓 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) )
85 84 fveq2d ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , if ( 𝑎 = 𝐸 , 𝐺 , 𝐼 ) ) ) ) )
86 81 85 73 3eqtr4d ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) )
87 64 86 oveq12d ⊢ ( 𝜓 → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , ( 𝐻 + 𝐺 ) , 𝐼 ) ) ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) ) )
88 31 32 87 3eqtr3rd ⊢ ( 𝜓 → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) ) = 0 )
89 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
90 3 6 4 89 grpinvid1 ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) ∈ 𝐾 ∧ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) ∈ 𝐾 ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) ↔ ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) ) = 0 ) )
91 24 55 77 90 syl3anc ⊢ ( 𝜓 → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) ↔ ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) ) = 0 ) )
92 88 91 mpbird ⊢ ( 𝜓 → ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) )
93 92 eqcomd ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , if ( 𝑎 = 𝐹 , 𝐻 , 𝐼 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐻 , if ( 𝑎 = 𝐹 , 𝐺 , 𝐼 ) ) ) ) ) )