This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mdetunilem5

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 · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
mdetunilem5.ph ⊢ ( 𝜓 → 𝜑 )
mdetunilem5.e ⊢ ( 𝜓 → 𝐸 ∈ 𝑁 )
mdetunilem5.fgh ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐾 ∧ 𝐻 ∈ 𝐾 ) )
Assertion mdetunilem5 ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ 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 mdetunilem5.ph ⊢ ( 𝜓 → 𝜑 )
15 mdetunilem5.e ⊢ ( 𝜓 → 𝐸 ∈ 𝑁 )
16 mdetunilem5.fgh ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐾 ∧ 𝐻 ∈ 𝐾 ) )
17 14 8 syl ⊢ ( 𝜓 → 𝑁 ∈ Fin )
18 14 9 syl ⊢ ( 𝜓 → 𝑅 ∈ Ring )
19 18 3ad2ant1 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑅 ∈ Ring )
20 16 simp1d ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐹 ∈ 𝐾 )
21 16 simp2d ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐺 ∈ 𝐾 )
22 3 6 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐾 ) → ( 𝐹 + 𝐺 ) ∈ 𝐾 )
23 19 20 21 22 syl3anc ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐹 + 𝐺 ) ∈ 𝐾 )
24 16 simp3d ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐻 ∈ 𝐾 )
25 23 24 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ∈ 𝐾 )
26 1 3 2 17 18 25 matbas2d ⊢ ( 𝜓 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ∈ 𝐵 )
27 20 24 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ∈ 𝐾 )
28 1 3 2 17 18 27 matbas2d ⊢ ( 𝜓 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ∈ 𝐵 )
29 21 24 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ∈ 𝐾 )
30 1 3 2 17 18 29 matbas2d ⊢ ( 𝜓 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ∈ 𝐵 )
31 snex ⊢ { 𝐸 } ∈ V
32 31 a1i ⊢ ( 𝜓 → { 𝐸 } ∈ V )
33 15 snssd ⊢ ( 𝜓 → { 𝐸 } ⊆ 𝑁 )
34 33 3ad2ant1 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ { 𝐸 } ∧ 𝑏 ∈ 𝑁 ) → { 𝐸 } ⊆ 𝑁 )
35 simp2 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ { 𝐸 } ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ { 𝐸 } )
36 34 35 sseldd ⊢ ( ( 𝜓 ∧ 𝑎 ∈ { 𝐸 } ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
37 36 20 syld3an2 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ { 𝐸 } ∧ 𝑏 ∈ 𝑁 ) → 𝐹 ∈ 𝐾 )
38 36 21 syld3an2 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ { 𝐸 } ∧ 𝑏 ∈ 𝑁 ) → 𝐺 ∈ 𝐾 )
39 eqidd ⊢ ( 𝜓 → ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐹 ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐹 ) )
40 eqidd ⊢ ( 𝜓 → ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐺 ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐺 ) )
41 32 17 37 38 39 40 offval22 ⊢ ( 𝜓 → ( ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐹 ) ∘f + ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐺 ) ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ ( 𝐹 + 𝐺 ) ) )
42 41 eqcomd ⊢ ( 𝜓 → ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ ( 𝐹 + 𝐺 ) ) = ( ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐹 ) ∘f + ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐺 ) ) )
43 mposnif ⊢ ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ ( 𝐹 + 𝐺 ) )
44 mposnif ⊢ ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐹 )
45 mposnif ⊢ ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐺 )
46 44 45 oveq12i ⊢ ( ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ∘f + ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ) = ( ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐹 ) ∘f + ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ 𝐺 ) )
47 42 43 46 3eqtr4g ⊢ ( 𝜓 → ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) = ( ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ∘f + ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ) )
48 ssid ⊢ 𝑁 ⊆ 𝑁
49 resmpo ⊢ ( ( { 𝐸 } ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) )
50 33 48 49 sylancl ⊢ ( 𝜓 → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) )
51 resmpo ⊢ ( ( { 𝐸 } ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) )
52 33 48 51 sylancl ⊢ ( 𝜓 → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) )
53 resmpo ⊢ ( ( { 𝐸 } ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) )
54 33 48 53 sylancl ⊢ ( 𝜓 → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) = ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) )
55 52 54 oveq12d ⊢ ( 𝜓 → ( ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) ∘f + ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) ) = ( ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ∘f + ( 𝑎 ∈ { 𝐸 } , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ) )
56 47 50 55 3eqtr4d ⊢ ( 𝜓 → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) = ( ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) ∘f + ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) ) )
57 eldifsni ⊢ ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) → 𝑎 ≠ 𝐸 )
58 57 3ad2ant2 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ≠ 𝐸 )
59 58 neneqd ⊢ ( ( 𝜓 ∧ 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) ∧ 𝑏 ∈ 𝑁 ) → ¬ 𝑎 = 𝐸 )
60 iffalse ⊢ ( ¬ 𝑎 = 𝐸 → if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) = 𝐻 )
61 iffalse ⊢ ( ¬ 𝑎 = 𝐸 → if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) = 𝐻 )
62 60 61 eqtr4d ⊢ ( ¬ 𝑎 = 𝐸 → if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) = if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) )
63 59 62 syl ⊢ ( ( 𝜓 ∧ 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) = if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) )
64 63 mpoeq3dva ⊢ ( 𝜓 → ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) = ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) )
65 difss ⊢ ( 𝑁 ∖ { 𝐸 } ) ⊆ 𝑁
66 resmpo ⊢ ( ( ( 𝑁 ∖ { 𝐸 } ) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) = ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) )
67 65 48 66 mp2an ⊢ ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) = ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) )
68 resmpo ⊢ ( ( ( 𝑁 ∖ { 𝐸 } ) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) = ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) )
69 65 48 68 mp2an ⊢ ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) = ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) )
70 64 67 69 3eqtr4g ⊢ ( 𝜓 → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) = ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) )
71 iffalse ⊢ ( ¬ 𝑎 = 𝐸 → if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) = 𝐻 )
72 60 71 eqtr4d ⊢ ( ¬ 𝑎 = 𝐸 → if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) = if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) )
73 59 72 syl ⊢ ( ( 𝜓 ∧ 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) = if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) )
74 73 mpoeq3dva ⊢ ( 𝜓 → ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) = ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) )
75 resmpo ⊢ ( ( ( 𝑁 ∖ { 𝐸 } ) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) = ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) )
76 65 48 75 mp2an ⊢ ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) = ( 𝑎 ∈ ( 𝑁 ∖ { 𝐸 } ) , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) )
77 74 67 76 3eqtr4g ⊢ ( 𝜓 → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) = ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) )
78 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem3 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ∈ 𝐵 ) ∧ ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ∈ 𝐵 ∧ 𝐸 ∈ 𝑁 ∧ ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) = ( ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) ∘f + ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ↾ ( { 𝐸 } × 𝑁 ) ) ) ) ∧ ( ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) = ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) ∧ ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) = ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ↾ ( ( 𝑁 ∖ { 𝐸 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ) ) )
79 14 26 28 30 15 56 70 77 78 syl332anc ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , ( 𝐹 + 𝐺 ) , 𝐻 ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , 𝐻 ) ) ) + ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐺 , 𝐻 ) ) ) ) )