Metamath Proof Explorer

Theorem mdetunilem4

Description: Lemma for mdetuni . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses mdetuni.a ⊢ A = N Mat R
mdetuni.b ⊢ B = Base A
mdetuni.k ⊢ K = Base R
mdetuni.0g ⊢ 0 ˙ = 0 R
mdetuni.1r ⊢ 1 ˙ = 1 R
mdetuni.pg ⊢ + ˙ = + R
mdetuni.tg ⊢ · ˙ = ⋅ R
mdetuni.n ⊢ φ → N ∈ Fin
mdetuni.r ⊢ φ → R ∈ Ring
mdetuni.ff ⊢ φ → D : B ⟶ K
mdetuni.al ⊢ φ → ∀ x ∈ B ∀ y ∈ N ∀ z ∈ N y ≠ z ∧ ∀ w ∈ N y x w = z x w → D ⁡ x = 0 ˙
mdetuni.li ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ w ∈ N x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = D ⁡ y + ˙ D ⁡ z
mdetuni.sc ⊢ φ → ∀ x ∈ B ∀ y ∈ K ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z
Assertion mdetunilem4 ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = F · ˙ D ⁡ G

Proof

Step Hyp Ref Expression
1 mdetuni.a ⊢ A = N Mat R
2 mdetuni.b ⊢ B = Base A
3 mdetuni.k ⊢ K = Base R
4 mdetuni.0g ⊢ 0 ˙ = 0 R
5 mdetuni.1r ⊢ 1 ˙ = 1 R
6 mdetuni.pg ⊢ + ˙ = + R
7 mdetuni.tg ⊢ · ˙ = ⋅ R
8 mdetuni.n ⊢ φ → N ∈ Fin
9 mdetuni.r ⊢ φ → R ∈ Ring
10 mdetuni.ff ⊢ φ → D : B ⟶ K
11 mdetuni.al ⊢ φ → ∀ x ∈ B ∀ y ∈ N ∀ z ∈ N y ≠ z ∧ ∀ w ∈ N y x w = z x w → D ⁡ x = 0 ˙
12 mdetuni.li ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ w ∈ N x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = D ⁡ y + ˙ D ⁡ z
13 mdetuni.sc ⊢ φ → ∀ x ∈ B ∀ y ∈ K ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z
14 simp32 ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → E ↾ H × N = H × N × F · ˙ f G ↾ H × N
15 simp33 ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → E ↾ N ∖ H × N = G ↾ N ∖ H × N
16 simp1 ⊢ H ∈ N ∧ E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → H ∈ N
17 simp23 ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N → G ∈ B
18 simp3 ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N → H ∈ N
19 simp21 ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N → E ∈ B
20 simp22 ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N → F ∈ K
21 13 3ad2ant1 ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N → ∀ x ∈ B ∀ y ∈ K ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z
22 reseq1 ⊢ x = E → x ↾ w × N = E ↾ w × N
23 22 eqeq1d ⊢ x = E → x ↾ w × N = w × N × y · ˙ f z ↾ w × N ↔ E ↾ w × N = w × N × y · ˙ f z ↾ w × N
24 reseq1 ⊢ x = E → x ↾ N ∖ w × N = E ↾ N ∖ w × N
25 24 eqeq1d ⊢ x = E → x ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ E ↾ N ∖ w × N = z ↾ N ∖ w × N
26 23 25 anbi12d ⊢ x = E → x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ E ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N
27 fveqeq2 ⊢ x = E → D ⁡ x = y · ˙ D ⁡ z ↔ D ⁡ E = y · ˙ D ⁡ z
28 26 27 imbi12d ⊢ x = E → x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z ↔ E ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = y · ˙ D ⁡ z
29 28 2ralbidv ⊢ x = E → ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z ↔ ∀ z ∈ B ∀ w ∈ N E ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = y · ˙ D ⁡ z
30 sneq ⊢ y = F → y = F
31 30 xpeq2d ⊢ y = F → w × N × y = w × N × F
32 31 oveq1d ⊢ y = F → w × N × y · ˙ f z ↾ w × N = w × N × F · ˙ f z ↾ w × N
33 32 eqeq2d ⊢ y = F → E ↾ w × N = w × N × y · ˙ f z ↾ w × N ↔ E ↾ w × N = w × N × F · ˙ f z ↾ w × N
34 33 anbi1d ⊢ y = F → E ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ E ↾ w × N = w × N × F · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N
35 oveq1 ⊢ y = F → y · ˙ D ⁡ z = F · ˙ D ⁡ z
36 35 eqeq2d ⊢ y = F → D ⁡ E = y · ˙ D ⁡ z ↔ D ⁡ E = F · ˙ D ⁡ z
37 34 36 imbi12d ⊢ y = F → E ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = y · ˙ D ⁡ z ↔ E ↾ w × N = w × N × F · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = F · ˙ D ⁡ z
38 37 2ralbidv ⊢ y = F → ∀ z ∈ B ∀ w ∈ N E ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = y · ˙ D ⁡ z ↔ ∀ z ∈ B ∀ w ∈ N E ↾ w × N = w × N × F · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = F · ˙ D ⁡ z
39 29 38 rspc2va ⊢ E ∈ B ∧ F ∈ K ∧ ∀ x ∈ B ∀ y ∈ K ∀ z ∈ B ∀ w ∈ N x ↾ w × N = w × N × y · ˙ f z ↾ w × N ∧ x ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ x = y · ˙ D ⁡ z → ∀ z ∈ B ∀ w ∈ N E ↾ w × N = w × N × F · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = F · ˙ D ⁡ z
40 19 20 21 39 syl21anc ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N → ∀ z ∈ B ∀ w ∈ N E ↾ w × N = w × N × F · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = F · ˙ D ⁡ z
41 reseq1 ⊢ z = G → z ↾ w × N = G ↾ w × N
42 41 oveq2d ⊢ z = G → w × N × F · ˙ f z ↾ w × N = w × N × F · ˙ f G ↾ w × N
43 42 eqeq2d ⊢ z = G → E ↾ w × N = w × N × F · ˙ f z ↾ w × N ↔ E ↾ w × N = w × N × F · ˙ f G ↾ w × N
44 reseq1 ⊢ z = G → z ↾ N ∖ w × N = G ↾ N ∖ w × N
45 44 eqeq2d ⊢ z = G → E ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ E ↾ N ∖ w × N = G ↾ N ∖ w × N
46 43 45 anbi12d ⊢ z = G → E ↾ w × N = w × N × F · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ E ↾ w × N = w × N × F · ˙ f G ↾ w × N ∧ E ↾ N ∖ w × N = G ↾ N ∖ w × N
47 fveq2 ⊢ z = G → D ⁡ z = D ⁡ G
48 47 oveq2d ⊢ z = G → F · ˙ D ⁡ z = F · ˙ D ⁡ G
49 48 eqeq2d ⊢ z = G → D ⁡ E = F · ˙ D ⁡ z ↔ D ⁡ E = F · ˙ D ⁡ G
50 46 49 imbi12d ⊢ z = G → E ↾ w × N = w × N × F · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = F · ˙ D ⁡ z ↔ E ↾ w × N = w × N × F · ˙ f G ↾ w × N ∧ E ↾ N ∖ w × N = G ↾ N ∖ w × N → D ⁡ E = F · ˙ D ⁡ G
51 sneq ⊢ w = H → w = H
52 51 xpeq1d ⊢ w = H → w × N = H × N
53 52 reseq2d ⊢ w = H → E ↾ w × N = E ↾ H × N
54 52 xpeq1d ⊢ w = H → w × N × F = H × N × F
55 52 reseq2d ⊢ w = H → G ↾ w × N = G ↾ H × N
56 54 55 oveq12d ⊢ w = H → w × N × F · ˙ f G ↾ w × N = H × N × F · ˙ f G ↾ H × N
57 53 56 eqeq12d ⊢ w = H → E ↾ w × N = w × N × F · ˙ f G ↾ w × N ↔ E ↾ H × N = H × N × F · ˙ f G ↾ H × N
58 51 difeq2d ⊢ w = H → N ∖ w = N ∖ H
59 58 xpeq1d ⊢ w = H → N ∖ w × N = N ∖ H × N
60 59 reseq2d ⊢ w = H → E ↾ N ∖ w × N = E ↾ N ∖ H × N
61 59 reseq2d ⊢ w = H → G ↾ N ∖ w × N = G ↾ N ∖ H × N
62 60 61 eqeq12d ⊢ w = H → E ↾ N ∖ w × N = G ↾ N ∖ w × N ↔ E ↾ N ∖ H × N = G ↾ N ∖ H × N
63 57 62 anbi12d ⊢ w = H → E ↾ w × N = w × N × F · ˙ f G ↾ w × N ∧ E ↾ N ∖ w × N = G ↾ N ∖ w × N ↔ E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N
64 63 imbi1d ⊢ w = H → E ↾ w × N = w × N × F · ˙ f G ↾ w × N ∧ E ↾ N ∖ w × N = G ↾ N ∖ w × N → D ⁡ E = F · ˙ D ⁡ G ↔ E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = F · ˙ D ⁡ G
65 50 64 rspc2va ⊢ G ∈ B ∧ H ∈ N ∧ ∀ z ∈ B ∀ w ∈ N E ↾ w × N = w × N × F · ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = F · ˙ D ⁡ z → E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = F · ˙ D ⁡ G
66 17 18 40 65 syl21anc ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N → E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = F · ˙ D ⁡ G
67 16 66 syl3an3 ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = F · ˙ D ⁡ G
68 14 15 67 mp2and ⊢ φ ∧ E ∈ B ∧ F ∈ K ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = H × N × F · ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = F · ˙ D ⁡ G