m2detleiblem3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > m2detleiblem3		Structured version Visualization version GIF version

Theorem m2detleiblem3 22971

Description: Lemma 3 for m2detleib 22973. (Contributed by AV, 16-Dec-2018.) (Proof shortened by AV, 2-Jan-2019.)

**Hypotheses**
Ref	Expression
m2detleiblem2.n	⊢ 𝑁 = {1, 2}
m2detleiblem2.p	⊢ 𝑃 = (Base‘(SymGrp‘𝑁))
m2detleiblem2.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
m2detleiblem2.b	⊢ 𝐵 = (Base‘𝐴)
m2detleiblem2.g	⊢ 𝐺 = (mulGrp‘𝑅)
m2detleiblem3.m	⊢ · = (+_g‘𝐺)

**Assertion**
Ref	Expression
m2detleiblem3	⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → (𝐺 Σ_g (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2)))

Distinct variable groups: 𝐵,𝑛 𝑛,𝑀 𝑛,𝑁 𝑃,𝑛 𝑄,𝑛 𝑅,𝑛 Allowed substitution hints: 𝐴(𝑛) · (𝑛) 𝐺(𝑛)

**Proof of Theorem m2detleiblem3**
Step	Hyp	Ref	Expression
1		m2detleiblem2.g	. . . 4 ⊢ 𝐺 = (mulGrp‘𝑅)
2		eqid 2763	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
3	1, 2	mgpbas 20392	. . 3 ⊢ (Base‘𝑅) = (Base‘𝐺)
4		m2detleiblem3.m	. . 3 ⊢ · = (+_g‘𝐺)
5	1	fvexi 6919	. . . 4 ⊢ 𝐺 ∈ V
6	5	a1i 11	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ V)
7		1ex 11327	. . . . . . 7 ⊢ 1 ∈ V
8		2nn 12440	. . . . . . 7 ⊢ 2 ∈ ℕ
9		prex 5400	. . . . . . . . 9 ⊢ {⟨1, 1⟩, ⟨2, 2⟩} ∈ V
10	9	prid1 4723	. . . . . . . 8 ⊢ {⟨1, 1⟩, ⟨2, 2⟩} ∈ {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}}
11		eqid 2763	. . . . . . . . 9 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
12		m2detleiblem2.p	. . . . . . . . 9 ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))
13		m2detleiblem2.n	. . . . . . . . 9 ⊢ 𝑁 = {1, 2}
14	11, 12, 13	symg2bas 19634	. . . . . . . 8 ⊢ ((1 ∈ V ∧ 2 ∈ ℕ) → 𝑃 = {{⟨1, 1⟩, ⟨2, 2⟩}, {⟨1, 2⟩, ⟨2, 1⟩}})
15	10, 14	eleqtrrid 2871	. . . . . . 7 ⊢ ((1 ∈ V ∧ 2 ∈ ℕ) → {⟨1, 1⟩, ⟨2, 2⟩} ∈ 𝑃)
16	7, 8, 15	mp2an 705	. . . . . 6 ⊢ {⟨1, 1⟩, ⟨2, 2⟩} ∈ 𝑃
17		eleq1 2852	. . . . . 6 ⊢ (𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} → (𝑄 ∈ 𝑃 ↔ {⟨1, 1⟩, ⟨2, 2⟩} ∈ 𝑃))
18	16, 17	mpbiri 261	. . . . 5 ⊢ (𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} → 𝑄 ∈ 𝑃)
19		m2detleiblem2.a	. . . . . . 7 ⊢ 𝐴 = (𝑁 Mat 𝑅)
20	13	oveq1i 7450	. . . . . . 7 ⊢ (𝑁 Mat 𝑅) = ({1, 2} Mat 𝑅)
21	19, 20	eqtri 2786	. . . . . 6 ⊢ 𝐴 = ({1, 2} Mat 𝑅)
22		m2detleiblem2.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐴)
23	13	fveq2i 6908	. . . . . . . 8 ⊢ (SymGrp‘𝑁) = (SymGrp‘{1, 2})
24	23	fveq2i 6908	. . . . . . 7 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘{1, 2}))
25	12, 24	eqtri 2786	. . . . . 6 ⊢ 𝑃 = (Base‘(SymGrp‘{1, 2}))
26	21, 22, 25	matepmcl 22804	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ {1, 2} ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅))
27	18, 26	syl3an2 1182	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ {1, 2} ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅))
28	13	mpteq1i 5199	. . . . 5 ⊢ (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)) = (𝑛 ∈ {1, 2} ↦ ((𝑄‘𝑛)𝑀𝑛))
29	28	fmpt 7131	. . . 4 ⊢ (∀𝑛 ∈ {1, 2} ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅) ↔ (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)):{1, 2}⟶(Base‘𝑅))
30	27, 29	sylib 221	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)):{1, 2}⟶(Base‘𝑅))
31	3, 4, 6, 30	gsumpr12val 18904	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → (𝐺 Σ_g (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) = (((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘1) · ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘2)))
32	7	prid1 4723	. . . . . 6 ⊢ 1 ∈ {1, 2}
33	32, 13	eleqtrri 2863	. . . . 5 ⊢ 1 ∈ 𝑁
34	19, 22, 12	matepmcl 22804	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ 𝑁 ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅))
35	18, 34	syl3an2 1182	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ 𝑁 ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅))
36		fveq2 6905	. . . . . . . . 9 ⊢ (𝑛 = 1 → (𝑄‘𝑛) = (𝑄‘1))
37		id 23	. . . . . . . . 9 ⊢ (𝑛 = 1 → 𝑛 = 1)
38	36, 37	oveq12d 7458	. . . . . . . 8 ⊢ (𝑛 = 1 → ((𝑄‘𝑛)𝑀𝑛) = ((𝑄‘1)𝑀1))
39	38	eleq1d 2849	. . . . . . 7 ⊢ (𝑛 = 1 → (((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅) ↔ ((𝑄‘1)𝑀1) ∈ (Base‘𝑅)))
40	39	rspcva 3578	. . . . . 6 ⊢ ((1 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅)) → ((𝑄‘1)𝑀1) ∈ (Base‘𝑅))
41	33, 35, 40	sylancr 599	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ((𝑄‘1)𝑀1) ∈ (Base‘𝑅))
42		eqid 2763	. . . . . 6 ⊢ (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)) = (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))
43	38, 42	fvmptg 7011	. . . . 5 ⊢ ((1 ∈ 𝑁 ∧ ((𝑄‘1)𝑀1) ∈ (Base‘𝑅)) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘1) = ((𝑄‘1)𝑀1))
44	33, 41, 43	sylancr 599	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘1) = ((𝑄‘1)𝑀1))
45		fveq1 6904	. . . . . . 7 ⊢ (𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} → (𝑄‘1) = ({⟨1, 1⟩, ⟨2, 2⟩}‘1))
46		1ne2 12577	. . . . . . . 8 ⊢ 1 ≠ 2
47	7, 7	fvpr1 7217	. . . . . . . 8 ⊢ (1 ≠ 2 → ({⟨1, 1⟩, ⟨2, 2⟩}‘1) = 1)
48	46, 47	ax-mp 5	. . . . . . 7 ⊢ ({⟨1, 1⟩, ⟨2, 2⟩}‘1) = 1
49	45, 48	eqtrdi 2814	. . . . . 6 ⊢ (𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} → (𝑄‘1) = 1)
50	49	3ad2ant2 1152	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → (𝑄‘1) = 1)
51	50	oveq1d 7455	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ((𝑄‘1)𝑀1) = (1𝑀1))
52	44, 51	eqtrd 2798	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘1) = (1𝑀1))
53		2ex 12444	. . . . . . 7 ⊢ 2 ∈ V
54	53	prid2 4724	. . . . . 6 ⊢ 2 ∈ {1, 2}
55	54, 13	eleqtrri 2863	. . . . 5 ⊢ 2 ∈ 𝑁
56		fveq2 6905	. . . . . . . . 9 ⊢ (𝑛 = 2 → (𝑄‘𝑛) = (𝑄‘2))
57		id 23	. . . . . . . . 9 ⊢ (𝑛 = 2 → 𝑛 = 2)
58	56, 57	oveq12d 7458	. . . . . . . 8 ⊢ (𝑛 = 2 → ((𝑄‘𝑛)𝑀𝑛) = ((𝑄‘2)𝑀2))
59	58	eleq1d 2849	. . . . . . 7 ⊢ (𝑛 = 2 → (((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅) ↔ ((𝑄‘2)𝑀2) ∈ (Base‘𝑅)))
60	59	rspcva 3578	. . . . . 6 ⊢ ((2 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅)) → ((𝑄‘2)𝑀2) ∈ (Base‘𝑅))
61	55, 35, 60	sylancr 599	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ((𝑄‘2)𝑀2) ∈ (Base‘𝑅))
62	58, 42	fvmptg 7011	. . . . 5 ⊢ ((2 ∈ 𝑁 ∧ ((𝑄‘2)𝑀2) ∈ (Base‘𝑅)) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘2) = ((𝑄‘2)𝑀2))
63	55, 61, 62	sylancr 599	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘2) = ((𝑄‘2)𝑀2))
64		fveq1 6904	. . . . . . 7 ⊢ (𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} → (𝑄‘2) = ({⟨1, 1⟩, ⟨2, 2⟩}‘2))
65	53, 53	fvpr2 7218	. . . . . . . 8 ⊢ (1 ≠ 2 → ({⟨1, 1⟩, ⟨2, 2⟩}‘2) = 2)
66	46, 65	ax-mp 5	. . . . . . 7 ⊢ ({⟨1, 1⟩, ⟨2, 2⟩}‘2) = 2
67	64, 66	eqtrdi 2814	. . . . . 6 ⊢ (𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} → (𝑄‘2) = 2)
68	67	3ad2ant2 1152	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → (𝑄‘2) = 2)
69	68	oveq1d 7455	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ((𝑄‘2)𝑀2) = (2𝑀2))
70	63, 69	eqtrd 2798	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘2) = (2𝑀2))
71	52, 70	oveq12d 7458	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → (((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘1) · ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘2)) = ((1𝑀1) · (2𝑀2)))
72	31, 71	eqtrd 2798	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → (𝐺 Σ_g (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 Vcvv 3454 {cpr 4590 ⟨cop 4838 ↦ cmpt 5189 ⟶wf 6551 ‘cfv 6555 (class class class)co 7440 1c1 11225 ℕcn 12359 2c2 12421 Basecbs 17413 +_gcplusg 17454 Σ_g cgsu 17637 SymGrpcsymg 19610 mulGrpcmgp 20387 Ringcrg 20486 Mat cmat 22749

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-ot 4862 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-om 7899 df-1st 8022 df-2nd 8023 df-supp 8202 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-2o 8502 df-oadd 8505 df-er 8742 df-map 8874 df-pm 8875 df-ixp 8951 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-fsupp 9379 df-sup 9458 df-dju 10006 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-7 12434 df-8 12435 df-9 12436 df-n0 12631 df-xnn0 12704 df-z 12718 df-dec 12839 df-uz 12990 df-fz 13664 df-seq 14169 df-fac 14442 df-bc 14471 df-hash 14499 df-struct 17351 df-sets 17368 df-slot 17386 df-ndx 17398 df-base 17414 df-ress 17435 df-plusg 17467 df-mulr 17468 df-sca 17470 df-vsca 17471 df-ip 17472 df-tset 17473 df-ple 17474 df-ds 17476 df-hom 17478 df-cco 17479 df-0g 17638 df-gsum 17639 df-prds 17644 df-pws 17646 df-efmnd 19091 df-symg 19611 df-mgp 20388 df-sra 21475 df-rgmod 21476 df-dsmm 22065 df-frlm 22080 df-mat 22750

This theorem is used by: m2detleib 22973

W3C validator