Metamath Proof Explorer

Theorem mdetunilem3

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

Ref Expression
Hypotheses mdetuni.a ⊢A=NMatR
mdetuni.b ⊢B=BaseA
mdetuni.k ⊢K=BaseR
mdetuni.0g ⊢0˙=0R
mdetuni.1r ⊢1˙=1R
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∈Ny≠z∧∀w∈Nyxw=zxw→D⁡x=0˙
mdetuni.li ⊢φ→∀x∈B∀y∈B∀z∈B∀w∈Nx↾w×N=y↾w×N+˙fz↾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∈Nx↾w×N=w×N×y·˙fz↾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+˙fG↾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=NMatR
2 mdetuni.b ⊢B=BaseA
3 mdetuni.k ⊢K=BaseR
4 mdetuni.0g ⊢0˙=0R
5 mdetuni.1r ⊢1˙=1R
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∈Ny≠z∧∀w∈Nyxw=zxw→D⁡x=0˙
12 mdetuni.li ⊢φ→∀x∈B∀y∈B∀z∈B∀w∈Nx↾w×N=y↾w×N+˙fz↾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∈Nx↾w×N=w×N×y·˙fz↾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+˙fG↾H×N∧E↾N∖H×N=F↾N∖H×N∧E↾N∖H×N=G↾N∖H×N→E↾H×N=F↾H×N+˙fG↾H×N
15 simp3l ⊢φ∧E∈B∧F∈B∧G∈B∧H∈N∧E↾H×N=F↾H×N+˙fG↾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+˙fG↾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∈Nx↾w×N=y↾w×N+˙fz↾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+˙fz↾w×N↔E↾w×N=y↾w×N+˙fz↾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+˙fz↾w×N∧x↾N∖w×N=y↾N∖w×N∧x↾N∖w×N=z↾N∖w×N↔E↾w×N=y↾w×N+˙fz↾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+˙fz↾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+˙fz↾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∈Nx↾w×N=y↾w×N+˙fz↾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∈NE↾w×N=y↾w×N+˙fz↾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+˙fz↾w×N=F↾w×N+˙fz↾w×N
35 34 eqeq2d ⊢y=F→E↾w×N=y↾w×N+˙fz↾w×N↔E↾w×N=F↾w×N+˙fz↾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+˙fz↾w×N∧E↾N∖w×N=y↾N∖w×N∧E↾N∖w×N=z↾N∖w×N↔E↾w×N=F↾w×N+˙fz↾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+˙fz↾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+˙fz↾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∈NE↾w×N=y↾w×N+˙fz↾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∈NE↾w×N=F↾w×N+˙fz↾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∈Nx↾w×N=y↾w×N+˙fz↾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∈NE↾w×N=F↾w×N+˙fz↾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∈NE↾w×N=F↾w×N+˙fz↾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+˙fz↾w×N=F↾w×N+˙fG↾w×N
48 47 eqeq2d ⊢z=G→E↾w×N=F↾w×N+˙fz↾w×N↔E↾w×N=F↾w×N+˙fG↾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+˙fz↾w×N∧E↾N∖w×N=F↾N∖w×N∧E↾N∖w×N=z↾N∖w×N↔E↾w×N=F↾w×N+˙fG↾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+˙fz↾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+˙fG↾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+˙fG↾w×N=F↾H×N+˙fG↾H×N
62 58 61 eqeq12d ⊢w=H→E↾w×N=F↾w×N+˙fG↾w×N↔E↾H×N=F↾H×N+˙fG↾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+˙fG↾w×N∧E↾N∖w×N=F↾N∖w×N∧E↾N∖w×N=G↾N∖w×N↔E↾H×N=F↾H×N+˙fG↾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+˙fG↾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+˙fG↾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∈NE↾w×N=F↾w×N+˙fz↾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+˙fG↾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+˙fG↾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+˙fG↾H×N→E↾H×N=F↾H×N+˙fG↾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+˙fG↾H×N∧E↾N∖H×N=F↾N∖H×N∧E↾N∖H×N=G↾N∖H×N→E↾H×N=F↾H×N+˙fG↾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+˙fG↾H×N∧E↾N∖H×N=F↾N∖H×N∧E↾N∖H×N=G↾N∖H×N→D⁡E=D⁡F+˙D⁡G