Step | Hyp | Ref
| Expression |
1 | | dmdprdpr.s |
. . . 4
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
2 | | dmdprdpr.t |
. . . 4
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
3 | | xpscf 17454 |
. . . 4
โข
({โจโ
, ๐โฉ, โจ1o, ๐โฉ}:2oโถ(SubGrpโ๐บ) โ (๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ))) |
4 | 1, 2, 3 | sylanbrc 584 |
. . 3
โข (๐ โ {โจโ
, ๐โฉ, โจ1o,
๐โฉ}:2oโถ(SubGrpโ๐บ)) |
5 | | 1n0 8439 |
. . . . 5
โข
1o โ โ
|
6 | 5 | necomi 2999 |
. . . 4
โข โ
โ 1o |
7 | | disjsn2 4678 |
. . . 4
โข (โ
โ 1o โ ({โ
} โฉ {1o}) =
โ
) |
8 | 6, 7 | mp1i 13 |
. . 3
โข (๐ โ ({โ
} โฉ
{1o}) = โ
) |
9 | | df2o3 8425 |
. . . . 5
โข
2o = {โ
, 1o} |
10 | | df-pr 4594 |
. . . . 5
โข {โ
,
1o} = ({โ
} โช {1o}) |
11 | 9, 10 | eqtri 2765 |
. . . 4
โข
2o = ({โ
} โช {1o}) |
12 | 11 | a1i 11 |
. . 3
โข (๐ โ 2o = ({โ
}
โช {1o})) |
13 | | dprdpr.s |
. . 3
โข โ =
(LSSumโ๐บ) |
14 | | dprdpr.1 |
. . . 4
โข (๐ โ ๐ โ (๐โ๐)) |
15 | | dprdpr.2 |
. . . 4
โข (๐ โ (๐ โฉ ๐) = { 0 }) |
16 | | dmdprdpr.z |
. . . . 5
โข ๐ = (Cntzโ๐บ) |
17 | | dmdprdpr.0 |
. . . . 5
โข 0 =
(0gโ๐บ) |
18 | 16, 17, 1, 2 | dmdprdpr 19835 |
. . . 4
โข (๐ โ (๐บdom DProd {โจโ
, ๐โฉ, โจ1o, ๐โฉ} โ (๐ โ (๐โ๐) โง (๐ โฉ ๐) = { 0 }))) |
19 | 14, 15, 18 | mpbir2and 712 |
. . 3
โข (๐ โ ๐บdom DProd {โจโ
, ๐โฉ, โจ1o, ๐โฉ}) |
20 | 4, 8, 12, 13, 19 | dprdsplit 19834 |
. 2
โข (๐ โ (๐บ DProd {โจโ
, ๐โฉ, โจ1o, ๐โฉ}) = ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โ
(๐บ DProd ({โจโ
,
๐โฉ,
โจ1o, ๐โฉ} โพ
{1o})))) |
21 | 4 | ffnd 6674 |
. . . . . . 7
โข (๐ โ {โจโ
, ๐โฉ, โจ1o,
๐โฉ} Fn
2o) |
22 | | 0ex 5269 |
. . . . . . . . 9
โข โ
โ V |
23 | 22 | prid1 4728 |
. . . . . . . 8
โข โ
โ {โ
, 1o} |
24 | 23, 9 | eleqtrri 2837 |
. . . . . . 7
โข โ
โ 2o |
25 | | fnressn 7109 |
. . . . . . 7
โข
(({โจโ
, ๐โฉ, โจ1o, ๐โฉ} Fn 2o โง
โ
โ 2o) โ ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}) =
{โจโ
, ({โจโ
, ๐โฉ, โจ1o, ๐โฉ}โโ
)โฉ}) |
26 | 21, 24, 25 | sylancl 587 |
. . . . . 6
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ {โ
})
= {โจโ
, ({โจโ
, ๐โฉ, โจ1o, ๐โฉ}โโ
)โฉ}) |
27 | | fvpr0o 17448 |
. . . . . . . . 9
โข (๐ โ (SubGrpโ๐บ) โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ}โโ
) =
๐) |
28 | 1, 27 | syl 17 |
. . . . . . . 8
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ}โโ
) =
๐) |
29 | 28 | opeq2d 4842 |
. . . . . . 7
โข (๐ โ โจโ
,
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ}โโ
)โฉ =
โจโ
, ๐โฉ) |
30 | 29 | sneqd 4603 |
. . . . . 6
โข (๐ โ {โจโ
,
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ}โโ
)โฉ} =
{โจโ
, ๐โฉ}) |
31 | 26, 30 | eqtrd 2777 |
. . . . 5
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ {โ
})
= {โจโ
, ๐โฉ}) |
32 | 31 | oveq2d 7378 |
. . . 4
โข (๐ โ (๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
})) =
(๐บ DProd {โจโ
,
๐โฉ})) |
33 | | dprdsn 19822 |
. . . . . 6
โข ((โ
โ V โง ๐ โ
(SubGrpโ๐บ)) โ
(๐บdom DProd {โจโ
,
๐โฉ} โง (๐บ DProd {โจโ
, ๐โฉ}) = ๐)) |
34 | 22, 1, 33 | sylancr 588 |
. . . . 5
โข (๐ โ (๐บdom DProd {โจโ
, ๐โฉ} โง (๐บ DProd {โจโ
, ๐โฉ}) = ๐)) |
35 | 34 | simprd 497 |
. . . 4
โข (๐ โ (๐บ DProd {โจโ
, ๐โฉ}) = ๐) |
36 | 32, 35 | eqtrd 2777 |
. . 3
โข (๐ โ (๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
})) =
๐) |
37 | | 1oex 8427 |
. . . . . . . . 9
โข
1o โ V |
38 | 37 | prid2 4729 |
. . . . . . . 8
โข
1o โ {โ
, 1o} |
39 | 38, 9 | eleqtrri 2837 |
. . . . . . 7
โข
1o โ 2o |
40 | | fnressn 7109 |
. . . . . . 7
โข
(({โจโ
, ๐โฉ, โจ1o, ๐โฉ} Fn 2o โง
1o โ 2o) โ ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {1o})
= {โจ1o, ({โจโ
, ๐โฉ, โจ1o, ๐โฉ}โ1o)โฉ}) |
41 | 21, 39, 40 | sylancl 587 |
. . . . . 6
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{1o}) = {โจ1o, ({โจโ
, ๐โฉ, โจ1o, ๐โฉ}โ1o)โฉ}) |
42 | | fvpr1o 17449 |
. . . . . . . . 9
โข (๐ โ (SubGrpโ๐บ) โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ}โ1o) = ๐) |
43 | 2, 42 | syl 17 |
. . . . . . . 8
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ}โ1o) = ๐) |
44 | 43 | opeq2d 4842 |
. . . . . . 7
โข (๐ โ โจ1o,
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ}โ1o)โฉ =
โจ1o, ๐โฉ) |
45 | 44 | sneqd 4603 |
. . . . . 6
โข (๐ โ {โจ1o,
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ}โ1o)โฉ} =
{โจ1o, ๐โฉ}) |
46 | 41, 45 | eqtrd 2777 |
. . . . 5
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{1o}) = {โจ1o, ๐โฉ}) |
47 | 46 | oveq2d 7378 |
. . . 4
โข (๐ โ (๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{1o})) = (๐บ
DProd {โจ1o, ๐โฉ})) |
48 | | 1on 8429 |
. . . . . 6
โข
1o โ On |
49 | | dprdsn 19822 |
. . . . . 6
โข
((1o โ On โง ๐ โ (SubGrpโ๐บ)) โ (๐บdom DProd {โจ1o, ๐โฉ} โง (๐บ DProd {โจ1o, ๐โฉ}) = ๐)) |
50 | 48, 2, 49 | sylancr 588 |
. . . . 5
โข (๐ โ (๐บdom DProd {โจ1o, ๐โฉ} โง (๐บ DProd {โจ1o, ๐โฉ}) = ๐)) |
51 | 50 | simprd 497 |
. . . 4
โข (๐ โ (๐บ DProd {โจ1o, ๐โฉ}) = ๐) |
52 | 47, 51 | eqtrd 2777 |
. . 3
โข (๐ โ (๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{1o})) = ๐) |
53 | 36, 52 | oveq12d 7380 |
. 2
โข (๐ โ ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โ
(๐บ DProd ({โจโ
,
๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = (๐ โ ๐)) |
54 | 20, 53 | eqtrd 2777 |
1
โข (๐ โ (๐บ DProd {โจโ
, ๐โฉ, โจ1o, ๐โฉ}) = (๐ โ ๐)) |