Step | Hyp | Ref
| Expression |
1 | | 0ex 5269 |
. . . . . 6
โข โ
โ V |
2 | | dmdprdpr.s |
. . . . . 6
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
3 | | dprdsn 19822 |
. . . . . 6
โข ((โ
โ V โง ๐ โ
(SubGrpโ๐บ)) โ
(๐บdom DProd {โจโ
,
๐โฉ} โง (๐บ DProd {โจโ
, ๐โฉ}) = ๐)) |
4 | 1, 2, 3 | sylancr 588 |
. . . . 5
โข (๐ โ (๐บdom DProd {โจโ
, ๐โฉ} โง (๐บ DProd {โจโ
, ๐โฉ}) = ๐)) |
5 | 4 | simpld 496 |
. . . 4
โข (๐ โ ๐บdom DProd {โจโ
, ๐โฉ}) |
6 | | dmdprdpr.t |
. . . . . . . 8
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
7 | | xpscf 17454 |
. . . . . . . 8
โข
({โจโ
, ๐โฉ, โจ1o, ๐โฉ}:2oโถ(SubGrpโ๐บ) โ (๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ))) |
8 | 2, 6, 7 | sylanbrc 584 |
. . . . . . 7
โข (๐ โ {โจโ
, ๐โฉ, โจ1o,
๐โฉ}:2oโถ(SubGrpโ๐บ)) |
9 | 8 | ffnd 6674 |
. . . . . 6
โข (๐ โ {โจโ
, ๐โฉ, โจ1o,
๐โฉ} Fn
2o) |
10 | 1 | prid1 4728 |
. . . . . . 7
โข โ
โ {โ
, 1o} |
11 | | df2o3 8425 |
. . . . . . 7
โข
2o = {โ
, 1o} |
12 | 10, 11 | eleqtrri 2837 |
. . . . . 6
โข โ
โ 2o |
13 | | fnressn 7109 |
. . . . . 6
โข
(({โจโ
, ๐โฉ, โจ1o, ๐โฉ} Fn 2o โง
โ
โ 2o) โ ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}) =
{โจโ
, ({โจโ
, ๐โฉ, โจ1o, ๐โฉ}โโ
)โฉ}) |
14 | 9, 12, 13 | sylancl 587 |
. . . . 5
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ {โ
})
= {โจโ
, ({โจโ
, ๐โฉ, โจ1o, ๐โฉ}โโ
)โฉ}) |
15 | | fvpr0o 17448 |
. . . . . . . 8
โข (๐ โ (SubGrpโ๐บ) โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ}โโ
) =
๐) |
16 | 2, 15 | syl 17 |
. . . . . . 7
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ}โโ
) =
๐) |
17 | 16 | opeq2d 4842 |
. . . . . 6
โข (๐ โ โจโ
,
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ}โโ
)โฉ =
โจโ
, ๐โฉ) |
18 | 17 | sneqd 4603 |
. . . . 5
โข (๐ โ {โจโ
,
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ}โโ
)โฉ} =
{โจโ
, ๐โฉ}) |
19 | 14, 18 | eqtrd 2777 |
. . . 4
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ {โ
})
= {โจโ
, ๐โฉ}) |
20 | 5, 19 | breqtrrd 5138 |
. . 3
โข (๐ โ ๐บdom DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{โ
})) |
21 | | 1on 8429 |
. . . . . 6
โข
1o โ On |
22 | | dprdsn 19822 |
. . . . . 6
โข
((1o โ On โง ๐ โ (SubGrpโ๐บ)) โ (๐บdom DProd {โจ1o, ๐โฉ} โง (๐บ DProd {โจ1o, ๐โฉ}) = ๐)) |
23 | 21, 6, 22 | sylancr 588 |
. . . . 5
โข (๐ โ (๐บdom DProd {โจ1o, ๐โฉ} โง (๐บ DProd {โจ1o, ๐โฉ}) = ๐)) |
24 | 23 | simpld 496 |
. . . 4
โข (๐ โ ๐บdom DProd {โจ1o, ๐โฉ}) |
25 | | 1oex 8427 |
. . . . . . . 8
โข
1o โ V |
26 | 25 | prid2 4729 |
. . . . . . 7
โข
1o โ {โ
, 1o} |
27 | 26, 11 | eleqtrri 2837 |
. . . . . 6
โข
1o โ 2o |
28 | | fnressn 7109 |
. . . . . 6
โข
(({โจโ
, ๐โฉ, โจ1o, ๐โฉ} Fn 2o โง
1o โ 2o) โ ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {1o})
= {โจ1o, ({โจโ
, ๐โฉ, โจ1o, ๐โฉ}โ1o)โฉ}) |
29 | 9, 27, 28 | sylancl 587 |
. . . . 5
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{1o}) = {โจ1o, ({โจโ
, ๐โฉ, โจ1o, ๐โฉ}โ1o)โฉ}) |
30 | | fvpr1o 17449 |
. . . . . . . 8
โข (๐ โ (SubGrpโ๐บ) โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ}โ1o) = ๐) |
31 | 6, 30 | syl 17 |
. . . . . . 7
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ}โ1o) = ๐) |
32 | 31 | opeq2d 4842 |
. . . . . 6
โข (๐ โ โจ1o,
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ}โ1o)โฉ =
โจ1o, ๐โฉ) |
33 | 32 | sneqd 4603 |
. . . . 5
โข (๐ โ {โจ1o,
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ}โ1o)โฉ} =
{โจ1o, ๐โฉ}) |
34 | 29, 33 | eqtrd 2777 |
. . . 4
โข (๐ โ ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{1o}) = {โจ1o, ๐โฉ}) |
35 | 24, 34 | breqtrrd 5138 |
. . 3
โข (๐ โ ๐บdom DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{1o})) |
36 | | 1n0 8439 |
. . . . . . . . 9
โข
1o โ โ
|
37 | 36 | necomi 2999 |
. . . . . . . 8
โข โ
โ 1o |
38 | | disjsn2 4678 |
. . . . . . . 8
โข (โ
โ 1o โ ({โ
} โฉ {1o}) =
โ
) |
39 | 37, 38 | mp1i 13 |
. . . . . . 7
โข (๐ โ ({โ
} โฉ
{1o}) = โ
) |
40 | | df-pr 4594 |
. . . . . . . . 9
โข {โ
,
1o} = ({โ
} โช {1o}) |
41 | 11, 40 | eqtri 2765 |
. . . . . . . 8
โข
2o = ({โ
} โช {1o}) |
42 | 41 | a1i 11 |
. . . . . . 7
โข (๐ โ 2o = ({โ
}
โช {1o})) |
43 | | dmdprdpr.z |
. . . . . . 7
โข ๐ = (Cntzโ๐บ) |
44 | | dmdprdpr.0 |
. . . . . . 7
โข 0 =
(0gโ๐บ) |
45 | 8, 39, 42, 43, 44 | dmdprdsplit 19833 |
. . . . . 6
โข (๐ โ (๐บdom DProd {โจโ
, ๐โฉ, โจ1o, ๐โฉ} โ ((๐บdom DProd ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ {โ
})
โง ๐บdom DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o})) โง
(๐บ DProd ({โจโ
,
๐โฉ,
โจ1o, ๐โฉ} โพ {โ
})) โ (๐โ(๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{1o}))) โง ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โฉ (๐บ DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = { 0
}))) |
46 | | 3anass 1096 |
. . . . . 6
โข (((๐บdom DProd ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ {โ
})
โง ๐บdom DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o})) โง
(๐บ DProd ({โจโ
,
๐โฉ,
โจ1o, ๐โฉ} โพ {โ
})) โ (๐โ(๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{1o}))) โง ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โฉ (๐บ DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = { 0 }) โ
((๐บdom DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {โ
}) โง ๐บdom DProd ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{1o})) โง ((๐บ
DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โ (๐โ(๐บ DProd ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{1o}))) โง ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โฉ (๐บ DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = { 0
}))) |
47 | 45, 46 | bitrdi 287 |
. . . . 5
โข (๐ โ (๐บdom DProd {โจโ
, ๐โฉ, โจ1o, ๐โฉ} โ ((๐บdom DProd ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ {โ
})
โง ๐บdom DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o})) โง
((๐บ DProd ({โจโ
,
๐โฉ,
โจ1o, ๐โฉ} โพ {โ
})) โ (๐โ(๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{1o}))) โง ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โฉ (๐บ DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = { 0
})))) |
48 | 47 | baibd 541 |
. . . 4
โข ((๐ โง (๐บdom DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}) โง
๐บdom DProd ({โจโ
,
๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) โ
(๐บdom DProd {โจโ
,
๐โฉ,
โจ1o, ๐โฉ} โ ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โ (๐โ(๐บ DProd ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{1o}))) โง ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โฉ (๐บ DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = { 0
}))) |
49 | 48 | ex 414 |
. . 3
โข (๐ โ ((๐บdom DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}) โง
๐บdom DProd ({โจโ
,
๐โฉ,
โจ1o, ๐โฉ} โพ {1o})) โ
(๐บdom DProd {โจโ
,
๐โฉ,
โจ1o, ๐โฉ} โ ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โ (๐โ(๐บ DProd ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{1o}))) โง ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โฉ (๐บ DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = { 0
})))) |
50 | 20, 35, 49 | mp2and 698 |
. 2
โข (๐ โ (๐บdom DProd {โจโ
, ๐โฉ, โจ1o, ๐โฉ} โ ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{โ
})) โ (๐โ(๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{1o}))) โง ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โฉ (๐บ DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = { 0
}))) |
51 | 19 | oveq2d 7378 |
. . . . 5
โข (๐ โ (๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
})) =
(๐บ DProd {โจโ
,
๐โฉ})) |
52 | 4 | simprd 497 |
. . . . 5
โข (๐ โ (๐บ DProd {โจโ
, ๐โฉ}) = ๐) |
53 | 51, 52 | eqtrd 2777 |
. . . 4
โข (๐ โ (๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
})) =
๐) |
54 | 34 | oveq2d 7378 |
. . . . . 6
โข (๐ โ (๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{1o})) = (๐บ
DProd {โจ1o, ๐โฉ})) |
55 | 23 | simprd 497 |
. . . . . 6
โข (๐ โ (๐บ DProd {โจ1o, ๐โฉ}) = ๐) |
56 | 54, 55 | eqtrd 2777 |
. . . . 5
โข (๐ โ (๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{1o})) = ๐) |
57 | 56 | fveq2d 6851 |
. . . 4
โข (๐ โ (๐โ(๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ
{1o}))) = (๐โ๐)) |
58 | 53, 57 | sseq12d 3982 |
. . 3
โข (๐ โ ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โ (๐โ(๐บ DProd ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{1o}))) โ ๐
โ (๐โ๐))) |
59 | 53, 56 | ineq12d 4178 |
. . . 4
โข (๐ โ ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โฉ (๐บ DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = (๐ โฉ ๐)) |
60 | 59 | eqeq1d 2739 |
. . 3
โข (๐ โ (((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โฉ (๐บ DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = { 0 } โ
(๐ โฉ ๐) = { 0 })) |
61 | 58, 60 | anbi12d 632 |
. 2
โข (๐ โ (((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โ (๐โ(๐บ DProd ({โจโ
, ๐โฉ, โจ1o,
๐โฉ} โพ
{1o}))) โง ((๐บ DProd ({โจโ
, ๐โฉ, โจ1o, ๐โฉ} โพ {โ
}))
โฉ (๐บ DProd
({โจโ
, ๐โฉ,
โจ1o, ๐โฉ} โพ {1o}))) = { 0 }) โ
(๐ โ (๐โ๐) โง (๐ โฉ ๐) = { 0 }))) |
62 | 50, 61 | bitrd 279 |
1
โข (๐ โ (๐บdom DProd {โจโ
, ๐โฉ, โจ1o, ๐โฉ} โ (๐ โ (๐โ๐) โง (๐ โฉ ๐) = { 0 }))) |