Metamath Proof Explorer

Theorem mdetunilem2

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 · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
mdetunilem2.ph ⊢ ( 𝜓 → 𝜑 )
mdetunilem2.eg ⊢ ( 𝜓 → ( 𝐸 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐸 ≠ 𝐺 ) )
mdetunilem2.f ⊢ ( ( 𝜓 ∧ 𝑏 ∈ 𝑁 ) → 𝐹 ∈ 𝐾 )
mdetunilem2.h ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐻 ∈ 𝐾 )
Assertion mdetunilem2 ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) ) = 0 )

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 mdetunilem2.ph ⊢ ( 𝜓 → 𝜑 )
15 mdetunilem2.eg ⊢ ( 𝜓 → ( 𝐸 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐸 ≠ 𝐺 ) )
16 mdetunilem2.f ⊢ ( ( 𝜓 ∧ 𝑏 ∈ 𝑁 ) → 𝐹 ∈ 𝐾 )
17 mdetunilem2.h ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐻 ∈ 𝐾 )
18 14 8 syl ⊢ ( 𝜓 → 𝑁 ∈ Fin )
19 14 9 syl ⊢ ( 𝜓 → 𝑅 ∈ Ring )
20 16 3adant2 ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝐹 ∈ 𝐾 )
21 20 17 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ∈ 𝐾 )
22 20 21 ifcld ⊢ ( ( 𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ∈ 𝐾 )
23 1 3 2 18 19 22 matbas2d ⊢ ( 𝜓 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) ∈ 𝐵 )
24 eqidd ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) )
25 iftrue ⊢ ( 𝑎 = 𝐸 → if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) = 𝐹 )
26 csbeq1a ⊢ ( 𝑏 = 𝑤 → 𝐹 = ⦋ 𝑤 / 𝑏 ⦌ 𝐹 )
27 25 26 sylan9eq ⊢ ( ( 𝑎 = 𝐸 ∧ 𝑏 = 𝑤 ) → if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) = ⦋ 𝑤 / 𝑏 ⦌ 𝐹 )
28 27 adantl ⊢ ( ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑎 = 𝐸 ∧ 𝑏 = 𝑤 ) ) → if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) = ⦋ 𝑤 / 𝑏 ⦌ 𝐹 )
29 eqidd ⊢ ( ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑎 = 𝐸 ) → 𝑁 = 𝑁 )
30 15 simp1d ⊢ ( 𝜓 → 𝐸 ∈ 𝑁 )
31 30 adantr ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → 𝐸 ∈ 𝑁 )
32 simpr ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → 𝑤 ∈ 𝑁 )
33 nfv ⊢ Ⅎ 𝑏 ( 𝜓 ∧ 𝑤 ∈ 𝑁 )
34 nfcsb1v ⊢ Ⅎ 𝑏 ⦋ 𝑤 / 𝑏 ⦌ 𝐹
35 34 nfel1 ⊢ Ⅎ 𝑏 ⦋ 𝑤 / 𝑏 ⦌ 𝐹 ∈ 𝐾
36 33 35 nfim ⊢ Ⅎ 𝑏 ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → ⦋ 𝑤 / 𝑏 ⦌ 𝐹 ∈ 𝐾 )
37 eleq1w ⊢ ( 𝑏 = 𝑤 → ( 𝑏 ∈ 𝑁 ↔ 𝑤 ∈ 𝑁 ) )
38 37 anbi2d ⊢ ( 𝑏 = 𝑤 → ( ( 𝜓 ∧ 𝑏 ∈ 𝑁 ) ↔ ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ) )
39 26 eleq1d ⊢ ( 𝑏 = 𝑤 → ( 𝐹 ∈ 𝐾 ↔ ⦋ 𝑤 / 𝑏 ⦌ 𝐹 ∈ 𝐾 ) )
40 38 39 imbi12d ⊢ ( 𝑏 = 𝑤 → ( ( ( 𝜓 ∧ 𝑏 ∈ 𝑁 ) → 𝐹 ∈ 𝐾 ) ↔ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → ⦋ 𝑤 / 𝑏 ⦌ 𝐹 ∈ 𝐾 ) ) )
41 36 40 16 chvarfv ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → ⦋ 𝑤 / 𝑏 ⦌ 𝐹 ∈ 𝐾 )
42 nfv ⊢ Ⅎ 𝑎 ( 𝜓 ∧ 𝑤 ∈ 𝑁 )
43 nfcv ⊢ Ⅎ 𝑏 𝐸
44 nfcv ⊢ Ⅎ 𝑎 𝑤
45 nfcv ⊢ Ⅎ 𝑎 ⦋ 𝑤 / 𝑏 ⦌ 𝐹
46 24 28 29 31 32 41 42 33 43 44 45 34 ovmpodxf ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → ( 𝐸 ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) 𝑤 ) = ⦋ 𝑤 / 𝑏 ⦌ 𝐹 )
47 15 simp3d ⊢ ( 𝜓 → 𝐸 ≠ 𝐺 )
48 47 adantr ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → 𝐸 ≠ 𝐺 )
49 neeq2 ⊢ ( 𝑎 = 𝐺 → ( 𝐸 ≠ 𝑎 ↔ 𝐸 ≠ 𝐺 ) )
50 48 49 syl5ibrcom ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → ( 𝑎 = 𝐺 → 𝐸 ≠ 𝑎 ) )
51 50 imp ⊢ ( ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑎 = 𝐺 ) → 𝐸 ≠ 𝑎 )
52 51 necomd ⊢ ( ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑎 = 𝐺 ) → 𝑎 ≠ 𝐸 )
53 52 neneqd ⊢ ( ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑎 = 𝐺 ) → ¬ 𝑎 = 𝐸 )
54 53 adantrr ⊢ ( ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑎 = 𝐺 ∧ 𝑏 = 𝑤 ) ) → ¬ 𝑎 = 𝐸 )
55 54 iffalsed ⊢ ( ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑎 = 𝐺 ∧ 𝑏 = 𝑤 ) ) → if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) = if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) )
56 iftrue ⊢ ( 𝑎 = 𝐺 → if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) = 𝐹 )
57 56 26 sylan9eq ⊢ ( ( 𝑎 = 𝐺 ∧ 𝑏 = 𝑤 ) → if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) = ⦋ 𝑤 / 𝑏 ⦌ 𝐹 )
58 57 adantl ⊢ ( ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑎 = 𝐺 ∧ 𝑏 = 𝑤 ) ) → if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) = ⦋ 𝑤 / 𝑏 ⦌ 𝐹 )
59 55 58 eqtrd ⊢ ( ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑎 = 𝐺 ∧ 𝑏 = 𝑤 ) ) → if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) = ⦋ 𝑤 / 𝑏 ⦌ 𝐹 )
60 eqidd ⊢ ( ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑎 = 𝐺 ) → 𝑁 = 𝑁 )
61 15 simp2d ⊢ ( 𝜓 → 𝐺 ∈ 𝑁 )
62 61 adantr ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → 𝐺 ∈ 𝑁 )
63 nfcv ⊢ Ⅎ 𝑏 𝐺
64 24 59 60 62 32 41 42 33 63 44 45 34 ovmpodxf ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → ( 𝐺 ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) 𝑤 ) = ⦋ 𝑤 / 𝑏 ⦌ 𝐹 )
65 46 64 eqtr4d ⊢ ( ( 𝜓 ∧ 𝑤 ∈ 𝑁 ) → ( 𝐸 ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) 𝑤 ) = ( 𝐺 ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) 𝑤 ) )
66 65 ralrimiva ⊢ ( 𝜓 → ∀ 𝑤 ∈ 𝑁 ( 𝐸 ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) 𝑤 ) = ( 𝐺 ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) 𝑤 ) )
67 1 2 3 4 5 6 7 8 9 10 11 12 13 mdetunilem1 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐸 ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) 𝑤 ) = ( 𝐺 ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) 𝑤 ) ) ∧ ( 𝐸 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐸 ≠ 𝐺 ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) ) = 0 )
68 14 23 66 15 67 syl31anc ⊢ ( 𝜓 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐸 , 𝐹 , if ( 𝑎 = 𝐺 , 𝐹 , 𝐻 ) ) ) ) = 0 )