Theorem lidlsubg 13770

Description: An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.)

Hypothesis

Ref	Expression
lidlcl.u	⊢ 𝑈 = (LIdeal‘𝑅)

Assertion

Ref	Expression
lidlsubg	⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝐼 ∈ (SubGrp‘𝑅))

Proof of Theorem lidlsubg

Dummy variables 𝑥 𝑗 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2189	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		lidlcl.u	. . . 4 ⊢ 𝑈 = (LIdeal‘𝑅)
3	1, 2	lidlss 13760	. . 3 ⊢ (𝐼 ∈ 𝑈 → 𝐼 ⊆ (Base‘𝑅))
4	3	adantl 277	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝐼 ⊆ (Base‘𝑅))
5		eqid 2189	. . . 4 ⊢ (0g‘𝑅) = (0g‘𝑅)
6	2, 5	lidl0cl 13767	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (0g‘𝑅) ∈ 𝐼)
7		elex2 2768	. . 3 ⊢ ((0g‘𝑅) ∈ 𝐼 → ∃𝑗 𝑗 ∈ 𝐼)
8	6, 7	syl 14	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → ∃𝑗 𝑗 ∈ 𝐼)
9		eqid 2189	. . . . . . 7 ⊢ (+g‘𝑅) = (+g‘𝑅)
10	2, 9	lidlacl 13768	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼)) → (𝑥(+g‘𝑅)𝑦) ∈ 𝐼)
11	10	anassrs 400	. . . . 5 ⊢ ((((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐼) → (𝑥(+g‘𝑅)𝑦) ∈ 𝐼)
12	11	ralrimiva 2563	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ 𝐼) → ∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼)
13		eqid 2189	. . . . . 6 ⊢ (invg‘𝑅) = (invg‘𝑅)
14	2, 13	lidlnegcl 13769	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑥 ∈ 𝐼) → ((invg‘𝑅)‘𝑥) ∈ 𝐼)
15	14	3expa 1205	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ 𝐼) → ((invg‘𝑅)‘𝑥) ∈ 𝐼)
16	12, 15	jca 306	. . 3 ⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ 𝐼) → (∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐼))
17	16	ralrimiva 2563	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐼))
18		ringgrp 13323	. . . 4 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
19	18	adantr 276	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝑅 ∈ Grp)
20	1, 9, 13	issubg2m 13101	. . 3 ⊢ (𝑅 ∈ Grp → (𝐼 ∈ (SubGrp‘𝑅) ↔ (𝐼 ⊆ (Base‘𝑅) ∧ ∃𝑗 𝑗 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐼))))
21	19, 20	syl 14	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐼 ∈ (SubGrp‘𝑅) ↔ (𝐼 ⊆ (Base‘𝑅) ∧ ∃𝑗 𝑗 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐼))))
22	4, 8, 17, 21	mpbir3and 1182	1 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → 𝐼 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 980   = wceq 1364  ∃wex 1503   ∈ wcel 2160  ∀wral 2468   ⊆ wss 3144  ‘cfv 5232  (class class class)co 5892  Basecbs 12487  +_gcplusg 12562  0_gc0g 12734  Grpcgrp 12918  inv_gcminusg 12919  SubGrpcsubg 13079  Ringcrg 13318  LIdealclidl 13751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-cnex 7922  ax-resscn 7923  ax-1cn 7924  ax-1re 7925  ax-icn 7926  ax-addcl 7927  ax-addrcl 7928  ax-mulcl 7929  ax-addcom 7931  ax-addass 7933  ax-i2m1 7936  ax-0lt1 7937  ax-0id 7939  ax-rnegex 7940  ax-pre-ltirr 7943  ax-pre-lttrn 7945  ax-pre-ltadd 7947

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5234  df-fn 5235  df-f 5236  df-f1 5237  df-fo 5238  df-f1o 5239  df-fv 5240  df-riota 5848  df-ov 5895  df-oprab 5896  df-mpo 5897  df-1st 6160  df-2nd 6161  df-pnf 8014  df-mnf 8015  df-ltxr 8017  df-inn 8940  df-2 8998  df-3 8999  df-4 9000  df-5 9001  df-6 9002  df-7 9003  df-8 9004  df-ndx 12490  df-slot 12491  df-base 12493  df-sets 12494  df-iress 12495  df-plusg 12575  df-mulr 12576  df-sca 12578  df-vsca 12579  df-ip 12580  df-0g 12736  df-mgm 12805  df-sgrp 12838  df-mnd 12851  df-grp 12921  df-minusg 12922  df-sbg 12923  df-subg 13082  df-mgp 13243  df-ur 13282  df-ring 13320  df-subrg 13534  df-lmod 13573  df-lssm 13637  df-sra 13719  df-rgmod 13720  df-lidl 13753

This theorem is referenced by:  lidlsubcl  13771  dflidl2  13772  df2idl2  13792  2idlcpbl  13807  qus1  13809  qusmul2  13811  quscrng  13815