Theorem cramerimplem1 22819

Description: Lemma 1 for cramerimp 22822: The determinant of the identity matrix with the ith column replaced by a (column) vector equals the ith component of the vector. (Contributed by AV, 15-Feb-2019.) (Revised by AV, 5-Jul-2022.)

Hypotheses

Ref	Expression
cramerimplem1.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
cramerimplem1.v	⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)
cramerimplem1.e	⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼)
cramerimplem1.d	⊢ 𝐷 = (𝑁 maDet 𝑅)

Assertion

Ref	Expression
cramerimplem1	⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐷‘𝐸) = (𝑍‘𝐼))

Proof of Theorem cramerimplem1

Step	Hyp	Ref	Expression
1		crngring 20326	. . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
2	1	anim2i 628	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
3	2	ancomd 466	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
4	3	3adant3 1148	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
5		simp3 1154	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝐼 ∈ 𝑁)
6	5	anim1i 626	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉))
7		cramerimplem1.v	. . . . . 6 ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)
8		cramerimplem1.a	. . . . . . 7 ⊢ 𝐴 = (𝑁 Mat 𝑅)
9	8	fveq2i 6884	. . . . . 6 ⊢ (1r‘𝐴) = (1r‘(𝑁 Mat 𝑅))
10		cramerimplem1.e	. . . . . 6 ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼)
11	7, 9, 10	1marepvmarrepid 22711	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉)) → (𝐼(𝐸(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼) = 𝐸)
12	4, 6, 11	syl2an2r 697	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐼(𝐸(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼) = 𝐸)
13	12	eqcomd 2767	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → 𝐸 = (𝐼(𝐸(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼))
14	13	fveq2d 6885	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐷‘𝐸) = (𝐷‘(𝐼(𝐸(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼)))
15		cramerimplem1.d	. . . . 5 ⊢ 𝐷 = (𝑁 maDet 𝑅)
16	15	a1i 11	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → 𝐷 = (𝑁 maDet 𝑅))
17	16	fveq1d 6883	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐷‘(𝐼(𝐸(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼)) = ((𝑁 maDet 𝑅)‘(𝐼(𝐸(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼)))
18		simpl2 1209	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → 𝑅 ∈ CRing)
19	5	anim1ci 627	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁))
20	8	eqcomi 2770	. . . . . . . 8 ⊢ (𝑁 Mat 𝑅) = 𝐴
21	20	fveq2i 6884	. . . . . . 7 ⊢ (Base‘(𝑁 Mat 𝑅)) = (Base‘𝐴)
22		eqid 2761	. . . . . . 7 ⊢ (1r‘𝐴) = (1r‘𝐴)
23	8, 21, 7, 22	ma1repvcl 22706	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁)) → (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ (Base‘(𝑁 Mat 𝑅)))
24	4, 19, 23	syl2an2r 697	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ (Base‘(𝑁 Mat 𝑅)))
25	10, 24	eqeltrid 2865	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → 𝐸 ∈ (Base‘(𝑁 Mat 𝑅)))
26	5	adantr 485	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → 𝐼 ∈ 𝑁)
27		elmapi 8845	. . . . . . . . 9 ⊢ (𝑍 ∈ ((Base‘𝑅) ↑m 𝑁) → 𝑍:𝑁⟶(Base‘𝑅))
28		ffvelcdm 7076	. . . . . . . . . 10 ⊢ ((𝑍:𝑁⟶(Base‘𝑅) ∧ 𝐼 ∈ 𝑁) → (𝑍‘𝐼) ∈ (Base‘𝑅))
29	28	ex 417	. . . . . . . . 9 ⊢ (𝑍:𝑁⟶(Base‘𝑅) → (𝐼 ∈ 𝑁 → (𝑍‘𝐼) ∈ (Base‘𝑅)))
30	27, 29	syl 18	. . . . . . . 8 ⊢ (𝑍 ∈ ((Base‘𝑅) ↑m 𝑁) → (𝐼 ∈ 𝑁 → (𝑍‘𝐼) ∈ (Base‘𝑅)))
31	30, 7	eleq2s 2879	. . . . . . 7 ⊢ (𝑍 ∈ 𝑉 → (𝐼 ∈ 𝑁 → (𝑍‘𝐼) ∈ (Base‘𝑅)))
32	31	com12 33	. . . . . 6 ⊢ (𝐼 ∈ 𝑁 → (𝑍 ∈ 𝑉 → (𝑍‘𝐼) ∈ (Base‘𝑅)))
33	32	3ad2ant3 1151	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → (𝑍 ∈ 𝑉 → (𝑍‘𝐼) ∈ (Base‘𝑅)))
34	33	imp 411	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝑍‘𝐼) ∈ (Base‘𝑅))
35		smadiadetr 22811	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐸 ∈ (Base‘(𝑁 Mat 𝑅))) ∧ (𝐼 ∈ 𝑁 ∧ (𝑍‘𝐼) ∈ (Base‘𝑅))) → ((𝑁 maDet 𝑅)‘(𝐼(𝐸(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼)) = ((𝑍‘𝐼)(.r‘𝑅)(((𝑁 ∖ {𝐼}) maDet 𝑅)‘(𝐼((𝑁 subMat 𝑅)‘𝐸)𝐼))))
36	18, 25, 26, 34, 35	syl22anc 851	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → ((𝑁 maDet 𝑅)‘(𝐼(𝐸(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼)) = ((𝑍‘𝐼)(.r‘𝑅)(((𝑁 ∖ {𝐼}) maDet 𝑅)‘(𝐼((𝑁 subMat 𝑅)‘𝐸)𝐼))))
37	17, 36	eqtrd 2796	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐷‘(𝐼(𝐸(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼)) = ((𝑍‘𝐼)(.r‘𝑅)(((𝑁 ∖ {𝐼}) maDet 𝑅)‘(𝐼((𝑁 subMat 𝑅)‘𝐸)𝐼))))
38	7, 9, 10	1marepvsma1 22719	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉)) → (𝐼((𝑁 subMat 𝑅)‘𝐸)𝐼) = (1r‘((𝑁 ∖ {𝐼}) Mat 𝑅)))
39	4, 6, 38	syl2an2r 697	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐼((𝑁 subMat 𝑅)‘𝐸)𝐼) = (1r‘((𝑁 ∖ {𝐼}) Mat 𝑅)))
40	39	fveq2d 6885	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (((𝑁 ∖ {𝐼}) maDet 𝑅)‘(𝐼((𝑁 subMat 𝑅)‘𝐸)𝐼)) = (((𝑁 ∖ {𝐼}) maDet 𝑅)‘(1r‘((𝑁 ∖ {𝐼}) Mat 𝑅))))
41	40	oveq2d 7426	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → ((𝑍‘𝐼)(.r‘𝑅)(((𝑁 ∖ {𝐼}) maDet 𝑅)‘(𝐼((𝑁 subMat 𝑅)‘𝐸)𝐼))) = ((𝑍‘𝐼)(.r‘𝑅)(((𝑁 ∖ {𝐼}) maDet 𝑅)‘(1r‘((𝑁 ∖ {𝐼}) Mat 𝑅)))))
42		diffi 9158	. . . . . . . 8 ⊢ (𝑁 ∈ Fin → (𝑁 ∖ {𝐼}) ∈ Fin)
43	42	anim1ci 627	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 ∈ CRing ∧ (𝑁 ∖ {𝐼}) ∈ Fin))
44	43	3adant3 1148	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → (𝑅 ∈ CRing ∧ (𝑁 ∖ {𝐼}) ∈ Fin))
45	44	adantr 485	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝑅 ∈ CRing ∧ (𝑁 ∖ {𝐼}) ∈ Fin))
46		eqid 2761	. . . . . 6 ⊢ ((𝑁 ∖ {𝐼}) maDet 𝑅) = ((𝑁 ∖ {𝐼}) maDet 𝑅)
47		eqid 2761	. . . . . 6 ⊢ ((𝑁 ∖ {𝐼}) Mat 𝑅) = ((𝑁 ∖ {𝐼}) Mat 𝑅)
48		eqid 2761	. . . . . 6 ⊢ (1r‘((𝑁 ∖ {𝐼}) Mat 𝑅)) = (1r‘((𝑁 ∖ {𝐼}) Mat 𝑅))
49		eqid 2761	. . . . . 6 ⊢ (1r‘𝑅) = (1r‘𝑅)
50	46, 47, 48, 49	mdet1 22737	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ (𝑁 ∖ {𝐼}) ∈ Fin) → (((𝑁 ∖ {𝐼}) maDet 𝑅)‘(1r‘((𝑁 ∖ {𝐼}) Mat 𝑅))) = (1r‘𝑅))
51	45, 50	syl 18	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (((𝑁 ∖ {𝐼}) maDet 𝑅)‘(1r‘((𝑁 ∖ {𝐼}) Mat 𝑅))) = (1r‘𝑅))
52	51	oveq2d 7426	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → ((𝑍‘𝐼)(.r‘𝑅)(((𝑁 ∖ {𝐼}) maDet 𝑅)‘(1r‘((𝑁 ∖ {𝐼}) Mat 𝑅)))) = ((𝑍‘𝐼)(.r‘𝑅)(1r‘𝑅)))
53	1	3ad2ant2 1150	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ Ring)
54		eqid 2761	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅)
55		eqid 2761	. . . . 5 ⊢ (.r‘𝑅) = (.r‘𝑅)
56	54, 55, 49	ringridm 20352	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (𝑍‘𝐼) ∈ (Base‘𝑅)) → ((𝑍‘𝐼)(.r‘𝑅)(1r‘𝑅)) = (𝑍‘𝐼))
57	53, 34, 56	syl2an2r 697	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → ((𝑍‘𝐼)(.r‘𝑅)(1r‘𝑅)) = (𝑍‘𝐼))
58	41, 52, 57	3eqtrd 2800	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → ((𝑍‘𝐼)(.r‘𝑅)(((𝑁 ∖ {𝐼}) maDet 𝑅)‘(𝐼((𝑁 subMat 𝑅)‘𝐸)𝐼))) = (𝑍‘𝐼))
59	14, 37, 58	3eqtrd 2800	1 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐷‘𝐸) = (𝑍‘𝐼))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1568   ∈ wcel 2141   ∖ cdif 3901  {csn 4588  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410   ↑_m cmap 8823  Fincfn 8942  Basecbs 17268  ._rcmulr 17310  1_rcur 20262  Ringcrg 20314  CRingccrg 20315   Mat cmat 22543   matRRep cmarrep 22692   matRepV cmatrepV 22693   subMat csubma 22712   maDet cmdat 22720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176  ax-addf 11178  ax-mulf 11179

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-xor 1540  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4595  df-ot 4597  df-uni 4872  df-int 4912  df-iun 4957  df-iin 4958  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7674  df-om 7862  df-1st 7985  df-2nd 7986  df-supp 8156  df-tpos 8221  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8452  df-2o 8453  df-er 8693  df-map 8825  df-pm 8826  df-ixp 8895  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-fsupp 9321  df-sup 9401  df-oi 9471  df-card 9924  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-div 11871  df-nn 12233  df-2 12302  df-3 12303  df-4 12304  df-5 12305  df-6 12306  df-7 12307  df-8 12308  df-9 12309  df-n0 12504  df-xnn0 12577  df-z 12591  df-dec 12711  df-uz 12862  df-rp 13016  df-fz 13535  df-fzo 13682  df-seq 14037  df-exp 14097  df-hash 14366  df-word 14550  df-lsw 14599  df-concat 14607  df-s1 14633  df-substr 14678  df-pfx 14708  df-splice 14786  df-reverse 14795  df-s2 14884  df-struct 17206  df-sets 17223  df-slot 17241  df-ndx 17253  df-base 17269  df-ress 17290  df-plusg 17322  df-mulr 17323  df-starv 17324  df-sca 17325  df-vsca 17326  df-ip 17327  df-tset 17328  df-ple 17329  df-ds 17331  df-unif 17332  df-hom 17333  df-cco 17334  df-0g 17493  df-gsum 17494  df-prds 17499  df-pws 17501  df-mre 17637  df-mrc 17638  df-acs 17640  df-mgm 18697  df-sgrp 18776  df-mnd 18792  df-mhm 18840  df-submnd 18841  df-efmnd 18927  df-grp 19002  df-minusg 19003  df-sbg 19004  df-mulg 19133  df-subg 19188  df-ghm 19283  df-gim 19328  df-cntz 19386  df-oppg 19415  df-symg 19439  df-pmtr 19511  df-psgn 19560  df-cmn 19851  df-abl 19852  df-mgp 20216  df-rng 20230  df-ur 20263  df-srg 20268  df-ring 20316  df-cring 20317  df-oppr 20418  df-dvdsr 20438  df-unit 20439  df-invr 20469  df-dvr 20482  df-rhm 20553  df-subrng 20630  df-subrg 20654  df-drng 20814  df-lmod 20962  df-lss 21032  df-sra 21273  df-rgmod 21274  df-cnfld 21502  df-zring 21576  df-zrh 21632  df-dsmm 21861  df-frlm 21876  df-mamu 22527  df-mat 22544  df-marrep 22694  df-marepv 22695  df-subma 22713  df-mdet 22721  df-minmar1 22771

This theorem is referenced by:  cramerimp  22822