Theorem mdetunilem1 20418

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

Hypotheses

Ref	Expression
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	⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))
mdetuni.sc	⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))

Assertion

Ref	Expression
mdetunilem1	⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → (𝐷‘𝐸) = 0 )

Distinct variable groups:   𝜑,𝑥,𝑦,𝑧,𝑤   𝑥,𝐵,𝑦,𝑧,𝑤   𝑥,𝐾,𝑦,𝑧,𝑤   𝑥,𝑁,𝑦,𝑧,𝑤   𝑥,𝐷,𝑦,𝑧,𝑤   𝑥, · ,𝑦,𝑧,𝑤   𝑥, + ,𝑦,𝑧,𝑤   𝑥, 0 ,𝑦,𝑧,𝑤   𝑥, 1 ,𝑦,𝑧,𝑤   𝑥,𝑅,𝑦,𝑧,𝑤   𝑥,𝐴,𝑦,𝑧,𝑤   𝑥,𝐸,𝑦,𝑧,𝑤   𝑥,𝐹,𝑦,𝑧,𝑤   𝑥,𝐺,𝑦,𝑧,𝑤

Proof of Theorem mdetunilem1

Step	Hyp	Ref	Expression
1		simpr3 1069	. 2 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → 𝐹 ≠ 𝐺)
2		simpl3 1066	. 2 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤))
3		neeq2 2857	. . . . 5 ⊢ (𝑧 = 𝐺 → (𝐹 ≠ 𝑧 ↔ 𝐹 ≠ 𝐺))
4		oveq1 6657	. . . . . . 7 ⊢ (𝑧 = 𝐺 → (𝑧𝐸𝑤) = (𝐺𝐸𝑤))
5	4	eqeq2d 2632	. . . . . 6 ⊢ (𝑧 = 𝐺 → ((𝐹𝐸𝑤) = (𝑧𝐸𝑤) ↔ (𝐹𝐸𝑤) = (𝐺𝐸𝑤)))
6	5	ralbidv 2986	. . . . 5 ⊢ (𝑧 = 𝐺 → (∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝑧𝐸𝑤) ↔ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)))
7	3, 6	anbi12d 747	. . . 4 ⊢ (𝑧 = 𝐺 → ((𝐹 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝑧𝐸𝑤)) ↔ (𝐹 ≠ 𝐺 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤))))
8	7	imbi1d 331	. . 3 ⊢ (𝑧 = 𝐺 → (((𝐹 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝑧𝐸𝑤)) → (𝐷‘𝐸) = 0 ) ↔ ((𝐹 ≠ 𝐺 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) → (𝐷‘𝐸) = 0 )))
9		simpl2 1065	. . . 4 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → 𝐸 ∈ 𝐵)
10		simpr1 1067	. . . 4 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → 𝐹 ∈ 𝑁)
11		simpl1 1064	. . . . 5 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → 𝜑)
12		mdetuni.al	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))
13	11, 12	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))
14		oveq 6656	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → (𝑦𝑥𝑤) = (𝑦𝐸𝑤))
15		oveq 6656	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → (𝑧𝑥𝑤) = (𝑧𝐸𝑤))
16	14, 15	eqeq12d 2637	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → ((𝑦𝑥𝑤) = (𝑧𝑥𝑤) ↔ (𝑦𝐸𝑤) = (𝑧𝐸𝑤)))
17	16	ralbidv 2986	. . . . . . . 8 ⊢ (𝑥 = 𝐸 → (∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤) ↔ ∀𝑤 ∈ 𝑁 (𝑦𝐸𝑤) = (𝑧𝐸𝑤)))
18	17	anbi2d 740	. . . . . . 7 ⊢ (𝑥 = 𝐸 → ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) ↔ (𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝐸𝑤) = (𝑧𝐸𝑤))))
19		fveq2 6191	. . . . . . . 8 ⊢ (𝑥 = 𝐸 → (𝐷‘𝑥) = (𝐷‘𝐸))
20	19	eqeq1d 2624	. . . . . . 7 ⊢ (𝑥 = 𝐸 → ((𝐷‘𝑥) = 0 ↔ (𝐷‘𝐸) = 0 ))
21	18, 20	imbi12d 334	. . . . . 6 ⊢ (𝑥 = 𝐸 → (((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ) ↔ ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝐸𝑤) = (𝑧𝐸𝑤)) → (𝐷‘𝐸) = 0 )))
22	21	ralbidv 2986	. . . . 5 ⊢ (𝑥 = 𝐸 → (∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ) ↔ ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝐸𝑤) = (𝑧𝐸𝑤)) → (𝐷‘𝐸) = 0 )))
23		neeq1 2856	. . . . . . . 8 ⊢ (𝑦 = 𝐹 → (𝑦 ≠ 𝑧 ↔ 𝐹 ≠ 𝑧))
24		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → (𝑦𝐸𝑤) = (𝐹𝐸𝑤))
25	24	eqeq1d 2624	. . . . . . . . 9 ⊢ (𝑦 = 𝐹 → ((𝑦𝐸𝑤) = (𝑧𝐸𝑤) ↔ (𝐹𝐸𝑤) = (𝑧𝐸𝑤)))
26	25	ralbidv 2986	. . . . . . . 8 ⊢ (𝑦 = 𝐹 → (∀𝑤 ∈ 𝑁 (𝑦𝐸𝑤) = (𝑧𝐸𝑤) ↔ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝑧𝐸𝑤)))
27	23, 26	anbi12d 747	. . . . . . 7 ⊢ (𝑦 = 𝐹 → ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝐸𝑤) = (𝑧𝐸𝑤)) ↔ (𝐹 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝑧𝐸𝑤))))
28	27	imbi1d 331	. . . . . 6 ⊢ (𝑦 = 𝐹 → (((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝐸𝑤) = (𝑧𝐸𝑤)) → (𝐷‘𝐸) = 0 ) ↔ ((𝐹 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝑧𝐸𝑤)) → (𝐷‘𝐸) = 0 )))
29	28	ralbidv 2986	. . . . 5 ⊢ (𝑦 = 𝐹 → (∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝐸𝑤) = (𝑧𝐸𝑤)) → (𝐷‘𝐸) = 0 ) ↔ ∀𝑧 ∈ 𝑁 ((𝐹 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝑧𝐸𝑤)) → (𝐷‘𝐸) = 0 )))
30	22, 29	rspc2va 3323	. . . 4 ⊢ (((𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝑁) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) → ∀𝑧 ∈ 𝑁 ((𝐹 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝑧𝐸𝑤)) → (𝐷‘𝐸) = 0 ))
31	9, 10, 13, 30	syl21anc 1325	. . 3 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → ∀𝑧 ∈ 𝑁 ((𝐹 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝑧𝐸𝑤)) → (𝐷‘𝐸) = 0 ))
32		simpr2 1068	. . 3 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → 𝐺 ∈ 𝑁)
33	8, 31, 32	rspcdva 3316	. 2 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → ((𝐹 ≠ 𝐺 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) → (𝐷‘𝐸) = 0 ))
34	1, 2, 33	mp2and 715	1 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → (𝐷‘𝐸) = 0 )

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912   ∖ cdif 3571  {csn 4177   × cxp 5112   ↾ cres 5116  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650   ∘_𝑓 cof 6895  Fincfn 7955  Basecbs 15857  +_gcplusg 15941  ._rcmulr 15942  0_gc0g 16100  1_rcur 18501  Ringcrg 18547   Mat cmat 20213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  mdetunilem2  20419  mdetuni0  20427