Step | Hyp | Ref
| Expression |
1 | | pi1fval.g |
. . . . 5
⊢ 𝐺 = (𝐽 π1 𝑌) |
2 | | pi1fval.3 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
3 | | pi1fval.4 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑋) |
4 | | eqid 2737 |
. . . . 5
⊢ (𝐽 Ω1 𝑌) = (𝐽 Ω1 𝑌) |
5 | 1, 2, 3, 4 | pi1val 23934 |
. . . 4
⊢ (𝜑 → 𝐺 = ((𝐽 Ω1 𝑌) /s (
≃ph‘𝐽))) |
6 | | pi1fval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) |
8 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (Base‘(𝐽 Ω1 𝑌)) = (Base‘(𝐽 Ω1 𝑌))) |
9 | 1, 2, 3, 4, 7, 8 | pi1buni 23937 |
. . . 4
⊢ (𝜑 → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
10 | | fvexd 6732 |
. . . 4
⊢ (𝜑 → (
≃ph‘𝐽) ∈ V) |
11 | | ovexd 7248 |
. . . 4
⊢ (𝜑 → (𝐽 Ω1 𝑌) ∈ V) |
12 | 1, 2, 3, 4, 7, 9 | pi1blem 23936 |
. . . . 5
⊢ (𝜑 → (((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵
∧ ∪ 𝐵 ⊆ (II Cn 𝐽))) |
13 | 12 | simpld 498 |
. . . 4
⊢ (𝜑 → ((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵) |
14 | 5, 9, 10, 11, 13 | qusin 17049 |
. . 3
⊢ (𝜑 → 𝐺 = ((𝐽 Ω1 𝑌) /s ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)))) |
15 | 4, 2, 3 | om1plusg 23931 |
. . 3
⊢ (𝜑 →
(*𝑝‘𝐽) = (+g‘(𝐽 Ω1 𝑌))) |
16 | | phtpcer 23892 |
. . . . 5
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |
17 | 16 | a1i 11 |
. . . 4
⊢ (𝜑 → (
≃ph‘𝐽) Er (II Cn 𝐽)) |
18 | 12 | simprd 499 |
. . . 4
⊢ (𝜑 → ∪ 𝐵
⊆ (II Cn 𝐽)) |
19 | 17, 18 | erinxp 8473 |
. . 3
⊢ (𝜑 → ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
Er ∪ 𝐵) |
20 | | eqid 2737 |
. . . . 5
⊢ ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)) |
21 | | eqid 2737 |
. . . . 5
⊢
(+g‘(𝐽 Ω1 𝑌)) = (+g‘(𝐽 Ω1 𝑌)) |
22 | 1, 2, 3, 7, 20, 4,
21 | pi1cpbl 23941 |
. . . 4
⊢ (𝜑 → ((𝑎(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑐 ∧ 𝑏(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑑) → (𝑎(+g‘(𝐽 Ω1 𝑌))𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(+g‘(𝐽 Ω1 𝑌))𝑑))) |
23 | 15 | oveqd 7230 |
. . . . 5
⊢ (𝜑 → (𝑎(*𝑝‘𝐽)𝑏) = (𝑎(+g‘(𝐽 Ω1 𝑌))𝑏)) |
24 | 15 | oveqd 7230 |
. . . . 5
⊢ (𝜑 → (𝑐(*𝑝‘𝐽)𝑑) = (𝑐(+g‘(𝐽 Ω1 𝑌))𝑑)) |
25 | 23, 24 | breq12d 5066 |
. . . 4
⊢ (𝜑 → ((𝑎(*𝑝‘𝐽)𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(*𝑝‘𝐽)𝑑) ↔ (𝑎(+g‘(𝐽 Ω1 𝑌))𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(+g‘(𝐽 Ω1 𝑌))𝑑))) |
26 | 22, 25 | sylibrd 262 |
. . 3
⊢ (𝜑 → ((𝑎(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑐 ∧ 𝑏(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑑) → (𝑎(*𝑝‘𝐽)𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(*𝑝‘𝐽)𝑑))) |
27 | 2 | 3ad2ant1 1135 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝐽 ∈ (TopOn‘𝑋)) |
28 | 3 | 3ad2ant1 1135 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝑌 ∈ 𝑋) |
29 | 9 | 3ad2ant1 1135 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
30 | | simp2 1139 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝑥 ∈ ∪ 𝐵) |
31 | | simp3 1140 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝑦 ∈ ∪ 𝐵) |
32 | 4, 27, 28, 29, 30, 31 | om1addcl 23930 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → (𝑥(*𝑝‘𝐽)𝑦) ∈ ∪ 𝐵) |
33 | 2 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝐽 ∈ (TopOn‘𝑋)) |
34 | 3 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑌 ∈ 𝑋) |
35 | 9 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
36 | 32 | 3adant3r3 1186 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥(*𝑝‘𝐽)𝑦) ∈ ∪ 𝐵) |
37 | | simpr3 1198 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑧 ∈ ∪ 𝐵) |
38 | 4, 33, 34, 35, 36, 37 | om1addcl 23930 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧) ∈ ∪ 𝐵) |
39 | | simpr1 1196 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑥 ∈ ∪ 𝐵) |
40 | | simpr2 1197 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑦 ∈ ∪ 𝐵) |
41 | 4, 33, 34, 35, 40, 37 | om1addcl 23930 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦(*𝑝‘𝐽)𝑧) ∈ ∪ 𝐵) |
42 | 4, 33, 34, 35, 39, 41 | om1addcl 23930 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)) ∈ ∪ 𝐵) |
43 | 1, 2, 3, 7 | pi1eluni 23939 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐵 ↔ (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌 ∧ (𝑥‘1) = 𝑌))) |
44 | 43 | biimpa 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌 ∧ (𝑥‘1) = 𝑌)) |
45 | 44 | 3ad2antr1 1190 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌 ∧ (𝑥‘1) = 𝑌)) |
46 | 45 | simp1d 1144 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑥 ∈ (II Cn 𝐽)) |
47 | 6 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝐵 = (Base‘𝐺)) |
48 | 1, 33, 34, 47 | pi1eluni 23939 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦 ∈ ∪ 𝐵 ↔ (𝑦 ∈ (II Cn 𝐽) ∧ (𝑦‘0) = 𝑌 ∧ (𝑦‘1) = 𝑌))) |
49 | 40, 48 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦 ∈ (II Cn 𝐽) ∧ (𝑦‘0) = 𝑌 ∧ (𝑦‘1) = 𝑌)) |
50 | 49 | simp1d 1144 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑦 ∈ (II Cn 𝐽)) |
51 | 1, 33, 34, 47 | pi1eluni 23939 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑧 ∈ ∪ 𝐵 ↔ (𝑧 ∈ (II Cn 𝐽) ∧ (𝑧‘0) = 𝑌 ∧ (𝑧‘1) = 𝑌))) |
52 | 37, 51 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑧 ∈ (II Cn 𝐽) ∧ (𝑧‘0) = 𝑌 ∧ (𝑧‘1) = 𝑌)) |
53 | 52 | simp1d 1144 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑧 ∈ (II Cn 𝐽)) |
54 | 45 | simp3d 1146 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥‘1) = 𝑌) |
55 | 49 | simp2d 1145 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦‘0) = 𝑌) |
56 | 54, 55 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥‘1) = (𝑦‘0)) |
57 | 49 | simp3d 1146 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦‘1) = 𝑌) |
58 | 52 | simp2d 1145 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑧‘0) = 𝑌) |
59 | 57, 58 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦‘1) = (𝑧‘0)) |
60 | | eqid 2737 |
. . . . 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)))) |
61 | 46, 50, 53, 56, 59, 60 | pcoass 23921 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)( ≃ph‘𝐽)(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧))) |
62 | | brinxp2 5626 |
. . . 4
⊢ (((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)) ↔ ((((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧) ∈ ∪ 𝐵 ∧ (𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)) ∈ ∪ 𝐵) ∧ ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)( ≃ph‘𝐽)(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)))) |
63 | 38, 42, 61, 62 | syl21anbrc 1346 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧))) |
64 | | pi1grplem.z |
. . . . . 6
⊢ 0 = ((0[,]1)
× {𝑌}) |
65 | 64 | pcoptcl 23918 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝑋) → ( 0 ∈ (II Cn 𝐽) ∧ ( 0 ‘0) = 𝑌 ∧ ( 0 ‘1) = 𝑌)) |
66 | 2, 3, 65 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ( 0 ∈ (II Cn 𝐽) ∧ ( 0 ‘0) = 𝑌 ∧ ( 0 ‘1) = 𝑌)) |
67 | 1, 2, 3, 7 | pi1eluni 23939 |
. . . 4
⊢ (𝜑 → ( 0 ∈ ∪ 𝐵
↔ ( 0 ∈ (II Cn 𝐽) ∧ ( 0 ‘0) = 𝑌 ∧ ( 0 ‘1) = 𝑌))) |
68 | 66, 67 | mpbird 260 |
. . 3
⊢ (𝜑 → 0 ∈ ∪ 𝐵) |
69 | 2 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝐽 ∈ (TopOn‘𝑋)) |
70 | 3 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝑌 ∈ 𝑋) |
71 | 9 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
72 | 68 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 0 ∈ ∪ 𝐵) |
73 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝑥 ∈ ∪ 𝐵) |
74 | 4, 69, 70, 71, 72, 73 | om1addcl 23930 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ( 0
(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵) |
75 | 18 | sselda 3901 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝑥 ∈ (II Cn 𝐽)) |
76 | 44 | simp2d 1145 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑥‘0) = 𝑌) |
77 | 64 | pcopt 23919 |
. . . . 5
⊢ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌) → ( 0
(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)𝑥) |
78 | 75, 76, 77 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ( 0
(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)𝑥) |
79 | | brinxp2 5626 |
. . . 4
⊢ (( 0
(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑥 ↔ ((( 0
(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵 ∧ 𝑥 ∈ ∪ 𝐵) ∧ ( 0
(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)𝑥)) |
80 | 74, 73, 78, 79 | syl21anbrc 1346 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ( 0
(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑥) |
81 | | eqid 2737 |
. . . . . . 7
⊢ (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) = (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) |
82 | 81 | pcorevcl 23922 |
. . . . . 6
⊢ (𝑥 ∈ (II Cn 𝐽) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = (𝑥‘1) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = (𝑥‘0))) |
83 | 75, 82 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = (𝑥‘1) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = (𝑥‘0))) |
84 | 83 | simp1d 1144 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽)) |
85 | 83 | simp2d 1145 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = (𝑥‘1)) |
86 | 44 | simp3d 1146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑥‘1) = 𝑌) |
87 | 85, 86 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = 𝑌) |
88 | 83 | simp3d 1146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = (𝑥‘0)) |
89 | 88, 76 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = 𝑌) |
90 | 1, 2, 3, 7 | pi1eluni 23939 |
. . . . 5
⊢ (𝜑 → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ ∪ 𝐵 ↔ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = 𝑌 ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = 𝑌))) |
91 | 90 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ ∪ 𝐵 ↔ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = 𝑌 ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = 𝑌))) |
92 | 84, 87, 89, 91 | mpbir3and 1344 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ ∪ 𝐵) |
93 | 4, 69, 70, 71, 92, 73 | om1addcl 23930 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵) |
94 | | eqid 2737 |
. . . . . . 7
⊢ ((0[,]1)
× {(𝑥‘1)}) =
((0[,]1) × {(𝑥‘1)}) |
95 | 81, 94 | pcorev 23924 |
. . . . . 6
⊢ (𝑥 ∈ (II Cn 𝐽) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)((0[,]1) × {(𝑥‘1)})) |
96 | 75, 95 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)((0[,]1) × {(𝑥‘1)})) |
97 | 86 | sneqd 4553 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → {(𝑥‘1)} = {𝑌}) |
98 | 97 | xpeq2d 5581 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((0[,]1) ×
{(𝑥‘1)}) = ((0[,]1)
× {𝑌})) |
99 | 64, 98 | eqtr4id 2797 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 0 = ((0[,]1) × {(𝑥‘1)})) |
100 | 96, 99 | breqtrrd 5081 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽) 0 ) |
101 | | brinxp2 5626 |
. . . 4
⊢ (((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)) 0 ↔ ((((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵 ∧ 0 ∈ ∪ 𝐵)
∧ ((𝑎 ∈ (0[,]1)
↦ (𝑥‘(1 −
𝑎)))(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽) 0 )) |
102 | 93, 72, 100, 101 | syl21anbrc 1346 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)) 0 ) |
103 | 14, 9, 15, 19, 11, 26, 32, 63, 68, 80, 92, 102 | qusgrp2 18481 |
. 2
⊢ (𝜑 → (𝐺 ∈ Grp ∧ [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (0g‘𝐺))) |
104 | | ecinxp 8474 |
. . . . 5
⊢ ((((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵
∧ 0
∈ ∪ 𝐵) → [ 0 ](
≃ph‘𝐽) = [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))) |
105 | 13, 68, 104 | syl2anc 587 |
. . . 4
⊢ (𝜑 → [ 0 ](
≃ph‘𝐽) = [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))) |
106 | 105 | eqeq1d 2739 |
. . 3
⊢ (𝜑 → ([ 0 ](
≃ph‘𝐽) = (0g‘𝐺) ↔ [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (0g‘𝐺))) |
107 | 106 | anbi2d 632 |
. 2
⊢ (𝜑 → ((𝐺 ∈ Grp ∧ [ 0 ](
≃ph‘𝐽) = (0g‘𝐺)) ↔ (𝐺 ∈ Grp ∧ [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (0g‘𝐺)))) |
108 | 103, 107 | mpbird 260 |
1
⊢ (𝜑 → (𝐺 ∈ Grp ∧ [ 0 ](
≃ph‘𝐽) = (0g‘𝐺))) |