Metamath Proof Explorer

Theorem issubg4

Description: A subgroup is a nonempty subset of the group closed under subtraction. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypotheses issubg4.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
issubg4.p ⊢ − = ( -g ‘ 𝐺 )
Assertion issubg4 ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 issubg4.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 issubg4.p ⊢ − = ( -g ‘ 𝐺 )
3 1 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )
4 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5 4 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
6 5 ne0d ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ≠ ∅ )
7 2 subgsubcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 − 𝑦 ) ∈ 𝑆 )
8 7 3expb ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 − 𝑦 ) ∈ 𝑆 )
9 8 ralrimivva ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 )
10 3 6 9 3jca ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) )
11 simplrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
12 simplrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → 𝑆 ≠ ∅ )
13 oveq1 ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( 𝑥 − 𝑦 ) = ( ( 0g ‘ 𝐺 ) − 𝑦 ) )
14 13 eleq1d ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( ( 𝑥 − 𝑦 ) ∈ 𝑆 ↔ ( ( 0g ‘ 𝐺 ) − 𝑦 ) ∈ 𝑆 ) )
15 14 ralbidv ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ↔ ∀ 𝑦 ∈ 𝑆 ( ( 0g ‘ 𝐺 ) − 𝑦 ) ∈ 𝑆 ) )
16 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 )
17 simprr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ≠ ∅ )
18 r19.2z ⊢ ( ( 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 )
19 17 18 sylan ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 )
20 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑥 − 𝑦 ) = ( 𝑥 − 𝑥 ) )
21 20 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 − 𝑦 ) ∈ 𝑆 ↔ ( 𝑥 − 𝑥 ) ∈ 𝑆 ) )
22 21 rspcv ⊢ ( 𝑥 ∈ 𝑆 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ( 𝑥 − 𝑥 ) ∈ 𝑆 ) )
23 22 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ( 𝑥 − 𝑥 ) ∈ 𝑆 ) )
24 simprl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ⊆ 𝐵 )
25 24 sselda ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
26 1 4 2 grpsubid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 − 𝑥 ) = ( 0g ‘ 𝐺 ) )
27 26 adantlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 − 𝑥 ) = ( 0g ‘ 𝐺 ) )
28 25 27 syldan ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 − 𝑥 ) = ( 0g ‘ 𝐺 ) )
29 28 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 − 𝑥 ) ∈ 𝑆 ↔ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) )
30 23 29 sylibd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ( 0g ‘ 𝐺 ) ∈ 𝑆 ) )
31 30 rexlimdva ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ( 0g ‘ 𝐺 ) ∈ 𝑆 ) )
32 31 imp ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
33 19 32 syldan ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
34 15 16 33 rspcdva ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( ( 0g ‘ 𝐺 ) − 𝑦 ) ∈ 𝑆 )
35 1 4 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
36 35 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
37 24 sselda ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝐵 )
38 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
39 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
40 1 38 39 2 grpsubval ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) − 𝑦 ) = ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
41 36 37 40 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) − 𝑦 ) = ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
42 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝐺 ∈ Grp )
43 1 39 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝐵 )
44 42 37 43 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝐵 )
45 1 38 4 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) )
46 42 44 45 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) )
47 41 46 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) − 𝑦 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) )
48 47 eleq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 0g ‘ 𝐺 ) − 𝑦 ) ∈ 𝑆 ↔ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) )
49 48 ralbidva ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) → ( ∀ 𝑦 ∈ 𝑆 ( ( 0g ‘ 𝐺 ) − 𝑦 ) ∈ 𝑆 ↔ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) )
50 49 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑆 ( ( 0g ‘ 𝐺 ) − 𝑦 ) ∈ 𝑆 ↔ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) )
51 34 50 mpbid ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 )
52 fveq2 ⊢ ( 𝑦 = 𝑧 → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) )
53 52 eleq1d ⊢ ( 𝑦 = 𝑧 → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ↔ ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 ) )
54 53 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 )
55 54 ad2ant2l ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 )
56 oveq2 ⊢ ( 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) → ( 𝑥 − 𝑦 ) = ( 𝑥 − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
57 56 eleq1d ⊢ ( 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) → ( ( 𝑥 − 𝑦 ) ∈ 𝑆 ↔ ( 𝑥 − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
58 57 rspcv ⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ( 𝑥 − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
59 55 58 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ( 𝑥 − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
60 simplll ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝐺 ∈ Grp )
61 simplrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
62 61 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑆 ⊆ 𝐵 )
63 simprl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑥 ∈ 𝑆 )
64 62 63 sseldd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑥 ∈ 𝐵 )
65 simprr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ 𝑆 )
66 62 65 sseldd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ 𝐵 )
67 1 38 2 39 60 64 66 grpsubinv ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑥 − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) )
68 67 eleq1d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ↔ ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) )
69 59 68 sylibd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) )
70 69 anassrs ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) )
71 70 ralrimdva ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ∀ 𝑧 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) )
72 71 ralimdva ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) )
73 72 impancom ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) )
74 51 73 mpd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 )
75 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) )
76 75 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) )
77 76 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑧 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ↔ ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) )
78 77 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ↔ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 )
79 74 78 sylib ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 )
80 r19.26 ⊢ ( ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ↔ ( ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) )
81 79 51 80 sylanbrc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) )
82 11 12 81 3jca ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ) )
83 82 exp42 ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ⊆ 𝐵 → ( 𝑆 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 → ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ) ) ) ) )
84 83 3impd ⊢ ( 𝐺 ∈ Grp → ( ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ) ) )
85 1 38 39 issubg2 ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝑆 ( ∀ 𝑧 ∈ 𝑆 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑆 ) ) ) )
86 84 85 sylibrd ⊢ ( 𝐺 ∈ Grp → ( ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) )
87 10 86 impbid2 ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 − 𝑦 ) ∈ 𝑆 ) ) )