Step | Hyp | Ref
| Expression |
1 | | pj1eu.2 |
. . . 4
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
2 | | pj1eu.3 |
. . . 4
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
3 | | pj1eu.a |
. . . . 5
โข + =
(+gโ๐บ) |
4 | | pj1eu.s |
. . . . 5
โข โ =
(LSSumโ๐บ) |
5 | 3, 4 | lsmelval 19439 |
. . . 4
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ)) โ (๐ โ (๐ โ ๐) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ))) |
6 | 1, 2, 5 | syl2anc 585 |
. . 3
โข (๐ โ (๐ โ (๐ โ ๐) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ))) |
7 | 6 | biimpa 478 |
. 2
โข ((๐ โง ๐ โ (๐ โ ๐)) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ)) |
8 | | reeanv 3216 |
. . . . 5
โข
(โ๐ฆ โ
๐ โ๐ฃ โ ๐ (๐ = (๐ฅ + ๐ฆ) โง ๐ = (๐ข + ๐ฃ)) โ (โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ) โง โ๐ฃ โ ๐ ๐ = (๐ข + ๐ฃ))) |
9 | | eqtr2 2757 |
. . . . . . 7
โข ((๐ = (๐ฅ + ๐ฆ) โง ๐ = (๐ข + ๐ฃ)) โ (๐ฅ + ๐ฆ) = (๐ข + ๐ฃ)) |
10 | | pj1eu.o |
. . . . . . . . 9
โข 0 =
(0gโ๐บ) |
11 | | pj1eu.z |
. . . . . . . . 9
โข ๐ = (Cntzโ๐บ) |
12 | 1 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ ๐ โ (SubGrpโ๐บ)) |
13 | 2 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ ๐ โ (SubGrpโ๐บ)) |
14 | | pj1eu.4 |
. . . . . . . . . 10
โข (๐ โ (๐ โฉ ๐) = { 0 }) |
15 | 14 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ (๐ โฉ ๐) = { 0 }) |
16 | | pj1eu.5 |
. . . . . . . . . 10
โข (๐ โ ๐ โ (๐โ๐)) |
17 | 16 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ ๐ โ (๐โ๐)) |
18 | | simplrl 776 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ ๐ฅ โ ๐) |
19 | | simplrr 777 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ ๐ข โ ๐) |
20 | | simprl 770 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ ๐ฆ โ ๐) |
21 | | simprr 772 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ ๐ฃ โ ๐) |
22 | 3, 10, 11, 12, 13, 15, 17, 18, 19, 20, 21 | subgdisjb 19483 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ ((๐ฅ + ๐ฆ) = (๐ข + ๐ฃ) โ (๐ฅ = ๐ข โง ๐ฆ = ๐ฃ))) |
23 | | simpl 484 |
. . . . . . . 8
โข ((๐ฅ = ๐ข โง ๐ฆ = ๐ฃ) โ ๐ฅ = ๐ข) |
24 | 22, 23 | syl6bi 253 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ ((๐ฅ + ๐ฆ) = (๐ข + ๐ฃ) โ ๐ฅ = ๐ข)) |
25 | 9, 24 | syl5 34 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โง (๐ฆ โ ๐ โง ๐ฃ โ ๐)) โ ((๐ = (๐ฅ + ๐ฆ) โง ๐ = (๐ข + ๐ฃ)) โ ๐ฅ = ๐ข)) |
26 | 25 | rexlimdvva 3202 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โ (โ๐ฆ โ ๐ โ๐ฃ โ ๐ (๐ = (๐ฅ + ๐ฆ) โง ๐ = (๐ข + ๐ฃ)) โ ๐ฅ = ๐ข)) |
27 | 8, 26 | biimtrrid 242 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ โง ๐ข โ ๐)) โ ((โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ) โง โ๐ฃ โ ๐ ๐ = (๐ข + ๐ฃ)) โ ๐ฅ = ๐ข)) |
28 | 27 | ralrimivva 3194 |
. . 3
โข (๐ โ โ๐ฅ โ ๐ โ๐ข โ ๐ ((โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ) โง โ๐ฃ โ ๐ ๐ = (๐ข + ๐ฃ)) โ ๐ฅ = ๐ข)) |
29 | 28 | adantr 482 |
. 2
โข ((๐ โง ๐ โ (๐ โ ๐)) โ โ๐ฅ โ ๐ โ๐ข โ ๐ ((โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ) โง โ๐ฃ โ ๐ ๐ = (๐ข + ๐ฃ)) โ ๐ฅ = ๐ข)) |
30 | | oveq1 7368 |
. . . . . 6
โข (๐ฅ = ๐ข โ (๐ฅ + ๐ฆ) = (๐ข + ๐ฆ)) |
31 | 30 | eqeq2d 2744 |
. . . . 5
โข (๐ฅ = ๐ข โ (๐ = (๐ฅ + ๐ฆ) โ ๐ = (๐ข + ๐ฆ))) |
32 | 31 | rexbidv 3172 |
. . . 4
โข (๐ฅ = ๐ข โ (โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ) โ โ๐ฆ โ ๐ ๐ = (๐ข + ๐ฆ))) |
33 | | oveq2 7369 |
. . . . . 6
โข (๐ฆ = ๐ฃ โ (๐ข + ๐ฆ) = (๐ข + ๐ฃ)) |
34 | 33 | eqeq2d 2744 |
. . . . 5
โข (๐ฆ = ๐ฃ โ (๐ = (๐ข + ๐ฆ) โ ๐ = (๐ข + ๐ฃ))) |
35 | 34 | cbvrexvw 3225 |
. . . 4
โข
(โ๐ฆ โ
๐ ๐ = (๐ข + ๐ฆ) โ โ๐ฃ โ ๐ ๐ = (๐ข + ๐ฃ)) |
36 | 32, 35 | bitrdi 287 |
. . 3
โข (๐ฅ = ๐ข โ (โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ) โ โ๐ฃ โ ๐ ๐ = (๐ข + ๐ฃ))) |
37 | 36 | reu4 3693 |
. 2
โข
(โ!๐ฅ โ
๐ โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ) โ (โ๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ) โง โ๐ฅ โ ๐ โ๐ข โ ๐ ((โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ) โง โ๐ฃ โ ๐ ๐ = (๐ข + ๐ฃ)) โ ๐ฅ = ๐ข))) |
38 | 7, 29, 37 | sylanbrc 584 |
1
โข ((๐ โง ๐ โ (๐ โ ๐)) โ โ!๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ)) |