Metamath Proof Explorer

Theorem subgint

Description: The intersection of a nonempty collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Assertion subgint ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 intssuni ⊢ ( 𝑆 ≠ ∅ → ∩ 𝑆 ⊆ ∪ 𝑆 )
2 1 adantl ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ⊆ ∪ 𝑆 )
3 ssel2 ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑔 ∈ 𝑆 ) → 𝑔 ∈ ( SubGrp ‘ 𝐺 ) )
4 3 adantlr ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑔 ∈ ( SubGrp ‘ 𝐺 ) )
5 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 5 subgss ⊢ ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) → 𝑔 ⊆ ( Base ‘ 𝐺 ) )
7 4 6 syl ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑔 ∈ 𝑆 ) → 𝑔 ⊆ ( Base ‘ 𝐺 ) )
8 7 ralrimiva ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ∀ 𝑔 ∈ 𝑆 𝑔 ⊆ ( Base ‘ 𝐺 ) )
9 unissb ⊢ ( ∪ 𝑆 ⊆ ( Base ‘ 𝐺 ) ↔ ∀ 𝑔 ∈ 𝑆 𝑔 ⊆ ( Base ‘ 𝐺 ) )
10 8 9 sylibr ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ∪ 𝑆 ⊆ ( Base ‘ 𝐺 ) )
11 2 10 sstrd ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ⊆ ( Base ‘ 𝐺 ) )
12 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
13 12 subg0cl ⊢ ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑔 )
14 4 13 syl ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑔 ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ 𝑔 )
15 14 ralrimiva ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ∀ 𝑔 ∈ 𝑆 ( 0g ‘ 𝐺 ) ∈ 𝑔 )
16 fvex ⊢ ( 0g ‘ 𝐺 ) ∈ V
17 16 elint2 ⊢ ( ( 0g ‘ 𝐺 ) ∈ ∩ 𝑆 ↔ ∀ 𝑔 ∈ 𝑆 ( 0g ‘ 𝐺 ) ∈ 𝑔 )
18 15 17 sylibr ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ( 0g ‘ 𝐺 ) ∈ ∩ 𝑆 )
19 18 ne0d ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ≠ ∅ )
20 4 adantlr ⊢ ( ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑔 ∈ 𝑆 ) → 𝑔 ∈ ( SubGrp ‘ 𝐺 ) )
21 simprl ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → 𝑥 ∈ ∩ 𝑆 )
22 elinti ⊢ ( 𝑥 ∈ ∩ 𝑆 → ( 𝑔 ∈ 𝑆 → 𝑥 ∈ 𝑔 ) )
23 22 imp ⊢ ( ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑔 ∈ 𝑆 ) → 𝑥 ∈ 𝑔 )
24 21 23 sylan ⊢ ( ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑔 ∈ 𝑆 ) → 𝑥 ∈ 𝑔 )
25 simprr ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → 𝑦 ∈ ∩ 𝑆 )
26 elinti ⊢ ( 𝑦 ∈ ∩ 𝑆 → ( 𝑔 ∈ 𝑆 → 𝑦 ∈ 𝑔 ) )
27 26 imp ⊢ ( ( 𝑦 ∈ ∩ 𝑆 ∧ 𝑔 ∈ 𝑆 ) → 𝑦 ∈ 𝑔 )
28 25 27 sylan ⊢ ( ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑔 ∈ 𝑆 ) → 𝑦 ∈ 𝑔 )
29 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
30 29 subgcl ⊢ ( ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑔 ∧ 𝑦 ∈ 𝑔 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑔 )
31 20 24 28 30 syl3anc ⊢ ( ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑔 ∈ 𝑆 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑔 )
32 31 ralrimiva ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → ∀ 𝑔 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑔 )
33 ovex ⊢ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ V
34 33 elint2 ⊢ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ∩ 𝑆 ↔ ∀ 𝑔 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑔 )
35 32 34 sylibr ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ∩ 𝑆 )
36 35 anassrs ⊢ ( ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝑆 ) ∧ 𝑦 ∈ ∩ 𝑆 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ∩ 𝑆 )
37 36 ralrimiva ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝑆 ) → ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ∩ 𝑆 )
38 4 adantlr ⊢ ( ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝑆 ) ∧ 𝑔 ∈ 𝑆 ) → 𝑔 ∈ ( SubGrp ‘ 𝐺 ) )
39 23 adantll ⊢ ( ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝑆 ) ∧ 𝑔 ∈ 𝑆 ) → 𝑥 ∈ 𝑔 )
40 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
41 40 subginvcl ⊢ ( ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑔 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑔 )
42 38 39 41 syl2anc ⊢ ( ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝑆 ) ∧ 𝑔 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑔 )
43 42 ralrimiva ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝑆 ) → ∀ 𝑔 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑔 )
44 fvex ⊢ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ V
45 44 elint2 ⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ∩ 𝑆 ↔ ∀ 𝑔 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑔 )
46 43 45 sylibr ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ∩ 𝑆 )
47 37 46 jca ⊢ ( ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝑆 ) → ( ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ∩ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ∩ 𝑆 ) )
48 47 ralrimiva ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ∀ 𝑥 ∈ ∩ 𝑆 ( ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ∩ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ∩ 𝑆 ) )
49 ssn0 ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ( SubGrp ‘ 𝐺 ) ≠ ∅ )
50 n0 ⊢ ( ( SubGrp ‘ 𝐺 ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( SubGrp ‘ 𝐺 ) )
51 subgrcl ⊢ ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
52 51 exlimiv ⊢ ( ∃ 𝑔 𝑔 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
53 50 52 sylbi ⊢ ( ( SubGrp ‘ 𝐺 ) ≠ ∅ → 𝐺 ∈ Grp )
54 5 29 40 issubg2 ⊢ ( 𝐺 ∈ Grp → ( ∩ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ∩ 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ∩ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ ∩ 𝑆 ( ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ∩ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ∩ 𝑆 ) ) ) )
55 49 53 54 3syl ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ( ∩ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ∩ 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ∩ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ ∩ 𝑆 ( ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ∩ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ∩ 𝑆 ) ) ) )
56 11 19 48 55 mpbir3and ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )