Metamath Proof Explorer

Theorem mdetunilem3

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 mdetunilem3 ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = D ⁡ 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 simp23 ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N
15 simp3l ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → E ↾ N ∖ H × N = F ↾ N ∖ H × N
16 simp3r ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → E ↾ N ∖ H × N = G ↾ N ∖ H × N
17 simprl ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N → G ∈ B
18 simprr ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N → H ∈ N
19 simpl2 ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N → E ∈ B
20 simpl3 ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N → F ∈ B
21 simpl1 ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N → φ
22 21 12 syl ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N → ∀ 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
23 reseq1 ⊢ x = E → x ↾ w × N = E ↾ w × N
24 23 eqeq1d ⊢ x = E → x ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ↔ E ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N
25 reseq1 ⊢ x = E → x ↾ N ∖ w × N = E ↾ N ∖ w × N
26 25 eqeq1d ⊢ x = E → x ↾ N ∖ w × N = y ↾ N ∖ w × N ↔ E ↾ N ∖ w × N = y ↾ N ∖ w × N
27 25 eqeq1d ⊢ x = E → x ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ E ↾ N ∖ w × N = z ↾ N ∖ w × N
28 24 26 27 3anbi123d ⊢ x = E → 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 ↔ E ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N
29 fveq2 ⊢ x = E → D ⁡ x = D ⁡ E
30 29 eqeq1d ⊢ x = E → D ⁡ x = D ⁡ y + ˙ D ⁡ z ↔ D ⁡ E = D ⁡ y + ˙ D ⁡ z
31 28 30 imbi12d ⊢ x = E → 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 ↔ E ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = D ⁡ y + ˙ D ⁡ z
32 31 2ralbidv ⊢ x = E → ∀ 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 ↔ ∀ z ∈ B ∀ w ∈ N E ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = D ⁡ y + ˙ D ⁡ z
33 reseq1 ⊢ y = F → y ↾ w × N = F ↾ w × N
34 33 oveq1d ⊢ y = F → y ↾ w × N + ˙ f z ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N
35 34 eqeq2d ⊢ y = F → E ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ↔ E ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N
36 reseq1 ⊢ y = F → y ↾ N ∖ w × N = F ↾ N ∖ w × N
37 36 eqeq2d ⊢ y = F → E ↾ N ∖ w × N = y ↾ N ∖ w × N ↔ E ↾ N ∖ w × N = F ↾ N ∖ w × N
38 35 37 3anbi12d ⊢ y = F → E ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ E ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N
39 fveq2 ⊢ y = F → D ⁡ y = D ⁡ F
40 39 oveq1d ⊢ y = F → D ⁡ y + ˙ D ⁡ z = D ⁡ F + ˙ D ⁡ z
41 40 eqeq2d ⊢ y = F → D ⁡ E = D ⁡ y + ˙ D ⁡ z ↔ D ⁡ E = D ⁡ F + ˙ D ⁡ z
42 38 41 imbi12d ⊢ y = F → E ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = D ⁡ y + ˙ D ⁡ z ↔ E ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = D ⁡ F + ˙ D ⁡ z
43 42 2ralbidv ⊢ y = F → ∀ z ∈ B ∀ w ∈ N E ↾ w × N = y ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = y ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = D ⁡ y + ˙ D ⁡ z ↔ ∀ z ∈ B ∀ w ∈ N E ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = D ⁡ F + ˙ D ⁡ z
44 32 43 rspc2va ⊢ E ∈ B ∧ F ∈ B ∧ ∀ 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 → ∀ z ∈ B ∀ w ∈ N E ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = D ⁡ F + ˙ D ⁡ z
45 19 20 22 44 syl21anc ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N → ∀ z ∈ B ∀ w ∈ N E ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = D ⁡ F + ˙ D ⁡ z
46 reseq1 ⊢ z = G → z ↾ w × N = G ↾ w × N
47 46 oveq2d ⊢ z = G → F ↾ w × N + ˙ f z ↾ w × N = F ↾ w × N + ˙ f G ↾ w × N
48 47 eqeq2d ⊢ z = G → E ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N ↔ E ↾ w × N = F ↾ w × N + ˙ f G ↾ w × N
49 reseq1 ⊢ z = G → z ↾ N ∖ w × N = G ↾ N ∖ w × N
50 49 eqeq2d ⊢ z = G → E ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ E ↾ N ∖ w × N = G ↾ N ∖ w × N
51 48 50 3anbi13d ⊢ z = G → E ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N ↔ E ↾ w × N = F ↾ w × N + ˙ f G ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = G ↾ N ∖ w × N
52 fveq2 ⊢ z = G → D ⁡ z = D ⁡ G
53 52 oveq2d ⊢ z = G → D ⁡ F + ˙ D ⁡ z = D ⁡ F + ˙ D ⁡ G
54 53 eqeq2d ⊢ z = G → D ⁡ E = D ⁡ F + ˙ D ⁡ z ↔ D ⁡ E = D ⁡ F + ˙ D ⁡ G
55 51 54 imbi12d ⊢ z = G → E ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = D ⁡ F + ˙ D ⁡ z ↔ E ↾ w × N = F ↾ w × N + ˙ f G ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = G ↾ N ∖ w × N → D ⁡ E = D ⁡ F + ˙ D ⁡ G
56 sneq ⊢ w = H → w = H
57 56 xpeq1d ⊢ w = H → w × N = H × N
58 57 reseq2d ⊢ w = H → E ↾ w × N = E ↾ H × N
59 57 reseq2d ⊢ w = H → F ↾ w × N = F ↾ H × N
60 57 reseq2d ⊢ w = H → G ↾ w × N = G ↾ H × N
61 59 60 oveq12d ⊢ w = H → F ↾ w × N + ˙ f G ↾ w × N = F ↾ H × N + ˙ f G ↾ H × N
62 58 61 eqeq12d ⊢ w = H → E ↾ w × N = F ↾ w × N + ˙ f G ↾ w × N ↔ E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N
63 56 difeq2d ⊢ w = H → N ∖ w = N ∖ H
64 63 xpeq1d ⊢ w = H → N ∖ w × N = N ∖ H × N
65 64 reseq2d ⊢ w = H → E ↾ N ∖ w × N = E ↾ N ∖ H × N
66 64 reseq2d ⊢ w = H → F ↾ N ∖ w × N = F ↾ N ∖ H × N
67 65 66 eqeq12d ⊢ w = H → E ↾ N ∖ w × N = F ↾ N ∖ w × N ↔ E ↾ N ∖ H × N = F ↾ N ∖ H × N
68 64 reseq2d ⊢ w = H → G ↾ N ∖ w × N = G ↾ N ∖ H × N
69 65 68 eqeq12d ⊢ w = H → E ↾ N ∖ w × N = G ↾ N ∖ w × N ↔ E ↾ N ∖ H × N = G ↾ N ∖ H × N
70 62 67 69 3anbi123d ⊢ w = H → E ↾ w × N = F ↾ w × N + ˙ f G ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = G ↾ N ∖ w × N ↔ E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N
71 70 imbi1d ⊢ w = H → E ↾ w × N = F ↾ w × N + ˙ f G ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = G ↾ N ∖ w × N → D ⁡ E = D ⁡ F + ˙ D ⁡ G ↔ E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = D ⁡ F + ˙ D ⁡ G
72 55 71 rspc2va ⊢ G ∈ B ∧ H ∈ N ∧ ∀ z ∈ B ∀ w ∈ N E ↾ w × N = F ↾ w × N + ˙ f z ↾ w × N ∧ E ↾ N ∖ w × N = F ↾ N ∖ w × N ∧ E ↾ N ∖ w × N = z ↾ N ∖ w × N → D ⁡ E = D ⁡ F + ˙ D ⁡ z → E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = D ⁡ F + ˙ D ⁡ G
73 17 18 45 72 syl21anc ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N → E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = D ⁡ F + ˙ D ⁡ G
74 73 3adantr3 ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N → E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = D ⁡ F + ˙ D ⁡ G
75 74 3adant3 ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = D ⁡ F + ˙ D ⁡ G
76 14 15 16 75 mp3and ⊢ φ ∧ E ∈ B ∧ F ∈ B ∧ G ∈ B ∧ H ∈ N ∧ E ↾ H × N = F ↾ H × N + ˙ f G ↾ H × N ∧ E ↾ N ∖ H × N = F ↾ N ∖ H × N ∧ E ↾ N ∖ H × N = G ↾ N ∖ H × N → D ⁡ E = D ⁡ F + ˙ D ⁡ G