Metamath Proof Explorer

Theorem mdetuni0

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 · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
mdetuni.e ⊢ 𝐸 = ( 𝑁 maDet 𝑅 )
mdetuni.cr ⊢ ( 𝜑 → 𝑅 ∈ CRing )
mdetuni.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion mdetuni0 ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) )

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 mdetuni.e ⊢ 𝐸 = ( 𝑁 maDet 𝑅 )
15 mdetuni.cr ⊢ ( 𝜑 → 𝑅 ∈ CRing )
16 mdetuni.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
17 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
18 9 17 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑅 ∈ Grp )
20 10 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑎 ) ∈ 𝐾 )
21 9 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑅 ∈ Ring )
22 8 9 jca ⊢ ( 𝜑 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
23 1 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
24 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
25 2 24 ringidcl ⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
26 22 23 25 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
27 10 26 ffvelrnd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 )
29 14 1 2 3 mdetf ⊢ ( 𝑅 ∈ CRing → 𝐸 : 𝐵 ⟶ 𝐾 )
30 15 29 syl ⊢ ( 𝜑 → 𝐸 : 𝐵 ⟶ 𝐾 )
31 30 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐸 ‘ 𝑎 ) ∈ 𝐾 )
32 3 7 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 ∧ ( 𝐸 ‘ 𝑎 ) ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ∈ 𝐾 )
33 21 28 31 32 syl3anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ∈ 𝐾 )
34 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
35 3 34 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐷 ‘ 𝑎 ) ∈ 𝐾 ∧ ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ∈ 𝐾 ) → ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ∈ 𝐾 )
36 19 20 33 35 syl3anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ∈ 𝐾 )
37 36 fmpttd ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) : 𝐵 ⟶ 𝐾 )
38 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) → 𝑏 ∈ 𝐵 )
39 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑏 ) )
40 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐸 ‘ 𝑎 ) = ( 𝐸 ‘ 𝑏 ) )
41 40 oveq2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) )
42 39 41 oveq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) = ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) )
43 eqid ⊢ ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) = ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) )
44 ovex ⊢ ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) ∈ V
45 42 43 44 fvmpt ⊢ ( 𝑏 ∈ 𝐵 → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) )
46 38 45 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) )
47 46 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) )
48 simp1 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝜑 )
49 simp21 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝑏 ∈ 𝐵 )
50 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) )
51 oveq2 ⊢ ( 𝑒 = 𝑤 → ( 𝑐 𝑏 𝑒 ) = ( 𝑐 𝑏 𝑤 ) )
52 oveq2 ⊢ ( 𝑒 = 𝑤 → ( 𝑑 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑤 ) )
53 51 52 eqeq12d ⊢ ( 𝑒 = 𝑤 → ( ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ↔ ( 𝑐 𝑏 𝑤 ) = ( 𝑑 𝑏 𝑤 ) ) )
54 53 cbvralvw ⊢ ( ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ↔ ∀ 𝑤 ∈ 𝑁 ( 𝑐 𝑏 𝑤 ) = ( 𝑑 𝑏 𝑤 ) )
55 50 54 sylib ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ∀ 𝑤 ∈ 𝑁 ( 𝑐 𝑏 𝑤 ) = ( 𝑑 𝑏 𝑤 ) )
56 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝑐 ∈ 𝑁 )
57 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝑑 ∈ 𝑁 )
58 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝑐 ≠ 𝑑 )
59 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem1 ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑐 𝑏 𝑤 ) = ( 𝑑 𝑏 𝑤 ) ) ∧ ( 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ∧ 𝑐 ≠ 𝑑 ) ) → ( 𝐷 ‘ 𝑏 ) = 0 )
60 48 49 55 56 57 58 59 syl33anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( 𝐷 ‘ 𝑏 ) = 0 )
61 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝑅 ∈ CRing )
62 14 1 2 4 61 49 56 57 58 50 mdetralt ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( 𝐸 ‘ 𝑏 ) = 0 )
63 62 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · 0 ) )
64 60 63 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) = ( 0 ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · 0 ) ) )
65 3 7 4 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · 0 ) = 0 )
66 9 27 65 syl2anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · 0 ) = 0 )
67 66 oveq2d ⊢ ( 𝜑 → ( 0 ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · 0 ) ) = ( 0 ( -g ‘ 𝑅 ) 0 ) )
68 3 4 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐾 )
69 3 4 34 grpsubid ⊢ ( ( 𝑅 ∈ Grp ∧ 0 ∈ 𝐾 ) → ( 0 ( -g ‘ 𝑅 ) 0 ) = 0 )
70 18 68 69 syl2anc2 ⊢ ( 𝜑 → ( 0 ( -g ‘ 𝑅 ) 0 ) = 0 )
71 67 70 eqtrd ⊢ ( 𝜑 → ( 0 ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · 0 ) ) = 0 )
72 71 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( 0 ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · 0 ) ) = 0 )
73 47 64 72 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = 0 )
74 73 3expia ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) → ( ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = 0 ) )
75 74 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = 0 ) )
76 simp1 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝜑 )
77 simp2ll ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑏 ∈ 𝐵 )
78 simp2lr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑐 ∈ 𝐵 )
79 simp2rl ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑑 ∈ 𝐵 )
80 simp2rr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑒 ∈ 𝑁 )
81 simp31 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) )
82 simp32 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
83 simp33 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
84 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem3 ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ∧ ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ) ∧ ( ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ 𝑏 ) = ( ( 𝐷 ‘ 𝑐 ) + ( 𝐷 ‘ 𝑑 ) ) )
85 76 77 78 79 80 81 82 83 84 syl332anc ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ 𝑏 ) = ( ( 𝐷 ‘ 𝑐 ) + ( 𝐷 ‘ 𝑑 ) ) )
86 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑅 ∈ CRing )
87 14 1 2 6 86 77 78 79 80 81 82 83 mdetrlin ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝐸 ‘ 𝑏 ) = ( ( 𝐸 ‘ 𝑐 ) + ( 𝐸 ‘ 𝑑 ) ) )
88 87 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( ( 𝐸 ‘ 𝑐 ) + ( 𝐸 ‘ 𝑑 ) ) ) )
89 85 88 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) = ( ( ( 𝐷 ‘ 𝑐 ) + ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( ( 𝐸 ‘ 𝑐 ) + ( 𝐸 ‘ 𝑑 ) ) ) ) )
90 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑏 ∈ 𝐵 )
91 90 45 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) )
92 91 3adant3 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) )
93 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑐 ∈ 𝐵 )
94 fveq2 ⊢ ( 𝑎 = 𝑐 → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑐 ) )
95 fveq2 ⊢ ( 𝑎 = 𝑐 → ( 𝐸 ‘ 𝑎 ) = ( 𝐸 ‘ 𝑐 ) )
96 95 oveq2d ⊢ ( 𝑎 = 𝑐 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) )
97 94 96 oveq12d ⊢ ( 𝑎 = 𝑐 → ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) = ( ( 𝐷 ‘ 𝑐 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) ) )
98 ovex ⊢ ( ( 𝐷 ‘ 𝑐 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) ) ∈ V
99 97 43 98 fvmpt ⊢ ( 𝑐 ∈ 𝐵 → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) = ( ( 𝐷 ‘ 𝑐 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) ) )
100 93 99 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) = ( ( 𝐷 ‘ 𝑐 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) ) )
101 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑑 ∈ 𝐵 )
102 fveq2 ⊢ ( 𝑎 = 𝑑 → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑑 ) )
103 fveq2 ⊢ ( 𝑎 = 𝑑 → ( 𝐸 ‘ 𝑎 ) = ( 𝐸 ‘ 𝑑 ) )
104 103 oveq2d ⊢ ( 𝑎 = 𝑑 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) )
105 102 104 oveq12d ⊢ ( 𝑎 = 𝑑 → ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) = ( ( 𝐷 ‘ 𝑑 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) )
106 ovex ⊢ ( ( 𝐷 ‘ 𝑑 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ∈ V
107 105 43 106 fvmpt ⊢ ( 𝑑 ∈ 𝐵 → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) = ( ( 𝐷 ‘ 𝑑 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) )
108 101 107 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) = ( ( 𝐷 ‘ 𝑑 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) )
109 100 108 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) + ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) = ( ( ( 𝐷 ‘ 𝑐 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) ) + ( ( 𝐷 ‘ 𝑑 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ) )
110 ringabl ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
111 9 110 syl ⊢ ( 𝜑 → 𝑅 ∈ Abel )
112 111 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑅 ∈ Abel )
113 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝐷 : 𝐵 ⟶ 𝐾 )
114 113 93 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝐷 ‘ 𝑐 ) ∈ 𝐾 )
115 113 101 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝐷 ‘ 𝑑 ) ∈ 𝐾 )
116 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑅 ∈ Ring )
117 27 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 )
118 30 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝐸 : 𝐵 ⟶ 𝐾 )
119 118 93 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝐸 ‘ 𝑐 ) ∈ 𝐾 )
120 3 7 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 ∧ ( 𝐸 ‘ 𝑐 ) ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) ∈ 𝐾 )
121 116 117 119 120 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) ∈ 𝐾 )
122 118 101 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝐸 ‘ 𝑑 ) ∈ 𝐾 )
123 3 7 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 ∧ ( 𝐸 ‘ 𝑑 ) ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ∈ 𝐾 )
124 116 117 122 123 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ∈ 𝐾 )
125 3 6 34 ablsub4 ⊢ ( ( 𝑅 ∈ Abel ∧ ( ( 𝐷 ‘ 𝑐 ) ∈ 𝐾 ∧ ( 𝐷 ‘ 𝑑 ) ∈ 𝐾 ) ∧ ( ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) ∈ 𝐾 ∧ ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ∈ 𝐾 ) ) → ( ( ( 𝐷 ‘ 𝑐 ) + ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) + ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ) = ( ( ( 𝐷 ‘ 𝑐 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) ) + ( ( 𝐷 ‘ 𝑑 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ) )
126 112 114 115 121 124 125 syl122anc ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝐷 ‘ 𝑐 ) + ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) + ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ) = ( ( ( 𝐷 ‘ 𝑐 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) ) + ( ( 𝐷 ‘ 𝑑 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ) )
127 3 6 7 ringdi ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 ∧ ( 𝐸 ‘ 𝑐 ) ∈ 𝐾 ∧ ( 𝐸 ‘ 𝑑 ) ∈ 𝐾 ) ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( ( 𝐸 ‘ 𝑐 ) + ( 𝐸 ‘ 𝑑 ) ) ) = ( ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) + ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) )
128 116 117 119 122 127 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( ( 𝐸 ‘ 𝑐 ) + ( 𝐸 ‘ 𝑑 ) ) ) = ( ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) + ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) )
129 128 eqcomd ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) + ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( ( 𝐸 ‘ 𝑐 ) + ( 𝐸 ‘ 𝑑 ) ) ) )
130 129 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝐷 ‘ 𝑐 ) + ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑐 ) ) + ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ) = ( ( ( 𝐷 ‘ 𝑐 ) + ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( ( 𝐸 ‘ 𝑐 ) + ( 𝐸 ‘ 𝑑 ) ) ) ) )
131 109 126 130 3eqtr2d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) + ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) = ( ( ( 𝐷 ‘ 𝑐 ) + ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( ( 𝐸 ‘ 𝑐 ) + ( 𝐸 ‘ 𝑑 ) ) ) ) )
132 131 3adant3 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) + ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) = ( ( ( 𝐷 ‘ 𝑐 ) + ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( ( 𝐸 ‘ 𝑐 ) + ( 𝐸 ‘ 𝑑 ) ) ) ) )
133 89 92 132 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) + ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) )
134 133 3expia ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) + ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) ) )
135 134 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) → ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) + ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) ) )
136 135 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ∀ 𝑑 ∈ 𝐵 ∀ 𝑒 ∈ 𝑁 ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) + ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) ) )
137 136 ralrimivva ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑑 ∈ 𝐵 ∀ 𝑒 ∈ 𝑁 ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f + ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) + ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) ) )
138 simp1 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝜑 )
139 simp2ll ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑏 ∈ 𝐵 )
140 simp2lr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑐 ∈ 𝐾 )
141 simp2rl ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑑 ∈ 𝐵 )
142 simp2rr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑒 ∈ 𝑁 )
143 simp3l ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) )
144 simp3r ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
145 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem4 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝑁 ∧ ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ 𝑏 ) = ( 𝑐 · ( 𝐷 ‘ 𝑑 ) ) )
146 138 139 140 141 142 143 144 145 syl133anc ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ 𝑏 ) = ( 𝑐 · ( 𝐷 ‘ 𝑑 ) ) )
147 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑅 ∈ CRing )
148 14 1 2 3 7 147 139 140 141 142 143 144 mdetrsca ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝐸 ‘ 𝑏 ) = ( 𝑐 · ( 𝐸 ‘ 𝑑 ) ) )
149 148 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑐 · ( 𝐸 ‘ 𝑑 ) ) ) )
150 146 149 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) = ( ( 𝑐 · ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑐 · ( 𝐸 ‘ 𝑑 ) ) ) ) )
151 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑏 ∈ 𝐵 )
152 151 45 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) )
153 152 3adant3 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( ( 𝐷 ‘ 𝑏 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑏 ) ) ) )
154 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑑 ∈ 𝐵 )
155 154 107 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) = ( ( 𝐷 ‘ 𝑑 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) )
156 155 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) = ( 𝑐 · ( ( 𝐷 ‘ 𝑑 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ) )
157 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑅 ∈ Ring )
158 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑐 ∈ 𝐾 )
159 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝐷 : 𝐵 ⟶ 𝐾 )
160 159 154 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝐷 ‘ 𝑑 ) ∈ 𝐾 )
161 27 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 )
162 30 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝐸 : 𝐵 ⟶ 𝐾 )
163 162 154 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝐸 ‘ 𝑑 ) ∈ 𝐾 )
164 157 161 163 123 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ∈ 𝐾 )
165 3 7 34 157 158 160 164 ringsubdi ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑐 · ( ( 𝐷 ‘ 𝑑 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ) = ( ( 𝑐 · ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( 𝑐 · ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ) )
166 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
167 166 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
168 15 167 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
169 168 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
170 166 3 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
171 166 7 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
172 170 171 cmn12 ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ CMnd ∧ ( 𝑐 ∈ 𝐾 ∧ ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 ∧ ( 𝐸 ‘ 𝑑 ) ∈ 𝐾 ) ) → ( 𝑐 · ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑐 · ( 𝐸 ‘ 𝑑 ) ) ) )
173 169 158 161 163 172 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑐 · ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑐 · ( 𝐸 ‘ 𝑑 ) ) ) )
174 173 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑐 · ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( 𝑐 · ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑑 ) ) ) ) = ( ( 𝑐 · ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑐 · ( 𝐸 ‘ 𝑑 ) ) ) ) )
175 156 165 174 3eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) = ( ( 𝑐 · ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑐 · ( 𝐸 ‘ 𝑑 ) ) ) ) )
176 175 3adant3 ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) = ( ( 𝑐 · ( 𝐷 ‘ 𝑑 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝑐 · ( 𝐸 ‘ 𝑑 ) ) ) ) )
177 150 153 176 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) )
178 177 3expia ⊢ ( ( 𝜑 ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) ) )
179 178 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) → ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) ) )
180 179 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐾 ) ) → ∀ 𝑑 ∈ 𝐵 ∀ 𝑒 ∈ 𝑁 ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) ) )
181 180 ralrimivva ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐾 ∀ 𝑑 ∈ 𝐵 ∀ 𝑒 ∈ 𝑁 ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑏 ) = ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑑 ) ) ) )
182 eqidd ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) = ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) )
183 fveq2 ⊢ ( 𝑎 = ( 1r ‘ 𝐴 ) → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) )
184 fveq2 ⊢ ( 𝑎 = ( 1r ‘ 𝐴 ) → ( 𝐸 ‘ 𝑎 ) = ( 𝐸 ‘ ( 1r ‘ 𝐴 ) ) )
185 184 oveq2d ⊢ ( 𝑎 = ( 1r ‘ 𝐴 ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ ( 1r ‘ 𝐴 ) ) ) )
186 183 185 oveq12d ⊢ ( 𝑎 = ( 1r ‘ 𝐴 ) → ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ ( 1r ‘ 𝐴 ) ) ) ) )
187 14 1 24 5 mdet1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝐸 ‘ ( 1r ‘ 𝐴 ) ) = 1 )
188 15 8 187 syl2anc ⊢ ( 𝜑 → ( 𝐸 ‘ ( 1r ‘ 𝐴 ) ) = 1 )
189 188 oveq2d ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ ( 1r ‘ 𝐴 ) ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · 1 ) )
190 3 7 5 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · 1 ) = ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) )
191 9 27 190 syl2anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · 1 ) = ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) )
192 189 191 eqtrd ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ ( 1r ‘ 𝐴 ) ) ) = ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) )
193 192 oveq2d ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ ( 1r ‘ 𝐴 ) ) ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝑅 ) ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ) )
194 3 4 34 grpsubid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝑅 ) ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ) = 0 )
195 18 27 194 syl2anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝑅 ) ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ) = 0 )
196 193 195 eqtrd ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ ( 1r ‘ 𝐴 ) ) ) ) = 0 )
197 186 196 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑎 = ( 1r ‘ 𝐴 ) ) → ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) = 0 )
198 4 fvexi ⊢ 0 ∈ V
199 198 a1i ⊢ ( 𝜑 → 0 ∈ V )
200 182 197 26 199 fvmptd ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ ( 1r ‘ 𝐴 ) ) = 0 )
201 eqid ⊢ { 𝑏 ∣ ∀ 𝑐 ∈ 𝐵 ∀ 𝑑 ∈ ( 𝑁 ↑m 𝑁 ) ( ∀ 𝑒 ∈ 𝑏 ( 𝑐 ‘ 𝑒 ) = if ( 𝑒 ∈ 𝑑 , 1 , 0 ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) = 0 ) } = { 𝑏 ∣ ∀ 𝑐 ∈ 𝐵 ∀ 𝑑 ∈ ( 𝑁 ↑m 𝑁 ) ( ∀ 𝑒 ∈ 𝑏 ( 𝑐 ‘ 𝑒 ) = if ( 𝑒 ∈ 𝑑 , 1 , 0 ) → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝑐 ) = 0 ) }
202 1 2 3 4 5 6 7 8 9 37 75 137 181 200 201 mdetunilem9 ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) = ( 𝐵 × { 0 } ) )
203 202 fveq1d ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝐹 ) = ( ( 𝐵 × { 0 } ) ‘ 𝐹 ) )
204 fveq2 ⊢ ( 𝑎 = 𝐹 → ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝐹 ) )
205 fveq2 ⊢ ( 𝑎 = 𝐹 → ( 𝐸 ‘ 𝑎 ) = ( 𝐸 ‘ 𝐹 ) )
206 205 oveq2d ⊢ ( 𝑎 = 𝐹 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) )
207 204 206 oveq12d ⊢ ( 𝑎 = 𝐹 → ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) = ( ( 𝐷 ‘ 𝐹 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ) )
208 207 adantl ⊢ ( ( 𝜑 ∧ 𝑎 = 𝐹 ) → ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) = ( ( 𝐷 ‘ 𝐹 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ) )
209 ovexd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ) ∈ V )
210 182 208 16 209 fvmptd ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐵 ↦ ( ( 𝐷 ‘ 𝑎 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝑎 ) ) ) ) ‘ 𝐹 ) = ( ( 𝐷 ‘ 𝐹 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ) )
211 198 fvconst2 ⊢ ( 𝐹 ∈ 𝐵 → ( ( 𝐵 × { 0 } ) ‘ 𝐹 ) = 0 )
212 16 211 syl ⊢ ( 𝜑 → ( ( 𝐵 × { 0 } ) ‘ 𝐹 ) = 0 )
213 203 210 212 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ) = 0 )
214 10 16 ffvelrnd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ 𝐾 )
215 30 16 ffvelrnd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐹 ) ∈ 𝐾 )
216 3 7 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) ∈ 𝐾 ∧ ( 𝐸 ‘ 𝐹 ) ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ∈ 𝐾 )
217 9 27 215 216 syl3anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ∈ 𝐾 )
218 3 4 34 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐷 ‘ 𝐹 ) ∈ 𝐾 ∧ ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ∈ 𝐾 ) → ( ( ( 𝐷 ‘ 𝐹 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ) = 0 ↔ ( 𝐷 ‘ 𝐹 ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ) )
219 18 214 217 218 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐷 ‘ 𝐹 ) ( -g ‘ 𝑅 ) ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ) = 0 ↔ ( 𝐷 ‘ 𝐹 ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ) )
220 213 219 mpbid ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) )