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

Theorem frlmsslsp 20933
 Description: A subset of a free module obtained by restricting the support set is spanned by the relevant unit vectors. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by AV, 24-Jun-2019.)
Hypotheses
Ref Expression
frlmsslsp.y 𝑌 = (𝑅 freeLMod 𝐼)
frlmsslsp.u 𝑈 = (𝑅 unitVec 𝐼)
frlmsslsp.k 𝐾 = (LSpan‘𝑌)
frlmsslsp.b 𝐵 = (Base‘𝑌)
frlmsslsp.z 0 = (0g𝑅)
frlmsslsp.c 𝐶 = {𝑥𝐵 ∣ (𝑥 supp 0 ) ⊆ 𝐽}
Assertion
Ref Expression
frlmsslsp ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (𝐾‘(𝑈𝐽)) = 𝐶)
Distinct variable groups:   𝑥,𝑌   𝑥,𝑈   𝑥,𝐵   𝑥, 0   𝑥,𝑅   𝑥,𝐼   𝑥,𝑉   𝑥,𝐽   𝑥,𝐾
Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem frlmsslsp
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frlmsslsp.y . . . . 5 𝑌 = (𝑅 freeLMod 𝐼)
21frlmlmod 20886 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼𝑉) → 𝑌 ∈ LMod)
323adant3 1129 . . 3 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 𝑌 ∈ LMod)
4 eqid 2824 . . . 4 (LSubSp‘𝑌) = (LSubSp‘𝑌)
5 frlmsslsp.b . . . 4 𝐵 = (Base‘𝑌)
6 frlmsslsp.z . . . 4 0 = (0g𝑅)
7 frlmsslsp.c . . . 4 𝐶 = {𝑥𝐵 ∣ (𝑥 supp 0 ) ⊆ 𝐽}
81, 4, 5, 6, 7frlmsslss2 20912 . . 3 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 𝐶 ∈ (LSubSp‘𝑌))
9 frlmsslsp.u . . . . . . . . . 10 𝑈 = (𝑅 unitVec 𝐼)
109, 1, 5uvcff 20928 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝐼𝑉) → 𝑈:𝐼𝐵)
11103adant3 1129 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 𝑈:𝐼𝐵)
1211adantr 484 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) → 𝑈:𝐼𝐵)
13 simp3 1135 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 𝐽𝐼)
1413sselda 3952 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) → 𝑦𝐼)
1512, 14ffvelrnd 6840 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) → (𝑈𝑦) ∈ 𝐵)
16 simpl2 1189 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) → 𝐼𝑉)
17 eqid 2824 . . . . . . . . 9 (Base‘𝑅) = (Base‘𝑅)
181, 17, 5frlmbasf 20897 . . . . . . . 8 ((𝐼𝑉 ∧ (𝑈𝑦) ∈ 𝐵) → (𝑈𝑦):𝐼⟶(Base‘𝑅))
1916, 15, 18syl2anc 587 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) → (𝑈𝑦):𝐼⟶(Base‘𝑅))
20 simpll1 1209 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) ∧ 𝑥 ∈ (𝐼𝐽)) → 𝑅 ∈ Ring)
21 simpll2 1210 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) ∧ 𝑥 ∈ (𝐼𝐽)) → 𝐼𝑉)
2214adantr 484 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) ∧ 𝑥 ∈ (𝐼𝐽)) → 𝑦𝐼)
23 eldifi 4088 . . . . . . . . 9 (𝑥 ∈ (𝐼𝐽) → 𝑥𝐼)
2423adantl 485 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) ∧ 𝑥 ∈ (𝐼𝐽)) → 𝑥𝐼)
25 disjdif 4403 . . . . . . . . . 10 (𝐽 ∩ (𝐼𝐽)) = ∅
26 disjne 4386 . . . . . . . . . 10 (((𝐽 ∩ (𝐼𝐽)) = ∅ ∧ 𝑦𝐽𝑥 ∈ (𝐼𝐽)) → 𝑦𝑥)
2725, 26mp3an1 1445 . . . . . . . . 9 ((𝑦𝐽𝑥 ∈ (𝐼𝐽)) → 𝑦𝑥)
2827adantll 713 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) ∧ 𝑥 ∈ (𝐼𝐽)) → 𝑦𝑥)
299, 20, 21, 22, 24, 28, 6uvcvv0 20927 . . . . . . 7 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) ∧ 𝑥 ∈ (𝐼𝐽)) → ((𝑈𝑦)‘𝑥) = 0 )
3019, 29suppss 7850 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) → ((𝑈𝑦) supp 0 ) ⊆ 𝐽)
31 oveq1 7152 . . . . . . . 8 (𝑥 = (𝑈𝑦) → (𝑥 supp 0 ) = ((𝑈𝑦) supp 0 ))
3231sseq1d 3983 . . . . . . 7 (𝑥 = (𝑈𝑦) → ((𝑥 supp 0 ) ⊆ 𝐽 ↔ ((𝑈𝑦) supp 0 ) ⊆ 𝐽))
3332, 7elrab2 3669 . . . . . 6 ((𝑈𝑦) ∈ 𝐶 ↔ ((𝑈𝑦) ∈ 𝐵 ∧ ((𝑈𝑦) supp 0 ) ⊆ 𝐽))
3415, 30, 33sylanbrc 586 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐽) → (𝑈𝑦) ∈ 𝐶)
3534ralrimiva 3177 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → ∀𝑦𝐽 (𝑈𝑦) ∈ 𝐶)
3611ffund 6506 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → Fun 𝑈)
3711fdmd 6511 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → dom 𝑈 = 𝐼)
3813, 37sseqtrrd 3993 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 𝐽 ⊆ dom 𝑈)
39 funimass4 6718 . . . . 5 ((Fun 𝑈𝐽 ⊆ dom 𝑈) → ((𝑈𝐽) ⊆ 𝐶 ↔ ∀𝑦𝐽 (𝑈𝑦) ∈ 𝐶))
4036, 38, 39syl2anc 587 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → ((𝑈𝐽) ⊆ 𝐶 ↔ ∀𝑦𝐽 (𝑈𝑦) ∈ 𝐶))
4135, 40mpbird 260 . . 3 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (𝑈𝐽) ⊆ 𝐶)
42 frlmsslsp.k . . . 4 𝐾 = (LSpan‘𝑌)
434, 42lspssp 19753 . . 3 ((𝑌 ∈ LMod ∧ 𝐶 ∈ (LSubSp‘𝑌) ∧ (𝑈𝐽) ⊆ 𝐶) → (𝐾‘(𝑈𝐽)) ⊆ 𝐶)
443, 8, 41, 43syl3anc 1368 . 2 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (𝐾‘(𝑈𝐽)) ⊆ 𝐶)
45 simpl1 1188 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑅 ∈ Ring)
46 simpl2 1189 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝐼𝑉)
477ssrab3 4042 . . . . . 6 𝐶𝐵
4847a1i 11 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 𝐶𝐵)
4948sselda 3952 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑦𝐵)
50 eqid 2824 . . . . 5 ( ·𝑠𝑌) = ( ·𝑠𝑌)
519, 1, 5, 50uvcresum 20930 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝑦𝐵) → 𝑦 = (𝑌 Σg (𝑦f ( ·𝑠𝑌)𝑈)))
5245, 46, 49, 51syl3anc 1368 . . 3 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑦 = (𝑌 Σg (𝑦f ( ·𝑠𝑌)𝑈)))
53 eqid 2824 . . . 4 (0g𝑌) = (0g𝑌)
54 lmodabl 19674 . . . . . 6 (𝑌 ∈ LMod → 𝑌 ∈ Abel)
553, 54syl 17 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 𝑌 ∈ Abel)
5655adantr 484 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑌 ∈ Abel)
57 imassrn 5927 . . . . . . . 8 (𝑈𝐽) ⊆ ran 𝑈
5811frnd 6509 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → ran 𝑈𝐵)
5957, 58sstrid 3963 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (𝑈𝐽) ⊆ 𝐵)
605, 4, 42lspcl 19741 . . . . . . 7 ((𝑌 ∈ LMod ∧ (𝑈𝐽) ⊆ 𝐵) → (𝐾‘(𝑈𝐽)) ∈ (LSubSp‘𝑌))
613, 59, 60syl2anc 587 . . . . . 6 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (𝐾‘(𝑈𝐽)) ∈ (LSubSp‘𝑌))
624lsssubg 19722 . . . . . 6 ((𝑌 ∈ LMod ∧ (𝐾‘(𝑈𝐽)) ∈ (LSubSp‘𝑌)) → (𝐾‘(𝑈𝐽)) ∈ (SubGrp‘𝑌))
633, 61, 62syl2anc 587 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (𝐾‘(𝑈𝐽)) ∈ (SubGrp‘𝑌))
6463adantr 484 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (𝐾‘(𝑈𝐽)) ∈ (SubGrp‘𝑌))
651, 17, 5frlmbasf 20897 . . . . . . . . 9 ((𝐼𝑉𝑦𝐵) → 𝑦:𝐼⟶(Base‘𝑅))
66653ad2antl2 1183 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) → 𝑦:𝐼⟶(Base‘𝑅))
6766ffnd 6503 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) → 𝑦 Fn 𝐼)
6811ffnd 6503 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 𝑈 Fn 𝐼)
6968adantr 484 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) → 𝑈 Fn 𝐼)
70 simpl2 1189 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) → 𝐼𝑉)
71 inidm 4179 . . . . . . 7 (𝐼𝐼) = 𝐼
7267, 69, 70, 70, 71offn 7410 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) → (𝑦f ( ·𝑠𝑌)𝑈) Fn 𝐼)
7349, 72syldan 594 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (𝑦f ( ·𝑠𝑌)𝑈) Fn 𝐼)
7449, 67syldan 594 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑦 Fn 𝐼)
7574adantrr 716 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) → 𝑦 Fn 𝐼)
7668adantr 484 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) → 𝑈 Fn 𝐼)
77 simpl2 1189 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) → 𝐼𝑉)
78 simprr 772 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) → 𝑧𝐼)
79 fnfvof 7413 . . . . . . . . 9 (((𝑦 Fn 𝐼𝑈 Fn 𝐼) ∧ (𝐼𝑉𝑧𝐼)) → ((𝑦f ( ·𝑠𝑌)𝑈)‘𝑧) = ((𝑦𝑧)( ·𝑠𝑌)(𝑈𝑧)))
8075, 76, 77, 78, 79syl22anc 837 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) → ((𝑦f ( ·𝑠𝑌)𝑈)‘𝑧) = ((𝑦𝑧)( ·𝑠𝑌)(𝑈𝑧)))
813adantr 484 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → 𝑌 ∈ LMod)
8261adantr 484 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → (𝐾‘(𝑈𝐽)) ∈ (LSubSp‘𝑌))
8347sseli 3948 . . . . . . . . . . . . . . . 16 (𝑦𝐶𝑦𝐵)
8483, 66sylan2 595 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑦:𝐼⟶(Base‘𝑅))
8584adantrr 716 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → 𝑦:𝐼⟶(Base‘𝑅))
8613sselda 3952 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑧𝐽) → 𝑧𝐼)
8786adantrl 715 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → 𝑧𝐼)
8885, 87ffvelrnd 6840 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → (𝑦𝑧) ∈ (Base‘𝑅))
891frlmsca 20890 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝐼𝑉) → 𝑅 = (Scalar‘𝑌))
90893adant3 1129 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 𝑅 = (Scalar‘𝑌))
9190fveq2d 6662 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (Base‘𝑅) = (Base‘(Scalar‘𝑌)))
9291adantr 484 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → (Base‘𝑅) = (Base‘(Scalar‘𝑌)))
9388, 92eleqtrd 2918 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → (𝑦𝑧) ∈ (Base‘(Scalar‘𝑌)))
945, 42lspssid 19750 . . . . . . . . . . . . . . 15 ((𝑌 ∈ LMod ∧ (𝑈𝐽) ⊆ 𝐵) → (𝑈𝐽) ⊆ (𝐾‘(𝑈𝐽)))
953, 59, 94syl2anc 587 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (𝑈𝐽) ⊆ (𝐾‘(𝑈𝐽)))
9695adantr 484 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → (𝑈𝐽) ⊆ (𝐾‘(𝑈𝐽)))
97 funfvima2 6982 . . . . . . . . . . . . . . . 16 ((Fun 𝑈𝐽 ⊆ dom 𝑈) → (𝑧𝐽 → (𝑈𝑧) ∈ (𝑈𝐽)))
9836, 38, 97syl2anc 587 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (𝑧𝐽 → (𝑈𝑧) ∈ (𝑈𝐽)))
9998imp 410 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑧𝐽) → (𝑈𝑧) ∈ (𝑈𝐽))
10099adantrl 715 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → (𝑈𝑧) ∈ (𝑈𝐽))
10196, 100sseldd 3953 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → (𝑈𝑧) ∈ (𝐾‘(𝑈𝐽)))
102 eqid 2824 . . . . . . . . . . . . 13 (Scalar‘𝑌) = (Scalar‘𝑌)
103 eqid 2824 . . . . . . . . . . . . 13 (Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌))
104102, 50, 103, 4lssvscl 19720 . . . . . . . . . . . 12 (((𝑌 ∈ LMod ∧ (𝐾‘(𝑈𝐽)) ∈ (LSubSp‘𝑌)) ∧ ((𝑦𝑧) ∈ (Base‘(Scalar‘𝑌)) ∧ (𝑈𝑧) ∈ (𝐾‘(𝑈𝐽)))) → ((𝑦𝑧)( ·𝑠𝑌)(𝑈𝑧)) ∈ (𝐾‘(𝑈𝐽)))
10581, 82, 93, 101, 104syl22anc 837 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐽)) → ((𝑦𝑧)( ·𝑠𝑌)(𝑈𝑧)) ∈ (𝐾‘(𝑈𝐽)))
106105anassrs 471 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) ∧ 𝑧𝐽) → ((𝑦𝑧)( ·𝑠𝑌)(𝑈𝑧)) ∈ (𝐾‘(𝑈𝐽)))
107106adantlrr 720 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ 𝑧𝐽) → ((𝑦𝑧)( ·𝑠𝑌)(𝑈𝑧)) ∈ (𝐾‘(𝑈𝐽)))
108 id 22 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶))
109108adantrr 716 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) → ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶))
110109adantr 484 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶))
111 simplrr 777 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → 𝑧𝐼)
112 simpr 488 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → ¬ 𝑧𝐽)
113111, 112eldifd 3930 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → 𝑧 ∈ (𝐼𝐽))
114 oveq1 7152 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝑥 supp 0 ) = (𝑦 supp 0 ))
115114sseq1d 3983 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝑥 supp 0 ) ⊆ 𝐽 ↔ (𝑦 supp 0 ) ⊆ 𝐽))
116115, 7elrab2 3669 . . . . . . . . . . . . . . . . 17 (𝑦𝐶 ↔ (𝑦𝐵 ∧ (𝑦 supp 0 ) ⊆ 𝐽))
117116simprbi 500 . . . . . . . . . . . . . . . 16 (𝑦𝐶 → (𝑦 supp 0 ) ⊆ 𝐽)
118117adantl 485 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (𝑦 supp 0 ) ⊆ 𝐽)
1196fvexi 6672 . . . . . . . . . . . . . . . 16 0 ∈ V
120119a1i 11 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 0 ∈ V)
12184, 118, 46, 120suppssr 7851 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) ∧ 𝑧 ∈ (𝐼𝐽)) → (𝑦𝑧) = 0 )
122110, 113, 121syl2anc 587 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → (𝑦𝑧) = 0 )
12390fveq2d 6662 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (0g𝑅) = (0g‘(Scalar‘𝑌)))
1246, 123syl5eq 2871 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 0 = (0g‘(Scalar‘𝑌)))
125124ad2antrr 725 . . . . . . . . . . . . 13 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → 0 = (0g‘(Scalar‘𝑌)))
126122, 125eqtrd 2859 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → (𝑦𝑧) = (0g‘(Scalar‘𝑌)))
127126oveq1d 7160 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → ((𝑦𝑧)( ·𝑠𝑌)(𝑈𝑧)) = ((0g‘(Scalar‘𝑌))( ·𝑠𝑌)(𝑈𝑧)))
1283ad2antrr 725 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → 𝑌 ∈ LMod)
12911ffvelrnda 6839 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑧𝐼) → (𝑈𝑧) ∈ 𝐵)
130129adantrl 715 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) → (𝑈𝑧) ∈ 𝐵)
131130adantr 484 . . . . . . . . . . . 12 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → (𝑈𝑧) ∈ 𝐵)
132 eqid 2824 . . . . . . . . . . . . 13 (0g‘(Scalar‘𝑌)) = (0g‘(Scalar‘𝑌))
1335, 102, 50, 132, 53lmod0vs 19660 . . . . . . . . . . . 12 ((𝑌 ∈ LMod ∧ (𝑈𝑧) ∈ 𝐵) → ((0g‘(Scalar‘𝑌))( ·𝑠𝑌)(𝑈𝑧)) = (0g𝑌))
134128, 131, 133syl2anc 587 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → ((0g‘(Scalar‘𝑌))( ·𝑠𝑌)(𝑈𝑧)) = (0g𝑌))
135127, 134eqtrd 2859 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → ((𝑦𝑧)( ·𝑠𝑌)(𝑈𝑧)) = (0g𝑌))
13661ad2antrr 725 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → (𝐾‘(𝑈𝐽)) ∈ (LSubSp‘𝑌))
13753, 4lss0cl 19711 . . . . . . . . . . 11 ((𝑌 ∈ LMod ∧ (𝐾‘(𝑈𝐽)) ∈ (LSubSp‘𝑌)) → (0g𝑌) ∈ (𝐾‘(𝑈𝐽)))
138128, 136, 137syl2anc 587 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → (0g𝑌) ∈ (𝐾‘(𝑈𝐽)))
139135, 138eqeltrd 2916 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) ∧ ¬ 𝑧𝐽) → ((𝑦𝑧)( ·𝑠𝑌)(𝑈𝑧)) ∈ (𝐾‘(𝑈𝐽)))
140107, 139pm2.61dan 812 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) → ((𝑦𝑧)( ·𝑠𝑌)(𝑈𝑧)) ∈ (𝐾‘(𝑈𝐽)))
14180, 140eqeltrd 2916 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ (𝑦𝐶𝑧𝐼)) → ((𝑦f ( ·𝑠𝑌)𝑈)‘𝑧) ∈ (𝐾‘(𝑈𝐽)))
142141expr 460 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (𝑧𝐼 → ((𝑦f ( ·𝑠𝑌)𝑈)‘𝑧) ∈ (𝐾‘(𝑈𝐽))))
143142ralrimiv 3176 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → ∀𝑧𝐼 ((𝑦f ( ·𝑠𝑌)𝑈)‘𝑧) ∈ (𝐾‘(𝑈𝐽)))
144 ffnfv 6870 . . . . 5 ((𝑦f ( ·𝑠𝑌)𝑈):𝐼⟶(𝐾‘(𝑈𝐽)) ↔ ((𝑦f ( ·𝑠𝑌)𝑈) Fn 𝐼 ∧ ∀𝑧𝐼 ((𝑦f ( ·𝑠𝑌)𝑈)‘𝑧) ∈ (𝐾‘(𝑈𝐽))))
14573, 143, 144sylanbrc 586 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (𝑦f ( ·𝑠𝑌)𝑈):𝐼⟶(𝐾‘(𝑈𝐽)))
1461, 6, 5frlmbasfsupp 20895 . . . . . . . 8 ((𝐼𝑉𝑦𝐵) → 𝑦 finSupp 0 )
147146fsuppimpd 8831 . . . . . . 7 ((𝐼𝑉𝑦𝐵) → (𝑦 supp 0 ) ∈ Fin)
14846, 49, 147syl2anc 587 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (𝑦 supp 0 ) ∈ Fin)
149 dffn2 6504 . . . . . . . . 9 ((𝑦f ( ·𝑠𝑌)𝑈) Fn 𝐼 ↔ (𝑦f ( ·𝑠𝑌)𝑈):𝐼⟶V)
15072, 149sylib 221 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) → (𝑦f ( ·𝑠𝑌)𝑈):𝐼⟶V)
15167adantr 484 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → 𝑦 Fn 𝐼)
15268ad2antrr 725 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → 𝑈 Fn 𝐼)
153 simpll2 1210 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → 𝐼𝑉)
154 eldifi 4088 . . . . . . . . . . 11 (𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 )) → 𝑥𝐼)
155154adantl 485 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → 𝑥𝐼)
156 fnfvof 7413 . . . . . . . . . 10 (((𝑦 Fn 𝐼𝑈 Fn 𝐼) ∧ (𝐼𝑉𝑥𝐼)) → ((𝑦f ( ·𝑠𝑌)𝑈)‘𝑥) = ((𝑦𝑥)( ·𝑠𝑌)(𝑈𝑥)))
157151, 152, 153, 155, 156syl22anc 837 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → ((𝑦f ( ·𝑠𝑌)𝑈)‘𝑥) = ((𝑦𝑥)( ·𝑠𝑌)(𝑈𝑥)))
158 ssidd 3975 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) → (𝑦 supp 0 ) ⊆ (𝑦 supp 0 ))
159119a1i 11 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) → 0 ∈ V)
16066, 158, 70, 159suppssr 7851 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → (𝑦𝑥) = 0 )
161124ad2antrr 725 . . . . . . . . . . 11 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → 0 = (0g‘(Scalar‘𝑌)))
162160, 161eqtrd 2859 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → (𝑦𝑥) = (0g‘(Scalar‘𝑌)))
163162oveq1d 7160 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → ((𝑦𝑥)( ·𝑠𝑌)(𝑈𝑥)) = ((0g‘(Scalar‘𝑌))( ·𝑠𝑌)(𝑈𝑥)))
1643ad2antrr 725 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → 𝑌 ∈ LMod)
16511adantr 484 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) → 𝑈:𝐼𝐵)
166 ffvelrn 6837 . . . . . . . . . . 11 ((𝑈:𝐼𝐵𝑥𝐼) → (𝑈𝑥) ∈ 𝐵)
167165, 154, 166syl2an 598 . . . . . . . . . 10 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → (𝑈𝑥) ∈ 𝐵)
1685, 102, 50, 132, 53lmod0vs 19660 . . . . . . . . . 10 ((𝑌 ∈ LMod ∧ (𝑈𝑥) ∈ 𝐵) → ((0g‘(Scalar‘𝑌))( ·𝑠𝑌)(𝑈𝑥)) = (0g𝑌))
169164, 167, 168syl2anc 587 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → ((0g‘(Scalar‘𝑌))( ·𝑠𝑌)(𝑈𝑥)) = (0g𝑌))
170157, 163, 1693eqtrd 2863 . . . . . . . 8 ((((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) ∧ 𝑥 ∈ (𝐼 ∖ (𝑦 supp 0 ))) → ((𝑦f ( ·𝑠𝑌)𝑈)‘𝑥) = (0g𝑌))
171150, 170suppss 7850 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐵) → ((𝑦f ( ·𝑠𝑌)𝑈) supp (0g𝑌)) ⊆ (𝑦 supp 0 ))
17249, 171syldan 594 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → ((𝑦f ( ·𝑠𝑌)𝑈) supp (0g𝑌)) ⊆ (𝑦 supp 0 ))
173148, 172ssfid 8732 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → ((𝑦f ( ·𝑠𝑌)𝑈) supp (0g𝑌)) ∈ Fin)
174 simp2 1134 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → 𝐼𝑉)
1751, 17, 5frlmbasmap 20896 . . . . . . . . . 10 ((𝐼𝑉𝑦𝐵) → 𝑦 ∈ ((Base‘𝑅) ↑m 𝐼))
176174, 83, 175syl2an 598 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑦 ∈ ((Base‘𝑅) ↑m 𝐼))
177 elmapfn 8419 . . . . . . . . 9 (𝑦 ∈ ((Base‘𝑅) ↑m 𝐼) → 𝑦 Fn 𝐼)
178176, 177syl 17 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑦 Fn 𝐼)
17911adantr 484 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑈:𝐼𝐵)
180179ffnd 6503 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑈 Fn 𝐼)
181178, 180, 46, 46, 71offn 7410 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (𝑦f ( ·𝑠𝑌)𝑈) Fn 𝐼)
182 fnfun 6441 . . . . . . 7 ((𝑦f ( ·𝑠𝑌)𝑈) Fn 𝐼 → Fun (𝑦f ( ·𝑠𝑌)𝑈))
183181, 182syl 17 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → Fun (𝑦f ( ·𝑠𝑌)𝑈))
184 ovexd 7180 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (𝑦f ( ·𝑠𝑌)𝑈) ∈ V)
185 fvexd 6673 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (0g𝑌) ∈ V)
186 funisfsupp 8829 . . . . . 6 ((Fun (𝑦f ( ·𝑠𝑌)𝑈) ∧ (𝑦f ( ·𝑠𝑌)𝑈) ∈ V ∧ (0g𝑌) ∈ V) → ((𝑦f ( ·𝑠𝑌)𝑈) finSupp (0g𝑌) ↔ ((𝑦f ( ·𝑠𝑌)𝑈) supp (0g𝑌)) ∈ Fin))
187183, 184, 185, 186syl3anc 1368 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → ((𝑦f ( ·𝑠𝑌)𝑈) finSupp (0g𝑌) ↔ ((𝑦f ( ·𝑠𝑌)𝑈) supp (0g𝑌)) ∈ Fin))
188173, 187mpbird 260 . . . 4 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (𝑦f ( ·𝑠𝑌)𝑈) finSupp (0g𝑌))
18953, 56, 46, 64, 145, 188gsumsubgcl 19036 . . 3 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → (𝑌 Σg (𝑦f ( ·𝑠𝑌)𝑈)) ∈ (𝐾‘(𝑈𝐽)))
19052, 189eqeltrd 2916 . 2 (((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) ∧ 𝑦𝐶) → 𝑦 ∈ (𝐾‘(𝑈𝐽)))
19144, 190eqelssd 3973 1 ((𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼) → (𝐾‘(𝑈𝐽)) = 𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  {crab 3137  Vcvv 3480   ∖ cdif 3916   ∩ cin 3918   ⊆ wss 3919  ∅c0 4275   class class class wbr 5052  dom cdm 5542  ran crn 5543   “ cima 5545  Fun wfun 6337   Fn wfn 6338  ⟶wf 6339  ‘cfv 6343  (class class class)co 7145   ∘f cof 7397   supp csupp 7820   ↑m cmap 8396  Fincfn 8499   finSupp cfsupp 8824  Basecbs 16479  Scalarcsca 16564   ·𝑠 cvsca 16565  0gc0g 16709   Σg cgsu 16710  SubGrpcsubg 18269  Abelcabl 18903  Ringcrg 19293  LModclmod 19627  LSubSpclss 19696  LSpanclspn 19736   freeLMod cfrlm 20883   unitVec cuvc 20919 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-tp 4554  df-op 4556  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7399  df-om 7571  df-1st 7679  df-2nd 7680  df-supp 7821  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-oadd 8096  df-er 8279  df-map 8398  df-ixp 8452  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-fsupp 8825  df-sup 8897  df-oi 8965  df-card 9359  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11693  df-3 11694  df-4 11695  df-5 11696  df-6 11697  df-7 11698  df-8 11699  df-9 11700  df-n0 11891  df-z 11975  df-dec 12092  df-uz 12237  df-fz 12891  df-fzo 13034  df-seq 13370  df-hash 13692  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-hom 16585  df-cco 16586  df-0g 16711  df-gsum 16712  df-prds 16717  df-pws 16719  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-mhm 17952  df-submnd 17953  df-grp 18102  df-minusg 18103  df-sbg 18104  df-mulg 18221  df-subg 18272  df-ghm 18352  df-cntz 18443  df-cmn 18904  df-abl 18905  df-mgp 19236  df-ur 19248  df-ring 19295  df-subrg 19526  df-lmod 19629  df-lss 19697  df-lsp 19737  df-lmhm 19787  df-sra 19937  df-rgmod 19938  df-dsmm 20869  df-frlm 20884  df-uvc 20920 This theorem is referenced by:  frlmlbs  20934
 Copyright terms: Public domain W3C validator