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 + ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ) ∧ ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐹 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐷𝐸 ) = ( ( 𝐷𝐹 ) + ( 𝐷𝐺 ) ) )