Step | Hyp | Ref
| Expression |
1 | | subgrcl 12970 |
. . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
2 | | eqger.r |
. . . 4
⊢ ∼ =
(𝐺 ~QG
𝑌) |
3 | 2 | releqgg 13011 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ (SubGrp‘𝐺)) → Rel ∼ ) |
4 | 1, 3 | mpancom 422 |
. 2
⊢ (𝑌 ∈ (SubGrp‘𝐺) → Rel ∼ ) |
5 | | eqger.x |
. . . . . . 7
⊢ 𝑋 = (Base‘𝐺) |
6 | 5 | subgss 12965 |
. . . . . 6
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) |
7 | | eqid 2177 |
. . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) |
8 | | eqid 2177 |
. . . . . . 7
⊢
(+g‘𝐺) = (+g‘𝐺) |
9 | 5, 7, 8, 2 | eqgval 13013 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑌))) |
10 | 1, 6, 9 | syl2anc 411 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑌))) |
11 | 10 | biimpa 296 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑌)) |
12 | 11 | simp2d 1010 |
. . 3
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → 𝑦 ∈ 𝑋) |
13 | 11 | simp1d 1009 |
. . 3
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → 𝑥 ∈ 𝑋) |
14 | 1 | adantr 276 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → 𝐺 ∈ Grp) |
15 | 5, 7 | grpinvcl 12853 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → ((invg‘𝐺)‘𝑥) ∈ 𝑋) |
16 | 14, 13, 15 | syl2anc 411 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → ((invg‘𝐺)‘𝑥) ∈ 𝑋) |
17 | 5, 8, 7 | grpinvadd 12880 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝑥) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)) = (((invg‘𝐺)‘𝑦)(+g‘𝐺)((invg‘𝐺)‘((invg‘𝐺)‘𝑥)))) |
18 | 14, 16, 12, 17 | syl3anc 1238 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → ((invg‘𝐺)‘(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)) = (((invg‘𝐺)‘𝑦)(+g‘𝐺)((invg‘𝐺)‘((invg‘𝐺)‘𝑥)))) |
19 | 5, 7 | grpinvinv 12869 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑥)) = 𝑥) |
20 | 14, 13, 19 | syl2anc 411 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → ((invg‘𝐺)‘((invg‘𝐺)‘𝑥)) = 𝑥) |
21 | 20 | oveq2d 5888 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → (((invg‘𝐺)‘𝑦)(+g‘𝐺)((invg‘𝐺)‘((invg‘𝐺)‘𝑥))) = (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑥)) |
22 | 18, 21 | eqtrd 2210 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → ((invg‘𝐺)‘(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)) = (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑥)) |
23 | 11 | simp3d 1011 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑌) |
24 | 7 | subginvcl 12974 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧
(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑌) → ((invg‘𝐺)‘(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)) ∈ 𝑌) |
25 | 23, 24 | syldan 282 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → ((invg‘𝐺)‘(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)) ∈ 𝑌) |
26 | 22, 25 | eqeltrrd 2255 |
. . 3
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑥) ∈ 𝑌) |
27 | 6 | adantr 276 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → 𝑌 ⊆ 𝑋) |
28 | 5, 7, 8, 2 | eqgval 13013 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → (𝑦 ∼ 𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑥) ∈ 𝑌))) |
29 | 14, 27, 28 | syl2anc 411 |
. . 3
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → (𝑦 ∼ 𝑥 ↔ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑥) ∈ 𝑌))) |
30 | 12, 13, 26, 29 | mpbir3and 1180 |
. 2
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∼ 𝑦) → 𝑦 ∼ 𝑥) |
31 | 13 | adantrr 479 |
. . 3
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑥 ∈ 𝑋) |
32 | 5, 7, 8, 2 | eqgval 13013 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌))) |
33 | 1, 6, 32 | syl2anc 411 |
. . . . . 6
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌))) |
34 | 33 | biimpa 296 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑦 ∼ 𝑧) → (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌)) |
35 | 34 | adantrl 478 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌)) |
36 | 35 | simp2d 1010 |
. . 3
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑧 ∈ 𝑋) |
37 | 1 | adantr 276 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝐺 ∈ Grp) |
38 | 37, 31, 15 | syl2anc 411 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → ((invg‘𝐺)‘𝑥) ∈ 𝑋) |
39 | 12 | adantrr 479 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑦 ∈ 𝑋) |
40 | 5, 7 | grpinvcl 12853 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
41 | 37, 39, 40 | syl2anc 411 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
42 | 5, 8, 37, 41, 36 | grpcld 12822 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑋) |
43 | 5, 8 | grpass 12818 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑥) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑋)) → ((((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = (((invg‘𝐺)‘𝑥)(+g‘𝐺)(𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)))) |
44 | 37, 38, 39, 42, 43 | syl13anc 1240 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → ((((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = (((invg‘𝐺)‘𝑥)(+g‘𝐺)(𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)))) |
45 | | eqid 2177 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
46 | 5, 8, 45, 7 | grprinv 12855 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑦)) = (0g‘𝐺)) |
47 | 37, 39, 46 | syl2anc 411 |
. . . . . . . 8
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑦(+g‘𝐺)((invg‘𝐺)‘𝑦)) = (0g‘𝐺)) |
48 | 47 | oveq1d 5887 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → ((𝑦(+g‘𝐺)((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) = ((0g‘𝐺)(+g‘𝐺)𝑧)) |
49 | 5, 8 | grpass 12818 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑦 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝑦) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦(+g‘𝐺)((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) = (𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) |
50 | 37, 39, 41, 36, 49 | syl13anc 1240 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → ((𝑦(+g‘𝐺)((invg‘𝐺)‘𝑦))(+g‘𝐺)𝑧) = (𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) |
51 | 5, 8, 45 | grplid 12838 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((0g‘𝐺)(+g‘𝐺)𝑧) = 𝑧) |
52 | 37, 36, 51 | syl2anc 411 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → ((0g‘𝐺)(+g‘𝐺)𝑧) = 𝑧) |
53 | 48, 50, 52 | 3eqtr3d 2218 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = 𝑧) |
54 | 53 | oveq2d 5888 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (((invg‘𝐺)‘𝑥)(+g‘𝐺)(𝑦(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧))) = (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑧)) |
55 | 44, 54 | eqtrd 2210 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → ((((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) = (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑧)) |
56 | | simpl 109 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑌 ∈ (SubGrp‘𝐺)) |
57 | 23 | adantrr 479 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑌) |
58 | 35 | simp3d 1011 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) |
59 | 8 | subgcl 12975 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧
(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑌 ∧ (((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧) ∈ 𝑌) → ((((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑌) |
60 | 56, 57, 58, 59 | syl3anc 1238 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → ((((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)(+g‘𝐺)(((invg‘𝐺)‘𝑦)(+g‘𝐺)𝑧)) ∈ 𝑌) |
61 | 55, 60 | eqeltrrd 2255 |
. . 3
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑧) ∈ 𝑌) |
62 | 6 | adantr 276 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑌 ⊆ 𝑋) |
63 | 5, 7, 8, 2 | eqgval 13013 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑧) ∈ 𝑌))) |
64 | 37, 62, 63 | syl2anc 411 |
. . 3
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑧) ∈ 𝑌))) |
65 | 31, 36, 61, 64 | mpbir3and 1180 |
. 2
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧)) → 𝑥 ∼ 𝑧) |
66 | 5, 8, 45, 7 | grplinv 12854 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) = (0g‘𝐺)) |
67 | 1, 66 | sylan 283 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) = (0g‘𝐺)) |
68 | 45 | subg0cl 12973 |
. . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑌) |
69 | 68 | adantr 276 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (0g‘𝐺) ∈ 𝑌) |
70 | 67, 69 | eqeltrd 2254 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌) |
71 | 70 | ex 115 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ 𝑋 → (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌)) |
72 | 71 | pm4.71rd 394 |
. . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ 𝑋 ↔ ((((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌 ∧ 𝑥 ∈ 𝑋))) |
73 | 5, 7, 8, 2 | eqgval 13013 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∼ 𝑥 ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌))) |
74 | 1, 6, 73 | syl2anc 411 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∼ 𝑥 ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌))) |
75 | | df-3an 980 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌)) |
76 | | anidm 396 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) ↔ 𝑥 ∈ 𝑋) |
77 | 76 | anbi2ci 459 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌) ↔ ((((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌 ∧ 𝑥 ∈ 𝑋)) |
78 | 75, 77 | bitri 184 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌) ↔ ((((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌 ∧ 𝑥 ∈ 𝑋)) |
79 | 74, 78 | bitrdi 196 |
. . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∼ 𝑥 ↔ ((((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑥) ∈ 𝑌 ∧ 𝑥 ∈ 𝑋))) |
80 | 72, 79 | bitr4d 191 |
. 2
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∼ 𝑥)) |
81 | 4, 30, 65, 80 | iserd 6558 |
1
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |