Metamath Proof Explorer

Theorem mdetunilem3

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 · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
Assertion mdetunilem3 ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ) ∧ ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )

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 simp23 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ) ∧ ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) )
15 simp3l ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ) ∧ ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) )
16 simp3r ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ) ∧ ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) )
17 simprl ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ) ) → 𝐺 ∈ 𝐵 )
18 simprr ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ) ) → 𝐻 ∈ 𝑁 )
19 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ) ) → 𝐸 ∈ 𝐵 )
20 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ) ) → 𝐹 ∈ 𝐵 )
21 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ) ) → 𝜑 )
22 21 12 syl ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
23 reseq1 ⊢ ( 𝑥 = 𝐸 → ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) )
24 23 eqeq1d ⊢ ( 𝑥 = 𝐸 → ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ↔ ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ) )
25 reseq1 ⊢ ( 𝑥 = 𝐸 → ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) )
26 25 eqeq1d ⊢ ( 𝑥 = 𝐸 → ( ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ↔ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) )
27 25 eqeq1d ⊢ ( 𝑥 = 𝐸 → ( ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ↔ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) )
28 24 26 27 3anbi123d ⊢ ( 𝑥 = 𝐸 → ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ↔ ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ) )
29 fveq2 ⊢ ( 𝑥 = 𝐸 → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝐸 ) )
30 29 eqeq1d ⊢ ( 𝑥 = 𝐸 → ( ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ↔ ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
31 28 30 imbi12d ⊢ ( 𝑥 = 𝐸 → ( ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) ↔ ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) ) )
32 31 2ralbidv ⊢ ( 𝑥 = 𝐸 → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) ) )
33 reseq1 ⊢ ( 𝑦 = 𝐹 → ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) = ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) )
34 33 oveq1d ⊢ ( 𝑦 = 𝐹 → ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) )
35 34 eqeq2d ⊢ ( 𝑦 = 𝐹 → ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ↔ ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ) )
36 reseq1 ⊢ ( 𝑦 = 𝐹 → ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) )
37 36 eqeq2d ⊢ ( 𝑦 = 𝐹 → ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ↔ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) )
38 35 37 3anbi12d ⊢ ( 𝑦 = 𝐹 → ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ↔ ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ) )
39 fveq2 ⊢ ( 𝑦 = 𝐹 → ( 𝐷 ‘ 𝑦 ) = ( 𝐷 ‘ 𝐹 ) )
40 39 oveq1d ⊢ ( 𝑦 = 𝐹 → ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝑧 ) ) )
41 40 eqeq2d ⊢ ( 𝑦 = 𝐹 → ( ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ↔ ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
42 38 41 imbi12d ⊢ ( 𝑦 = 𝐹 → ( ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) ↔ ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝑧 ) ) ) ) )
43 42 2ralbidv ⊢ ( 𝑦 = 𝐹 → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝑧 ) ) ) ) )
44 32 43 rspc2va ⊢ ( ( ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
45 19 20 22 44 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ) ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
46 reseq1 ⊢ ( 𝑧 = 𝐺 → ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) = ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) )
47 46 oveq2d ⊢ ( 𝑧 = 𝐺 → ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) )
48 47 eqeq2d ⊢ ( 𝑧 = 𝐺 → ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ↔ ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ) )
49 reseq1 ⊢ ( 𝑧 = 𝐺 → ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) )
50 49 eqeq2d ⊢ ( 𝑧 = 𝐺 → ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ↔ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) )
51 48 50 3anbi13d ⊢ ( 𝑧 = 𝐺 → ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ↔ ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ) )
52 fveq2 ⊢ ( 𝑧 = 𝐺 → ( 𝐷 ‘ 𝑧 ) = ( 𝐷 ‘ 𝐺 ) )
53 52 oveq2d ⊢ ( 𝑧 = 𝐺 → ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝑧 ) ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )
54 53 eqeq2d ⊢ ( 𝑧 = 𝐺 → ( ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝑧 ) ) ↔ ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) )
55 51 54 imbi12d ⊢ ( 𝑧 = 𝐺 → ( ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝑧 ) ) ) ↔ ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) ) )
56 sneq ⊢ ( 𝑤 = 𝐻 → { 𝑤 } = { 𝐻 } )
57 56 xpeq1d ⊢ ( 𝑤 = 𝐻 → ( { 𝑤 } × 𝑁 ) = ( { 𝐻 } × 𝑁 ) )
58 57 reseq2d ⊢ ( 𝑤 = 𝐻 → ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) )
59 57 reseq2d ⊢ ( 𝑤 = 𝐻 → ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) = ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) )
60 57 reseq2d ⊢ ( 𝑤 = 𝐻 → ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) = ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) )
61 59 60 oveq12d ⊢ ( 𝑤 = 𝐻 → ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) )
62 58 61 eqeq12d ⊢ ( 𝑤 = 𝐻 → ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ↔ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ) )
63 56 difeq2d ⊢ ( 𝑤 = 𝐻 → ( 𝑁 ∖ { 𝑤 } ) = ( 𝑁 ∖ { 𝐻 } ) )
64 63 xpeq1d ⊢ ( 𝑤 = 𝐻 → ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) = ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) )
65 64 reseq2d ⊢ ( 𝑤 = 𝐻 → ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) )
66 64 reseq2d ⊢ ( 𝑤 = 𝐻 → ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) )
67 65 66 eqeq12d ⊢ ( 𝑤 = 𝐻 → ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ↔ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) )
68 64 reseq2d ⊢ ( 𝑤 = 𝐻 → ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) )
69 65 68 eqeq12d ⊢ ( 𝑤 = 𝐻 → ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ↔ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) )
70 62 67 69 3anbi123d ⊢ ( 𝑤 = 𝐻 → ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ↔ ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) )
71 70 imbi1d ⊢ ( 𝑤 = 𝐻 → ( ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) ↔ ( ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) ) )
72 55 71 rspc2va ⊢ ( ( ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝑧 ) ) ) ) → ( ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) )
73 17 18 45 72 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ) ) → ( ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) )
74 73 3adantr3 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ) ) → ( ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) )
75 74 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ) ∧ ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) ) )
76 14 15 16 75 mp3and ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵 ) ∧ ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( 𝐹 ↾ ( { 𝐻 } × 𝑁 ) ) ∘f + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ) ∧ ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( ( 𝐷 ‘ 𝐹 ) + ( 𝐷 ‘ 𝐺 ) ) )