scmatsgrp1 - Metamath Proof Explorer

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

Theorem scmatsgrp1 20451

Description: The set of scalar matrices is a subgroup of the group/ring of diagonal matrices. (Contributed by AV, 21-Aug-2019.)

**Hypotheses**
Ref	Expression
scmatid.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
scmatid.b	⊢ 𝐵 = (Base‘𝐴)
scmatid.e	⊢ 𝐸 = (Base‘𝑅)
scmatid.0	⊢ 0 = (0_g‘𝑅)
scmatid.s	⊢ 𝑆 = (𝑁 ScMat 𝑅)
scmatsgrp1.d	⊢ 𝐷 = (𝑁 DMat 𝑅)
scmatsgrp1.c	⊢ 𝐶 = (𝐴 ↾_s 𝐷)

**Assertion**
Ref	Expression
scmatsgrp1	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubGrp‘𝐶))

Proof of Theorem scmatsgrp1 Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		scmatid.a	. . . . 5 ⊢ 𝐴 = (𝑁 Mat 𝑅)
2		scmatid.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐴)
3		scmatid.e	. . . . 5 ⊢ 𝐸 = (Base‘𝑅)
4		scmatid.0	. . . . 5 ⊢ 0 = (0_g‘𝑅)
5		scmatid.s	. . . . 5 ⊢ 𝑆 = (𝑁 ScMat 𝑅)
6		scmatsgrp1.d	. . . . 5 ⊢ 𝐷 = (𝑁 DMat 𝑅)
7	1, 2, 3, 4, 5, 6	scmatdmat 20444	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → 𝑥 ∈ 𝐷))
8	7	ssrdv 3715	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ⊆ 𝐷)
9	1, 2, 4, 6	dmatsgrp 20428	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → 𝐷 ∈ (SubGrp‘𝐴))
10	9	ancoms 468	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐷 ∈ (SubGrp‘𝐴))
11		scmatsgrp1.c	. . . . . 6 ⊢ 𝐶 = (𝐴 ↾_s 𝐷)
12	11	subgbas 17720	. . . . 5 ⊢ (𝐷 ∈ (SubGrp‘𝐴) → 𝐷 = (Base‘𝐶))
13	12	eqcomd 2730	. . . 4 ⊢ (𝐷 ∈ (SubGrp‘𝐴) → (Base‘𝐶) = 𝐷)
14	10, 13	syl 17	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘𝐶) = 𝐷)
15	8, 14	sseqtr4d 3748	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ⊆ (Base‘𝐶))
16	1, 2, 3, 4, 5	scmatid 20443	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1_r‘𝐴) ∈ 𝑆)
17		ne0i 4029	. . 3 ⊢ ((1_r‘𝐴) ∈ 𝑆 → 𝑆 ≠ ∅)
18	16, 17	syl 17	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ≠ ∅)
19	10	adantr 472	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝐷 ∈ (SubGrp‘𝐴))
20	7	com12 32	. . . . . . 7 ⊢ (𝑥 ∈ 𝑆 → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑥 ∈ 𝐷))
21	20	adantr 472	. . . . . 6 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑥 ∈ 𝐷))
22	21	impcom 445	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ 𝐷)
23	1, 2, 3, 4, 5, 6	scmatdmat 20444	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ 𝑆 → 𝑦 ∈ 𝐷))
24	23	a1d 25	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → (𝑦 ∈ 𝑆 → 𝑦 ∈ 𝐷)))
25	24	imp32 448	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝐷)
26		eqid 2724	. . . . . . 7 ⊢ (-_g‘𝐴) = (-_g‘𝐴)
27		eqid 2724	. . . . . . 7 ⊢ (-_g‘𝐶) = (-_g‘𝐶)
28	26, 11, 27	subgsub 17728	. . . . . 6 ⊢ ((𝐷 ∈ (SubGrp‘𝐴) ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥(-_g‘𝐴)𝑦) = (𝑥(-_g‘𝐶)𝑦))
29	28	eqcomd 2730	. . . . 5 ⊢ ((𝐷 ∈ (SubGrp‘𝐴) ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥(-_g‘𝐶)𝑦) = (𝑥(-_g‘𝐴)𝑦))
30	19, 22, 25, 29	syl3anc 1439	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(-_g‘𝐶)𝑦) = (𝑥(-_g‘𝐴)𝑦))
31	1, 2, 3, 4, 5	scmatsubcl 20446	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(-_g‘𝐴)𝑦) ∈ 𝑆)
32	30, 31	eqeltrd 2803	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(-_g‘𝐶)𝑦) ∈ 𝑆)
33	32	ralrimivva 3073	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(-_g‘𝐶)𝑦) ∈ 𝑆)
34	1, 2, 4, 6	dmatsrng 20430	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → 𝐷 ∈ (SubRing‘𝐴))
35	34	ancoms 468	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐷 ∈ (SubRing‘𝐴))
36	11	subrgring 18906	. . . 4 ⊢ (𝐷 ∈ (SubRing‘𝐴) → 𝐶 ∈ Ring)
37	35, 36	syl 17	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring)
38		ringgrp 18673	. . 3 ⊢ (𝐶 ∈ Ring → 𝐶 ∈ Grp)
39		eqid 2724	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
40	39, 27	issubg4 17735	. . 3 ⊢ (𝐶 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐶) ↔ (𝑆 ⊆ (Base‘𝐶) ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(-_g‘𝐶)𝑦) ∈ 𝑆)))
41	37, 38, 40	3syl 18	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑆 ∈ (SubGrp‘𝐶) ↔ (𝑆 ⊆ (Base‘𝐶) ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(-_g‘𝐶)𝑦) ∈ 𝑆)))
42	15, 18, 33, 41	mpbir3and 1382	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubGrp‘𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∧ w3a 1072 = wceq 1596 ∈ wcel 2103 ≠ wne 2896 ∀wral 3014 ⊆ wss 3680 ∅c0 4023 ‘cfv 6001 (class class class)co 6765 Fincfn 8072 Basecbs 15980 ↾_s cress 15981 0_gc0g 16223 Grpcgrp 17544 -_gcsg 17546 SubGrpcsubg 17710 1_rcur 18622 Ringcrg 18668 SubRingcsubrg 18899 Mat cmat 20336 DMat cdmat 20417 ScMat cscmat 20418

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-rep 4879 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 ax-inf2 8651 ax-cnex 10105 ax-resscn 10106 ax-1cn 10107 ax-icn 10108 ax-addcl 10109 ax-addrcl 10110 ax-mulcl 10111 ax-mulrcl 10112 ax-mulcom 10113 ax-addass 10114 ax-mulass 10115 ax-distr 10116 ax-i2m1 10117 ax-1ne0 10118 ax-1rid 10119 ax-rnegex 10120 ax-rrecex 10121 ax-cnre 10122 ax-pre-lttri 10123 ax-pre-lttrn 10124 ax-pre-ltadd 10125 ax-pre-mulgt0 10126

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-nel 3000 df-ral 3019 df-rex 3020 df-reu 3021 df-rmo 3022 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-pss 3696 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-tp 4290 df-op 4292 df-ot 4294 df-uni 4545 df-int 4584 df-iun 4630 df-iin 4631 df-br 4761 df-opab 4821 df-mpt 4838 df-tr 4861 df-id 5128 df-eprel 5133 df-po 5139 df-so 5140 df-fr 5177 df-se 5178 df-we 5179 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-pred 5793 df-ord 5839 df-on 5840 df-lim 5841 df-suc 5842 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-isom 6010 df-riota 6726 df-ov 6768 df-oprab 6769 df-mpt2 6770 df-of 7014 df-om 7183 df-1st 7285 df-2nd 7286 df-supp 7416 df-wrecs 7527 df-recs 7588 df-rdg 7626 df-1o 7680 df-oadd 7684 df-er 7862 df-map 7976 df-ixp 8026 df-en 8073 df-dom 8074 df-sdom 8075 df-fin 8076 df-fsupp 8392 df-sup 8464 df-oi 8531 df-card 8878 df-pnf 10189 df-mnf 10190 df-xr 10191 df-ltxr 10192 df-le 10193 df-sub 10381 df-neg 10382 df-nn 11134 df-2 11192 df-3 11193 df-4 11194 df-5 11195 df-6 11196 df-7 11197 df-8 11198 df-9 11199 df-n0 11406 df-z 11491 df-dec 11607 df-uz 11801 df-fz 12441 df-fzo 12581 df-seq 12917 df-hash 13233 df-struct 15982 df-ndx 15983 df-slot 15984 df-base 15986 df-sets 15987 df-ress 15988 df-plusg 16077 df-mulr 16078 df-sca 16080 df-vsca 16081 df-ip 16082 df-tset 16083 df-ple 16084 df-ds 16087 df-hom 16089 df-cco 16090 df-0g 16225 df-gsum 16226 df-prds 16231 df-pws 16233 df-mre 16369 df-mrc 16370 df-acs 16372 df-mgm 17364 df-sgrp 17406 df-mnd 17417 df-mhm 17457 df-submnd 17458 df-grp 17547 df-minusg 17548 df-sbg 17549 df-mulg 17663 df-subg 17713 df-ghm 17780 df-cntz 17871 df-cmn 18316 df-abl 18317 df-mgp 18611 df-ur 18623 df-ring 18670 df-subrg 18901 df-lmod 18988 df-lss 19056 df-sra 19295 df-rgmod 19296 df-dsmm 20199 df-frlm 20214 df-mamu 20313 df-mat 20337 df-dmat 20419 df-scmat 20420

This theorem is referenced by: scmatsrng1 20452

W3C validator