Step | Hyp | Ref
| Expression |
1 | | pi1fval.g |
. . . . 5
⊢ 𝐺 = (𝐽 π1 𝑌) |
2 | | pi1fval.3 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
3 | | pi1fval.4 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑋) |
4 | | eqid 2610 |
. . . . 5
⊢ (𝐽 Ω1 𝑌) = (𝐽 Ω1 𝑌) |
5 | 1, 2, 3, 4 | pi1val 22645 |
. . . 4
⊢ (𝜑 → 𝐺 = ((𝐽 Ω1 𝑌) /s (
≃ph‘𝐽))) |
6 | | pi1fval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) |
8 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (Base‘(𝐽 Ω1 𝑌)) = (Base‘(𝐽 Ω1 𝑌))) |
9 | 1, 2, 3, 4, 7, 8 | pi1buni 22648 |
. . . 4
⊢ (𝜑 → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
10 | | fvex 6113 |
. . . . 5
⊢ (
≃ph‘𝐽) ∈ V |
11 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 → (
≃ph‘𝐽) ∈ V) |
12 | | ovex 6577 |
. . . . 5
⊢ (𝐽 Ω1 𝑌) ∈ V |
13 | 12 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐽 Ω1 𝑌) ∈ V) |
14 | 1, 2, 3, 4, 7, 9 | pi1blem 22647 |
. . . . 5
⊢ (𝜑 → (((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵
∧ ∪ 𝐵 ⊆ (II Cn 𝐽))) |
15 | 14 | simpld 474 |
. . . 4
⊢ (𝜑 → ((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵) |
16 | 5, 9, 11, 13, 15 | qusin 16027 |
. . 3
⊢ (𝜑 → 𝐺 = ((𝐽 Ω1 𝑌) /s ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)))) |
17 | 4, 2, 3 | om1plusg 22642 |
. . 3
⊢ (𝜑 →
(*𝑝‘𝐽) = (+g‘(𝐽 Ω1 𝑌))) |
18 | | phtpcer 22602 |
. . . . 5
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → (
≃ph‘𝐽) Er (II Cn 𝐽)) |
20 | 14 | simprd 478 |
. . . 4
⊢ (𝜑 → ∪ 𝐵
⊆ (II Cn 𝐽)) |
21 | 19, 20 | erinxp 7708 |
. . 3
⊢ (𝜑 → ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
Er ∪ 𝐵) |
22 | | eqid 2610 |
. . . . 5
⊢ ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)) |
23 | | eqid 2610 |
. . . . 5
⊢
(+g‘(𝐽 Ω1 𝑌)) = (+g‘(𝐽 Ω1 𝑌)) |
24 | 1, 2, 3, 7, 22, 4,
23 | pi1cpbl 22652 |
. . . 4
⊢ (𝜑 → ((𝑎(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑐 ∧ 𝑏(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑑) → (𝑎(+g‘(𝐽 Ω1 𝑌))𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(+g‘(𝐽 Ω1 𝑌))𝑑))) |
25 | 17 | oveqd 6566 |
. . . . 5
⊢ (𝜑 → (𝑎(*𝑝‘𝐽)𝑏) = (𝑎(+g‘(𝐽 Ω1 𝑌))𝑏)) |
26 | 17 | oveqd 6566 |
. . . . 5
⊢ (𝜑 → (𝑐(*𝑝‘𝐽)𝑑) = (𝑐(+g‘(𝐽 Ω1 𝑌))𝑑)) |
27 | 25, 26 | breq12d 4596 |
. . . 4
⊢ (𝜑 → ((𝑎(*𝑝‘𝐽)𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(*𝑝‘𝐽)𝑑) ↔ (𝑎(+g‘(𝐽 Ω1 𝑌))𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(+g‘(𝐽 Ω1 𝑌))𝑑))) |
28 | 24, 27 | sylibrd 248 |
. . 3
⊢ (𝜑 → ((𝑎(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑐 ∧ 𝑏(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑑) → (𝑎(*𝑝‘𝐽)𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(*𝑝‘𝐽)𝑑))) |
29 | 2 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝐽 ∈ (TopOn‘𝑋)) |
30 | 3 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝑌 ∈ 𝑋) |
31 | 9 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
32 | | simp2 1055 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝑥 ∈ ∪ 𝐵) |
33 | | simp3 1056 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝑦 ∈ ∪ 𝐵) |
34 | 4, 29, 30, 31, 32, 33 | om1addcl 22641 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → (𝑥(*𝑝‘𝐽)𝑦) ∈ ∪ 𝐵) |
35 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝐽 ∈ (TopOn‘𝑋)) |
36 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑌 ∈ 𝑋) |
37 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
38 | 34 | 3adant3r3 1268 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥(*𝑝‘𝐽)𝑦) ∈ ∪ 𝐵) |
39 | | simpr3 1062 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑧 ∈ ∪ 𝐵) |
40 | 4, 35, 36, 37, 38, 39 | om1addcl 22641 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧) ∈ ∪ 𝐵) |
41 | | simpr1 1060 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑥 ∈ ∪ 𝐵) |
42 | | simpr2 1061 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑦 ∈ ∪ 𝐵) |
43 | 4, 35, 36, 37, 42, 39 | om1addcl 22641 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦(*𝑝‘𝐽)𝑧) ∈ ∪ 𝐵) |
44 | 4, 35, 36, 37, 41, 43 | om1addcl 22641 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)) ∈ ∪ 𝐵) |
45 | 1, 2, 3, 7 | pi1eluni 22650 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐵 ↔ (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌 ∧ (𝑥‘1) = 𝑌))) |
46 | 45 | biimpa 500 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌 ∧ (𝑥‘1) = 𝑌)) |
47 | 46 | 3ad2antr1 1219 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌 ∧ (𝑥‘1) = 𝑌)) |
48 | 47 | simp1d 1066 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑥 ∈ (II Cn 𝐽)) |
49 | 6 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝐵 = (Base‘𝐺)) |
50 | 1, 35, 36, 49 | pi1eluni 22650 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦 ∈ ∪ 𝐵 ↔ (𝑦 ∈ (II Cn 𝐽) ∧ (𝑦‘0) = 𝑌 ∧ (𝑦‘1) = 𝑌))) |
51 | 42, 50 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦 ∈ (II Cn 𝐽) ∧ (𝑦‘0) = 𝑌 ∧ (𝑦‘1) = 𝑌)) |
52 | 51 | simp1d 1066 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑦 ∈ (II Cn 𝐽)) |
53 | 1, 35, 36, 49 | pi1eluni 22650 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑧 ∈ ∪ 𝐵 ↔ (𝑧 ∈ (II Cn 𝐽) ∧ (𝑧‘0) = 𝑌 ∧ (𝑧‘1) = 𝑌))) |
54 | 39, 53 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑧 ∈ (II Cn 𝐽) ∧ (𝑧‘0) = 𝑌 ∧ (𝑧‘1) = 𝑌)) |
55 | 54 | simp1d 1066 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑧 ∈ (II Cn 𝐽)) |
56 | 47 | simp3d 1068 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥‘1) = 𝑌) |
57 | 51 | simp2d 1067 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦‘0) = 𝑌) |
58 | 56, 57 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥‘1) = (𝑦‘0)) |
59 | 51 | simp3d 1068 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦‘1) = 𝑌) |
60 | 54 | simp2d 1067 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑧‘0) = 𝑌) |
61 | 59, 60 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦‘1) = (𝑧‘0)) |
62 | | eqid 2610 |
. . . . 5
⊢ (𝑢 ∈ (0[,]1) ↦ if(𝑢 ≤ (1 / 2), if(𝑢 ≤ (1 / 4), (2 · 𝑢), (𝑢 + (1 / 4))), ((𝑢 / 2) + (1 / 2)))) = (𝑢 ∈ (0[,]1) ↦ if(𝑢 ≤ (1 / 2), if(𝑢 ≤ (1 / 4), (2 · 𝑢), (𝑢 + (1 / 4))), ((𝑢 / 2) + (1 / 2)))) |
63 | 48, 52, 55, 58, 61, 62 | pcoass 22632 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)( ≃ph‘𝐽)(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧))) |
64 | | brinxp2 5103 |
. . . 4
⊢ (((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)) ↔ (((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧) ∈ ∪ 𝐵 ∧ (𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)) ∈ ∪ 𝐵 ∧ ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)( ≃ph‘𝐽)(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)))) |
65 | 40, 44, 63, 64 | syl3anbrc 1239 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧))) |
66 | | pi1grplem.z |
. . . . . 6
⊢ 0 = ((0[,]1)
× {𝑌}) |
67 | 66 | pcoptcl 22629 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝑋) → ( 0 ∈ (II Cn 𝐽) ∧ ( 0 ‘0) = 𝑌 ∧ ( 0 ‘1) = 𝑌)) |
68 | 2, 3, 67 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ( 0 ∈ (II Cn 𝐽) ∧ ( 0 ‘0) = 𝑌 ∧ ( 0 ‘1) = 𝑌)) |
69 | 1, 2, 3, 7 | pi1eluni 22650 |
. . . 4
⊢ (𝜑 → ( 0 ∈ ∪ 𝐵
↔ ( 0 ∈ (II Cn 𝐽) ∧ ( 0 ‘0) = 𝑌 ∧ ( 0 ‘1) = 𝑌))) |
70 | 68, 69 | mpbird 246 |
. . 3
⊢ (𝜑 → 0 ∈ ∪ 𝐵) |
71 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝐽 ∈ (TopOn‘𝑋)) |
72 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝑌 ∈ 𝑋) |
73 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
74 | 70 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 0 ∈ ∪ 𝐵) |
75 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝑥 ∈ ∪ 𝐵) |
76 | 4, 71, 72, 73, 74, 75 | om1addcl 22641 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ( 0
(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵) |
77 | 20 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝑥 ∈ (II Cn 𝐽)) |
78 | 46 | simp2d 1067 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑥‘0) = 𝑌) |
79 | 66 | pcopt 22630 |
. . . . 5
⊢ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌) → ( 0
(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)𝑥) |
80 | 77, 78, 79 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ( 0
(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)𝑥) |
81 | | brinxp2 5103 |
. . . 4
⊢ (( 0
(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑥 ↔ (( 0
(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵 ∧ 𝑥 ∈ ∪ 𝐵 ∧ ( 0
(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)𝑥)) |
82 | 76, 75, 80, 81 | syl3anbrc 1239 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ( 0
(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑥) |
83 | | eqid 2610 |
. . . . . . 7
⊢ (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) = (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) |
84 | 83 | pcorevcl 22633 |
. . . . . 6
⊢ (𝑥 ∈ (II Cn 𝐽) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = (𝑥‘1) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = (𝑥‘0))) |
85 | 77, 84 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = (𝑥‘1) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = (𝑥‘0))) |
86 | 85 | simp1d 1066 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽)) |
87 | 85 | simp2d 1067 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = (𝑥‘1)) |
88 | 46 | simp3d 1068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑥‘1) = 𝑌) |
89 | 87, 88 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = 𝑌) |
90 | 85 | simp3d 1068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = (𝑥‘0)) |
91 | 90, 78 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = 𝑌) |
92 | 1, 2, 3, 7 | pi1eluni 22650 |
. . . . 5
⊢ (𝜑 → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ ∪ 𝐵 ↔ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = 𝑌 ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = 𝑌))) |
93 | 92 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ ∪ 𝐵 ↔ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = 𝑌 ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = 𝑌))) |
94 | 86, 89, 91, 93 | mpbir3and 1238 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ ∪ 𝐵) |
95 | 4, 71, 72, 73, 94, 75 | om1addcl 22641 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵) |
96 | | eqid 2610 |
. . . . . . 7
⊢ ((0[,]1)
× {(𝑥‘1)}) =
((0[,]1) × {(𝑥‘1)}) |
97 | 83, 96 | pcorev 22635 |
. . . . . 6
⊢ (𝑥 ∈ (II Cn 𝐽) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)((0[,]1) × {(𝑥‘1)})) |
98 | 77, 97 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)((0[,]1) × {(𝑥‘1)})) |
99 | 88 | sneqd 4137 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → {(𝑥‘1)} = {𝑌}) |
100 | 99 | xpeq2d 5063 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((0[,]1) ×
{(𝑥‘1)}) = ((0[,]1)
× {𝑌})) |
101 | 100, 66 | syl6reqr 2663 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 0 = ((0[,]1) × {(𝑥‘1)})) |
102 | 98, 101 | breqtrrd 4611 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽) 0 ) |
103 | | brinxp2 5103 |
. . . 4
⊢ (((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)) 0 ↔ (((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵 ∧ 0 ∈ ∪ 𝐵
∧ ((𝑎 ∈ (0[,]1)
↦ (𝑥‘(1 −
𝑎)))(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽) 0 )) |
104 | 95, 74, 102, 103 | syl3anbrc 1239 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)) 0 ) |
105 | 16, 9, 17, 21, 13, 28, 34, 65, 70, 82, 94, 104 | qusgrp2 17356 |
. 2
⊢ (𝜑 → (𝐺 ∈ Grp ∧ [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (0g‘𝐺))) |
106 | | ecinxp 7709 |
. . . . 5
⊢ ((((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵
∧ 0
∈ ∪ 𝐵) → [ 0 ](
≃ph‘𝐽) = [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))) |
107 | 15, 70, 106 | syl2anc 691 |
. . . 4
⊢ (𝜑 → [ 0 ](
≃ph‘𝐽) = [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))) |
108 | 107 | eqeq1d 2612 |
. . 3
⊢ (𝜑 → ([ 0 ](
≃ph‘𝐽) = (0g‘𝐺) ↔ [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (0g‘𝐺))) |
109 | 108 | anbi2d 736 |
. 2
⊢ (𝜑 → ((𝐺 ∈ Grp ∧ [ 0 ](
≃ph‘𝐽) = (0g‘𝐺)) ↔ (𝐺 ∈ Grp ∧ [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (0g‘𝐺)))) |
110 | 105, 109 | mpbird 246 |
1
⊢ (𝜑 → (𝐺 ∈ Grp ∧ [ 0 ](
≃ph‘𝐽) = (0g‘𝐺))) |