| 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 25070 |
. . . 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 25073 |
. . . 4
⊢ (𝜑 → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
| 10 | | fvexd 6921 |
. . . 4
⊢ (𝜑 → (
≃ph‘𝐽) ∈ V) |
| 11 | | ovexd 7466 |
. . . 4
⊢ (𝜑 → (𝐽 Ω1 𝑌) ∈ V) |
| 12 | 1, 2, 3, 4, 7, 9 | pi1blem 25072 |
. . . . 5
⊢ (𝜑 → (((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵
∧ ∪ 𝐵 ⊆ (II Cn 𝐽))) |
| 13 | 12 | simpld 494 |
. . . 4
⊢ (𝜑 → ((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵) |
| 14 | 5, 9, 10, 11, 13 | qusin 17589 |
. . 3
⊢ (𝜑 → 𝐺 = ((𝐽 Ω1 𝑌) /s ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)))) |
| 15 | 4, 2, 3 | om1plusg 25067 |
. . 3
⊢ (𝜑 →
(*𝑝‘𝐽) = (+g‘(𝐽 Ω1 𝑌))) |
| 16 | | phtpcer 25027 |
. . . . 5
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |
| 17 | 16 | a1i 11 |
. . . 4
⊢ (𝜑 → (
≃ph‘𝐽) Er (II Cn 𝐽)) |
| 18 | 12 | simprd 495 |
. . . 4
⊢ (𝜑 → ∪ 𝐵
⊆ (II Cn 𝐽)) |
| 19 | 17, 18 | erinxp 8831 |
. . 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 25077 |
. . . 4
⊢ (𝜑 → ((𝑎(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑐 ∧ 𝑏(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑑) → (𝑎(+g‘(𝐽 Ω1 𝑌))𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(+g‘(𝐽 Ω1 𝑌))𝑑))) |
| 23 | 15 | oveqd 7448 |
. . . . 5
⊢ (𝜑 → (𝑎(*𝑝‘𝐽)𝑏) = (𝑎(+g‘(𝐽 Ω1 𝑌))𝑏)) |
| 24 | 15 | oveqd 7448 |
. . . . 5
⊢ (𝜑 → (𝑐(*𝑝‘𝐽)𝑑) = (𝑐(+g‘(𝐽 Ω1 𝑌))𝑑)) |
| 25 | 23, 24 | breq12d 5156 |
. . . 4
⊢ (𝜑 → ((𝑎(*𝑝‘𝐽)𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(*𝑝‘𝐽)𝑑) ↔ (𝑎(+g‘(𝐽 Ω1 𝑌))𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(+g‘(𝐽 Ω1 𝑌))𝑑))) |
| 26 | 22, 25 | sylibrd 259 |
. . 3
⊢ (𝜑 → ((𝑎(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑐 ∧ 𝑏(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑑) → (𝑎(*𝑝‘𝐽)𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(*𝑝‘𝐽)𝑑))) |
| 27 | 2 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝐽 ∈ (TopOn‘𝑋)) |
| 28 | 3 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝑌 ∈ 𝑋) |
| 29 | 9 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
| 30 | | simp2 1138 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝑥 ∈ ∪ 𝐵) |
| 31 | | simp3 1139 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → 𝑦 ∈ ∪ 𝐵) |
| 32 | 4, 27, 28, 29, 30, 31 | om1addcl 25066 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵) → (𝑥(*𝑝‘𝐽)𝑦) ∈ ∪ 𝐵) |
| 33 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝐽 ∈ (TopOn‘𝑋)) |
| 34 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑌 ∈ 𝑋) |
| 35 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
| 36 | 32 | 3adant3r3 1185 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥(*𝑝‘𝐽)𝑦) ∈ ∪ 𝐵) |
| 37 | | simpr3 1197 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑧 ∈ ∪ 𝐵) |
| 38 | 4, 33, 34, 35, 36, 37 | om1addcl 25066 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧) ∈ ∪ 𝐵) |
| 39 | | simpr1 1195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑥 ∈ ∪ 𝐵) |
| 40 | | simpr2 1196 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑦 ∈ ∪ 𝐵) |
| 41 | 4, 33, 34, 35, 40, 37 | om1addcl 25066 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦(*𝑝‘𝐽)𝑧) ∈ ∪ 𝐵) |
| 42 | 4, 33, 34, 35, 39, 41 | om1addcl 25066 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)) ∈ ∪ 𝐵) |
| 43 | 1, 2, 3, 7 | pi1eluni 25075 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐵 ↔ (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌 ∧ (𝑥‘1) = 𝑌))) |
| 44 | 43 | biimpa 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌 ∧ (𝑥‘1) = 𝑌)) |
| 45 | 44 | 3ad2antr1 1189 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌 ∧ (𝑥‘1) = 𝑌)) |
| 46 | 45 | simp1d 1143 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑥 ∈ (II Cn 𝐽)) |
| 47 | 6 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝐵 = (Base‘𝐺)) |
| 48 | 1, 33, 34, 47 | pi1eluni 25075 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦 ∈ ∪ 𝐵 ↔ (𝑦 ∈ (II Cn 𝐽) ∧ (𝑦‘0) = 𝑌 ∧ (𝑦‘1) = 𝑌))) |
| 49 | 40, 48 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦 ∈ (II Cn 𝐽) ∧ (𝑦‘0) = 𝑌 ∧ (𝑦‘1) = 𝑌)) |
| 50 | 49 | simp1d 1143 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑦 ∈ (II Cn 𝐽)) |
| 51 | 1, 33, 34, 47 | pi1eluni 25075 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑧 ∈ ∪ 𝐵 ↔ (𝑧 ∈ (II Cn 𝐽) ∧ (𝑧‘0) = 𝑌 ∧ (𝑧‘1) = 𝑌))) |
| 52 | 37, 51 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑧 ∈ (II Cn 𝐽) ∧ (𝑧‘0) = 𝑌 ∧ (𝑧‘1) = 𝑌)) |
| 53 | 52 | simp1d 1143 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → 𝑧 ∈ (II Cn 𝐽)) |
| 54 | 45 | simp3d 1145 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥‘1) = 𝑌) |
| 55 | 49 | simp2d 1144 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦‘0) = 𝑌) |
| 56 | 54, 55 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑥‘1) = (𝑦‘0)) |
| 57 | 49 | simp3d 1145 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → (𝑦‘1) = 𝑌) |
| 58 | 52 | simp2d 1144 |
. . . . . 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 25057 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)( ≃ph‘𝐽)(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧))) |
| 62 | | brinxp2 5763 |
. . . 4
⊢ (((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)) ↔ ((((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧) ∈ ∪ 𝐵 ∧ (𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)) ∈ ∪ 𝐵) ∧ ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)( ≃ph‘𝐽)(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧)))) |
| 63 | 38, 42, 61, 62 | syl21anbrc 1345 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵)) → ((𝑥(*𝑝‘𝐽)𝑦)(*𝑝‘𝐽)𝑧)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑥(*𝑝‘𝐽)(𝑦(*𝑝‘𝐽)𝑧))) |
| 64 | | pi1grplem.z |
. . . . . 6
⊢ 0 = ((0[,]1)
× {𝑌}) |
| 65 | 64 | pcoptcl 25054 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝑋) → ( 0 ∈ (II Cn 𝐽) ∧ ( 0 ‘0) = 𝑌 ∧ ( 0 ‘1) = 𝑌)) |
| 66 | 2, 3, 65 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ( 0 ∈ (II Cn 𝐽) ∧ ( 0 ‘0) = 𝑌 ∧ ( 0 ‘1) = 𝑌)) |
| 67 | 1, 2, 3, 7 | pi1eluni 25075 |
. . . 4
⊢ (𝜑 → ( 0 ∈ ∪ 𝐵
↔ ( 0 ∈ (II Cn 𝐽) ∧ ( 0 ‘0) = 𝑌 ∧ ( 0 ‘1) = 𝑌))) |
| 68 | 66, 67 | mpbird 257 |
. . 3
⊢ (𝜑 → 0 ∈ ∪ 𝐵) |
| 69 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝐽 ∈ (TopOn‘𝑋)) |
| 70 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝑌 ∈ 𝑋) |
| 71 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
| 72 | 68 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 0 ∈ ∪ 𝐵) |
| 73 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝑥 ∈ ∪ 𝐵) |
| 74 | 4, 69, 70, 71, 72, 73 | om1addcl 25066 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ( 0
(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵) |
| 75 | 18 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 𝑥 ∈ (II Cn 𝐽)) |
| 76 | 44 | simp2d 1144 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑥‘0) = 𝑌) |
| 77 | 64 | pcopt 25055 |
. . . . 5
⊢ ((𝑥 ∈ (II Cn 𝐽) ∧ (𝑥‘0) = 𝑌) → ( 0
(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)𝑥) |
| 78 | 75, 76, 77 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ( 0
(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)𝑥) |
| 79 | | brinxp2 5763 |
. . . 4
⊢ (( 0
(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑥 ↔ ((( 0
(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵 ∧ 𝑥 ∈ ∪ 𝐵) ∧ ( 0
(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽)𝑥)) |
| 80 | 74, 73, 78, 79 | syl21anbrc 1345 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ( 0
(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑥) |
| 81 | | eqid 2737 |
. . . . . . 7
⊢ (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) = (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) |
| 82 | 81 | pcorevcl 25058 |
. . . . . 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 1143 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽)) |
| 85 | 83 | simp2d 1144 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = (𝑥‘1)) |
| 86 | 44 | simp3d 1145 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑥‘1) = 𝑌) |
| 87 | 85, 86 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = 𝑌) |
| 88 | 83 | simp3d 1145 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = (𝑥‘0)) |
| 89 | 88, 76 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = 𝑌) |
| 90 | 1, 2, 3, 7 | pi1eluni 25075 |
. . . . 5
⊢ (𝜑 → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ ∪ 𝐵 ↔ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = 𝑌 ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = 𝑌))) |
| 91 | 90 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ ∪ 𝐵 ↔ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ (II Cn 𝐽) ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘0) = 𝑌 ∧ ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))‘1) = 𝑌))) |
| 92 | 84, 87, 89, 91 | mpbir3and 1343 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → (𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎))) ∈ ∪ 𝐵) |
| 93 | 4, 69, 70, 71, 92, 73 | om1addcl 25066 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵) |
| 94 | | eqid 2737 |
. . . . . . 7
⊢ ((0[,]1)
× {(𝑥‘1)}) =
((0[,]1) × {(𝑥‘1)}) |
| 95 | 81, 94 | pcorev 25060 |
. . . . . 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 4638 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → {(𝑥‘1)} = {𝑌}) |
| 98 | 97 | xpeq2d 5715 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((0[,]1) ×
{(𝑥‘1)}) = ((0[,]1)
× {𝑌})) |
| 99 | 64, 98 | eqtr4id 2796 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → 0 = ((0[,]1) × {(𝑥‘1)})) |
| 100 | 96, 99 | breqtrrd 5171 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽) 0 ) |
| 101 | | brinxp2 5763 |
. . . 4
⊢ (((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)) 0 ↔ ((((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥) ∈ ∪ 𝐵 ∧ 0 ∈ ∪ 𝐵)
∧ ((𝑎 ∈ (0[,]1)
↦ (𝑥‘(1 −
𝑎)))(*𝑝‘𝐽)𝑥)( ≃ph‘𝐽) 0 )) |
| 102 | 93, 72, 100, 101 | syl21anbrc 1345 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐵) → ((𝑎 ∈ (0[,]1) ↦ (𝑥‘(1 − 𝑎)))(*𝑝‘𝐽)𝑥)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)) 0 ) |
| 103 | 14, 9, 15, 19, 11, 26, 32, 63, 68, 80, 92, 102 | qusgrp2 19076 |
. 2
⊢ (𝜑 → (𝐺 ∈ Grp ∧ [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (0g‘𝐺))) |
| 104 | | ecinxp 8832 |
. . . . 5
⊢ ((((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵
∧ 0
∈ ∪ 𝐵) → [ 0 ](
≃ph‘𝐽) = [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))) |
| 105 | 13, 68, 104 | syl2anc 584 |
. . . 4
⊢ (𝜑 → [ 0 ](
≃ph‘𝐽) = [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))) |
| 106 | 105 | eqeq1d 2739 |
. . 3
⊢ (𝜑 → ([ 0 ](
≃ph‘𝐽) = (0g‘𝐺) ↔ [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (0g‘𝐺))) |
| 107 | 106 | anbi2d 630 |
. 2
⊢ (𝜑 → ((𝐺 ∈ Grp ∧ [ 0 ](
≃ph‘𝐽) = (0g‘𝐺)) ↔ (𝐺 ∈ Grp ∧ [ 0 ]((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (0g‘𝐺)))) |
| 108 | 103, 107 | mpbird 257 |
1
⊢ (𝜑 → (𝐺 ∈ Grp ∧ [ 0 ](
≃ph‘𝐽) = (0g‘𝐺))) |