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

Metamath Proof Explorer

Theorem mdetunilem1

Description: Lemma for mdetuni . (Contributed by SO, 14-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 mdetunilem1 ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → ( 𝐷 ‘ 𝐸 ) = 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 simpr3 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → 𝐹 ≠ 𝐺 )
15 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) )
16 neeq2 ⊢ ( 𝑧 = 𝐺 → ( 𝐹 ≠ 𝑧 ↔ 𝐹 ≠ 𝐺 ) )
17 oveq1 ⊢ ( 𝑧 = 𝐺 → ( 𝑧 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) )
18 17 eqeq2d ⊢ ( 𝑧 = 𝐺 → ( ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ↔ ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) )
19 18 ralbidv ⊢ ( 𝑧 = 𝐺 → ( ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ↔ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) )
20 16 19 anbi12d ⊢ ( 𝑧 = 𝐺 → ( ( 𝐹 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) ↔ ( 𝐹 ≠ 𝐺 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ) )
21 20 imbi1d ⊢ ( 𝑧 = 𝐺 → ( ( ( 𝐹 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) ↔ ( ( 𝐹 ≠ 𝐺 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) ) )
22 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → 𝐸 ∈ 𝐵 )
23 simpr1 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → 𝐹 ∈ 𝑁 )
24 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → 𝜑 )
25 24 11 syl ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) )
26 oveq ⊢ ( 𝑥 = 𝐸 → ( 𝑦 𝑥 𝑤 ) = ( 𝑦 𝐸 𝑤 ) )
27 oveq ⊢ ( 𝑥 = 𝐸 → ( 𝑧 𝑥 𝑤 ) = ( 𝑧 𝐸 𝑤 ) )
28 26 27 eqeq12d ⊢ ( 𝑥 = 𝐸 → ( ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ↔ ( 𝑦 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) )
29 28 ralbidv ⊢ ( 𝑥 = 𝐸 → ( ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ↔ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) )
30 29 anbi2d ⊢ ( 𝑥 = 𝐸 → ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) ↔ ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) ) )
31 fveqeq2 ⊢ ( 𝑥 = 𝐸 → ( ( 𝐷 ‘ 𝑥 ) = 0 ↔ ( 𝐷 ‘ 𝐸 ) = 0 ) )
32 30 31 imbi12d ⊢ ( 𝑥 = 𝐸 → ( ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) ↔ ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) ) )
33 32 ralbidv ⊢ ( 𝑥 = 𝐸 → ( ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) ) )
34 neeq1 ⊢ ( 𝑦 = 𝐹 → ( 𝑦 ≠ 𝑧 ↔ 𝐹 ≠ 𝑧 ) )
35 oveq1 ⊢ ( 𝑦 = 𝐹 → ( 𝑦 𝐸 𝑤 ) = ( 𝐹 𝐸 𝑤 ) )
36 35 eqeq1d ⊢ ( 𝑦 = 𝐹 → ( ( 𝑦 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ↔ ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) )
37 36 ralbidv ⊢ ( 𝑦 = 𝐹 → ( ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ↔ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) )
38 34 37 anbi12d ⊢ ( 𝑦 = 𝐹 → ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) ↔ ( 𝐹 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) ) )
39 38 imbi1d ⊢ ( 𝑦 = 𝐹 → ( ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) ↔ ( ( 𝐹 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) ) )
40 39 ralbidv ⊢ ( 𝑦 = 𝐹 → ( ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) ↔ ∀ 𝑧 ∈ 𝑁 ( ( 𝐹 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) ) )
41 33 40 rspc2va ⊢ ( ( ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) ) → ∀ 𝑧 ∈ 𝑁 ( ( 𝐹 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) )
42 22 23 25 41 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → ∀ 𝑧 ∈ 𝑁 ( ( 𝐹 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝑧 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) )
43 simpr2 ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → 𝐺 ∈ 𝑁 )
44 21 42 43 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → ( ( 𝐹 ≠ 𝐺 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 ) )
45 14 15 44 mp2and ⊢ ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝐹 𝐸 𝑤 ) = ( 𝐺 𝐸 𝑤 ) ) ∧ ( 𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺 ) ) → ( 𝐷 ‘ 𝐸 ) = 0 )