| Step | Hyp | Ref
| Expression |
| 1 | | coass 6285 |
. . . . 5
⊢ ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = (𝐴 ∘ ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 2 | | df1o2 8513 |
. . . . . . . . 9
⊢
1o = {∅} |
| 3 | | pf1ind.cb |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) |
| 4 | 3 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
| 5 | | 0ex 5307 |
. . . . . . . . 9
⊢ ∅
∈ V |
| 6 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) = (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) |
| 7 | 2, 4, 5, 6 | mapsncnv 8933 |
. . . . . . . 8
⊢ ◡(𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) = (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})) |
| 8 | 7 | coeq2i 5871 |
. . . . . . 7
⊢ ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) ∘
◡(𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) =
((𝑏 ∈ (𝐵 ↑m
1o) ↦ (𝑏‘∅)) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) |
| 9 | 2, 4, 5, 6 | mapsnf1o2 8934 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)):(𝐵 ↑m
1o)–1-1-onto→𝐵 |
| 10 | | f1ococnv2 6875 |
. . . . . . . 8
⊢ ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)):(𝐵 ↑m
1o)–1-1-onto→𝐵 → ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) ∘
◡(𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) = ( I
↾ 𝐵)) |
| 11 | 9, 10 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) ∘
◡(𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) = ( I
↾ 𝐵)) |
| 12 | 8, 11 | eqtr3id 2791 |
. . . . . 6
⊢ (𝜑 → ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = ( I ↾ 𝐵)) |
| 13 | 12 | coeq2d 5873 |
. . . . 5
⊢ (𝜑 → (𝐴 ∘ ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) = (𝐴 ∘ ( I ↾ 𝐵))) |
| 14 | 1, 13 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = (𝐴 ∘ ( I ↾ 𝐵))) |
| 15 | | pf1ind.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑄) |
| 16 | | pf1ind.cq |
. . . . . 6
⊢ 𝑄 = ran
(eval1‘𝑅) |
| 17 | 16, 3 | pf1f 22354 |
. . . . 5
⊢ (𝐴 ∈ 𝑄 → 𝐴:𝐵⟶𝐵) |
| 18 | | fcoi1 6782 |
. . . . 5
⊢ (𝐴:𝐵⟶𝐵 → (𝐴 ∘ ( I ↾ 𝐵)) = 𝐴) |
| 19 | 15, 17, 18 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝐴 ∘ ( I ↾ 𝐵)) = 𝐴) |
| 20 | 14, 19 | eqtrd 2777 |
. . 3
⊢ (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = 𝐴) |
| 21 | | pf1ind.cp |
. . . 4
⊢ + =
(+g‘𝑅) |
| 22 | | pf1ind.ct |
. . . 4
⊢ · =
(.r‘𝑅) |
| 23 | | eqid 2737 |
. . . . . 6
⊢
(1o eval 𝑅) = (1o eval 𝑅) |
| 24 | 23, 3 | evlval 22119 |
. . . . 5
⊢
(1o eval 𝑅) = ((1o evalSub 𝑅)‘𝐵) |
| 25 | 24 | rneqi 5948 |
. . . 4
⊢ ran
(1o eval 𝑅) =
ran ((1o evalSub 𝑅)‘𝐵) |
| 26 | | an4 656 |
. . . . . 6
⊢ (((𝑎 ∈ ran (1o eval
𝑅) ∧ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) ↔ ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) ∧ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}))) |
| 27 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ran
(1o eval 𝑅) =
ran (1o eval 𝑅) |
| 28 | 16, 3, 27 | mpfpf1 22355 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ran (1o eval
𝑅) → (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄) |
| 29 | 16, 3, 27 | mpfpf1 22355 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ran (1o eval
𝑅) → (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄) |
| 30 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
| 31 | | pf1ind.wc |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏)) |
| 32 | 30, 31 | elab 3679 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ {𝑥 ∣ 𝜓} ↔ 𝜏) |
| 33 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (𝑓 ∈ {𝑥 ∣ 𝜓} ↔ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 34 | 32, 33 | bitr3id 285 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (𝜏 ↔ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 35 | 34 | anbi1d 631 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → ((𝜏 ∧ 𝜂) ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂))) |
| 36 | 35 | anbi1d 631 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (((𝜏 ∧ 𝜂) ∧ 𝜑) ↔ (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑))) |
| 37 | | ovex 7464 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∘f + 𝑔) ∈ V |
| 38 | | pf1ind.we |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 ∘f + 𝑔) → (𝜓 ↔ 𝜁)) |
| 39 | 37, 38 | elab 3679 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∘f + 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ 𝜁) |
| 40 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (𝑓 ∘f + 𝑔) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔)) |
| 41 | 40 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → ((𝑓 ∘f + 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥 ∣ 𝜓})) |
| 42 | 39, 41 | bitr3id 285 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (𝜁 ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥 ∣ 𝜓})) |
| 43 | 36, 42 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → ((((𝜏 ∧ 𝜂) ∧ 𝜑) → 𝜁) ↔ ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥 ∣ 𝜓}))) |
| 44 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑔 ∈ V |
| 45 | | pf1ind.wd |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂)) |
| 46 | 44, 45 | elab 3679 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ {𝑥 ∣ 𝜓} ↔ 𝜂) |
| 47 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (𝑔 ∈ {𝑥 ∣ 𝜓} ↔ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 48 | 46, 47 | bitr3id 285 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (𝜂 ↔ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 49 | 48 | anbi2d 630 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}))) |
| 50 | 49 | anbi1d 631 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑) ↔ (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑))) |
| 51 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))))) |
| 52 | 51 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
| 53 | 50, 52 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥 ∣ 𝜓}) ↔ ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓}))) |
| 54 | | pf1ind.ad |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁) |
| 55 | 54 | expcom 413 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂)) → (𝜑 → 𝜁)) |
| 56 | 55 | an4s 660 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄) ∧ (𝜏 ∧ 𝜂)) → (𝜑 → 𝜁)) |
| 57 | 56 | expimpd 453 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄) → (((𝜏 ∧ 𝜂) ∧ 𝜑) → 𝜁)) |
| 58 | 43, 53, 57 | vtocl2ga 3578 |
. . . . . . . . . . 11
⊢ (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄 ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄) → ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
| 59 | 28, 29, 58 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ran (1o eval
𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
| 60 | 59 | expcomd 416 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ran (1o eval
𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → (𝜑 → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓}))) |
| 61 | 60 | impcom 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
| 62 | 25, 3 | mpff 22128 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ran (1o eval
𝑅) → 𝑎:(𝐵 ↑m
1o)⟶𝐵) |
| 63 | 62 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑎:(𝐵 ↑m
1o)⟶𝐵) |
| 64 | 63 | ffnd 6737 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑎 Fn (𝐵 ↑m
1o)) |
| 65 | 25, 3 | mpff 22128 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ran (1o eval
𝑅) → 𝑏:(𝐵 ↑m
1o)⟶𝐵) |
| 66 | 65 | ad2antll 729 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑏:(𝐵 ↑m
1o)⟶𝐵) |
| 67 | 66 | ffnd 6737 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑏 Fn (𝐵 ↑m
1o)) |
| 68 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})) = (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})) |
| 69 | 2, 4, 5, 68 | mapsnf1o3 8935 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})):𝐵–1-1-onto→(𝐵 ↑m
1o) |
| 70 | | f1of 6848 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐵 ↦ (1o × {𝑤})):𝐵–1-1-onto→(𝐵 ↑m 1o) →
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤})):𝐵⟶(𝐵 ↑m
1o)) |
| 71 | 69, 70 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})):𝐵⟶(𝐵 ↑m
1o)) |
| 72 | | ovexd 7466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (𝐵 ↑m 1o) ∈
V) |
| 73 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝐵 ∈ V) |
| 74 | | inidm 4227 |
. . . . . . . . . 10
⊢ ((𝐵 ↑m
1o) ∩ (𝐵
↑m 1o)) = (𝐵 ↑m
1o) |
| 75 | 64, 67, 71, 72, 72, 73, 74 | ofco 7722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → ((𝑎 ∘f + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))))) |
| 76 | 75 | eleq1d 2826 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘f + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
| 77 | 61, 76 | sylibrd 259 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘f + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 78 | 77 | expimpd 453 |
. . . . . 6
⊢ (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) ∧ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) → ((𝑎 ∘f + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 79 | 26, 78 | biimtrid 242 |
. . . . 5
⊢ (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) → ((𝑎 ∘f + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 80 | 79 | imp 406 |
. . . 4
⊢ ((𝜑 ∧ ((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}))) → ((𝑎 ∘f + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
| 81 | | ovex 7464 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∘f · 𝑔) ∈ V |
| 82 | | pf1ind.wf |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 ∘f · 𝑔) → (𝜓 ↔ 𝜎)) |
| 83 | 81, 82 | elab 3679 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∘f · 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ 𝜎) |
| 84 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (𝑓 ∘f · 𝑔) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔)) |
| 85 | 84 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → ((𝑓 ∘f · 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥 ∣ 𝜓})) |
| 86 | 83, 85 | bitr3id 285 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (𝜎 ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥 ∣ 𝜓})) |
| 87 | 36, 86 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → ((((𝜏 ∧ 𝜂) ∧ 𝜑) → 𝜎) ↔ ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥 ∣ 𝜓}))) |
| 88 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))))) |
| 89 | 88 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
| 90 | 50, 89 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) → (((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥 ∣ 𝜓}) ↔ ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓}))) |
| 91 | | pf1ind.mu |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎) |
| 92 | 91 | expcom 413 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂)) → (𝜑 → 𝜎)) |
| 93 | 92 | an4s 660 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄) ∧ (𝜏 ∧ 𝜂)) → (𝜑 → 𝜎)) |
| 94 | 93 | expimpd 453 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄) → (((𝜏 ∧ 𝜂) ∧ 𝜑) → 𝜎)) |
| 95 | 87, 90, 94 | vtocl2ga 3578 |
. . . . . . . . . . 11
⊢ (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄 ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄) → ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
| 96 | 28, 29, 95 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ran (1o eval
𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
| 97 | 96 | expcomd 416 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ran (1o eval
𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → (𝜑 → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓}))) |
| 98 | 97 | impcom 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
| 99 | 64, 67, 71, 72, 72, 73, 74 | ofco 7722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → ((𝑎 ∘f · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))))) |
| 100 | 99 | eleq1d 2826 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘f · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
| 101 | 98, 100 | sylibrd 259 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘f · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 102 | 101 | expimpd 453 |
. . . . . 6
⊢ (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) ∧ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) → ((𝑎 ∘f · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 103 | 26, 102 | biimtrid 242 |
. . . . 5
⊢ (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) → ((𝑎 ∘f · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 104 | 103 | imp 406 |
. . . 4
⊢ ((𝜑 ∧ ((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}))) → ((𝑎 ∘f · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
| 105 | | coeq1 5868 |
. . . . 5
⊢ (𝑦 = ((𝐵 ↑m 1o) ×
{𝑎}) → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = (((𝐵 ↑m 1o) ×
{𝑎}) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 106 | 105 | eleq1d 2826 |
. . . 4
⊢ (𝑦 = ((𝐵 ↑m 1o) ×
{𝑎}) → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ (((𝐵 ↑m 1o) ×
{𝑎}) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 107 | | coeq1 5868 |
. . . . 5
⊢ (𝑦 = (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘𝑎)) → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 108 | 107 | eleq1d 2826 |
. . . 4
⊢ (𝑦 = (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘𝑎)) → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 109 | | coeq1 5868 |
. . . . 5
⊢ (𝑦 = 𝑎 → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 110 | 109 | eleq1d 2826 |
. . . 4
⊢ (𝑦 = 𝑎 → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 111 | | coeq1 5868 |
. . . . 5
⊢ (𝑦 = 𝑏 → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 112 | 111 | eleq1d 2826 |
. . . 4
⊢ (𝑦 = 𝑏 → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 113 | | coeq1 5868 |
. . . . 5
⊢ (𝑦 = (𝑎 ∘f + 𝑏) → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = ((𝑎 ∘f + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 114 | 113 | eleq1d 2826 |
. . . 4
⊢ (𝑦 = (𝑎 ∘f + 𝑏) → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘f + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 115 | | coeq1 5868 |
. . . . 5
⊢ (𝑦 = (𝑎 ∘f · 𝑏) → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = ((𝑎 ∘f · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 116 | 115 | eleq1d 2826 |
. . . 4
⊢ (𝑦 = (𝑎 ∘f · 𝑏) → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘f · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 117 | | coeq1 5868 |
. . . . 5
⊢ (𝑦 = (𝐴 ∘ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) →
(𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 118 | 117 | eleq1d 2826 |
. . . 4
⊢ (𝑦 = (𝐴 ∘ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) →
((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 119 | 16 | pf1rcl 22353 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑄 → 𝑅 ∈ CRing) |
| 120 | 15, 119 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 121 | 120 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑅 ∈ CRing) |
| 122 | | 1on 8518 |
. . . . . . . . . . . 12
⊢
1o ∈ On |
| 123 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(1o mPoly 𝑅) = (1o mPoly 𝑅) |
| 124 | 123 | mplassa 22042 |
. . . . . . . . . . . 12
⊢
((1o ∈ On ∧ 𝑅 ∈ CRing) → (1o mPoly
𝑅) ∈
AssAlg) |
| 125 | 122, 120,
124 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (1o mPoly 𝑅) ∈
AssAlg) |
| 126 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
| 127 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(algSc‘(Poly1‘𝑅)) =
(algSc‘(Poly1‘𝑅)) |
| 128 | 126, 127 | ply1ascl 22261 |
. . . . . . . . . . . 12
⊢
(algSc‘(Poly1‘𝑅)) = (algSc‘(1o mPoly 𝑅)) |
| 129 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Scalar‘(1o mPoly 𝑅)) = (Scalar‘(1o mPoly
𝑅)) |
| 130 | 128, 129 | asclrhm 21910 |
. . . . . . . . . . 11
⊢
((1o mPoly 𝑅) ∈ AssAlg →
(algSc‘(Poly1‘𝑅)) ∈ ((Scalar‘(1o
mPoly 𝑅)) RingHom
(1o mPoly 𝑅))) |
| 131 | 125, 130 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(algSc‘(Poly1‘𝑅)) ∈ ((Scalar‘(1o
mPoly 𝑅)) RingHom
(1o mPoly 𝑅))) |
| 132 | 122 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1o ∈
On) |
| 133 | 123, 132,
120 | mplsca 22033 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 = (Scalar‘(1o mPoly 𝑅))) |
| 134 | 133 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 RingHom (1o mPoly 𝑅)) =
((Scalar‘(1o mPoly 𝑅)) RingHom (1o mPoly 𝑅))) |
| 135 | 131, 134 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ (𝜑 →
(algSc‘(Poly1‘𝑅)) ∈ (𝑅 RingHom (1o mPoly 𝑅))) |
| 136 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(1o mPoly 𝑅)) = (Base‘(1o mPoly 𝑅)) |
| 137 | 3, 136 | rhmf 20485 |
. . . . . . . . 9
⊢
((algSc‘(Poly1‘𝑅)) ∈ (𝑅 RingHom (1o mPoly 𝑅)) →
(algSc‘(Poly1‘𝑅)):𝐵⟶(Base‘(1o mPoly
𝑅))) |
| 138 | 135, 137 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(algSc‘(Poly1‘𝑅)):𝐵⟶(Base‘(1o mPoly
𝑅))) |
| 139 | 138 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) →
((algSc‘(Poly1‘𝑅))‘𝑎) ∈ (Base‘(1o mPoly
𝑅))) |
| 140 | | eqid 2737 |
. . . . . . . 8
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
| 141 | 140, 23, 3, 123, 136 | evl1val 22333 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧
((algSc‘(Poly1‘𝑅))‘𝑎) ∈ (Base‘(1o mPoly
𝑅))) →
((eval1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) = (((1o eval 𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 142 | 121, 139,
141 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((eval1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) = (((1o eval 𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 143 | 140, 126,
3, 127 | evl1sca 22338 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑎 ∈ 𝐵) → ((eval1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) = (𝐵 × {𝑎})) |
| 144 | 120, 143 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((eval1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) = (𝐵 × {𝑎})) |
| 145 | 3 | ressid 17290 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ CRing → (𝑅 ↾s 𝐵) = 𝑅) |
| 146 | 121, 145 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑅 ↾s 𝐵) = 𝑅) |
| 147 | 146 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (1o mPoly (𝑅 ↾s 𝐵)) = (1o mPoly 𝑅)) |
| 148 | 147 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (algSc‘(1o mPoly
(𝑅 ↾s
𝐵))) =
(algSc‘(1o mPoly 𝑅))) |
| 149 | 148, 128 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (algSc‘(1o mPoly
(𝑅 ↾s
𝐵))) =
(algSc‘(Poly1‘𝑅))) |
| 150 | 149 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((algSc‘(1o mPoly
(𝑅 ↾s
𝐵)))‘𝑎) =
((algSc‘(Poly1‘𝑅))‘𝑎)) |
| 151 | 150 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((1o eval 𝑅)‘((algSc‘(1o mPoly
(𝑅 ↾s
𝐵)))‘𝑎)) = ((1o eval 𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎))) |
| 152 | | eqid 2737 |
. . . . . . . . 9
⊢
(1o mPoly (𝑅 ↾s 𝐵)) = (1o mPoly (𝑅 ↾s 𝐵)) |
| 153 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑅 ↾s 𝐵) = (𝑅 ↾s 𝐵) |
| 154 | | eqid 2737 |
. . . . . . . . 9
⊢
(algSc‘(1o mPoly (𝑅 ↾s 𝐵))) = (algSc‘(1o mPoly
(𝑅 ↾s
𝐵))) |
| 155 | 122 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 1o ∈
On) |
| 156 | | crngring 20242 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 157 | 3 | subrgid 20573 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅)) |
| 158 | 120, 156,
157 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅)) |
| 159 | 158 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐵 ∈ (SubRing‘𝑅)) |
| 160 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
| 161 | 24, 152, 153, 3, 154, 155, 121, 159, 160 | evlssca 22113 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((1o eval 𝑅)‘((algSc‘(1o mPoly
(𝑅 ↾s
𝐵)))‘𝑎)) = ((𝐵 ↑m 1o) ×
{𝑎})) |
| 162 | 151, 161 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((1o eval 𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) = ((𝐵 ↑m 1o) × {𝑎})) |
| 163 | 162 | coeq1d 5872 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((1o eval 𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = (((𝐵 ↑m 1o) × {𝑎}) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 164 | 142, 144,
163 | 3eqtr3d 2785 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐵 × {𝑎}) = (((𝐵 ↑m 1o) ×
{𝑎}) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 165 | | pf1ind.co |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → 𝜒) |
| 166 | | vsnex 5434 |
. . . . . . . . . 10
⊢ {𝑓} ∈ V |
| 167 | 4, 166 | xpex 7773 |
. . . . . . . . 9
⊢ (𝐵 × {𝑓}) ∈ V |
| 168 | | pf1ind.wa |
. . . . . . . . 9
⊢ (𝑥 = (𝐵 × {𝑓}) → (𝜓 ↔ 𝜒)) |
| 169 | 167, 168 | elab 3679 |
. . . . . . . 8
⊢ ((𝐵 × {𝑓}) ∈ {𝑥 ∣ 𝜓} ↔ 𝜒) |
| 170 | 165, 169 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → (𝐵 × {𝑓}) ∈ {𝑥 ∣ 𝜓}) |
| 171 | 170 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 (𝐵 × {𝑓}) ∈ {𝑥 ∣ 𝜓}) |
| 172 | | sneq 4636 |
. . . . . . . . 9
⊢ (𝑓 = 𝑎 → {𝑓} = {𝑎}) |
| 173 | 172 | xpeq2d 5715 |
. . . . . . . 8
⊢ (𝑓 = 𝑎 → (𝐵 × {𝑓}) = (𝐵 × {𝑎})) |
| 174 | 173 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑓 = 𝑎 → ((𝐵 × {𝑓}) ∈ {𝑥 ∣ 𝜓} ↔ (𝐵 × {𝑎}) ∈ {𝑥 ∣ 𝜓})) |
| 175 | 174 | rspccva 3621 |
. . . . . 6
⊢
((∀𝑓 ∈
𝐵 (𝐵 × {𝑓}) ∈ {𝑥 ∣ 𝜓} ∧ 𝑎 ∈ 𝐵) → (𝐵 × {𝑎}) ∈ {𝑥 ∣ 𝜓}) |
| 176 | 171, 175 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐵 × {𝑎}) ∈ {𝑥 ∣ 𝜓}) |
| 177 | 164, 176 | eqeltrrd 2842 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((𝐵 ↑m 1o) ×
{𝑎}) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
| 178 | | pf1ind.pr |
. . . . . . . 8
⊢ (𝜑 → 𝜃) |
| 179 | | resiexg 7934 |
. . . . . . . . . 10
⊢ (𝐵 ∈ V → ( I ↾
𝐵) ∈
V) |
| 180 | 4, 179 | ax-mp 5 |
. . . . . . . . 9
⊢ ( I
↾ 𝐵) ∈
V |
| 181 | | pf1ind.wb |
. . . . . . . . 9
⊢ (𝑥 = ( I ↾ 𝐵) → (𝜓 ↔ 𝜃)) |
| 182 | 180, 181 | elab 3679 |
. . . . . . . 8
⊢ (( I
↾ 𝐵) ∈ {𝑥 ∣ 𝜓} ↔ 𝜃) |
| 183 | 178, 182 | sylibr 234 |
. . . . . . 7
⊢ (𝜑 → ( I ↾ 𝐵) ∈ {𝑥 ∣ 𝜓}) |
| 184 | 12, 183 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
| 185 | | el1o 8533 |
. . . . . . . . . 10
⊢ (𝑎 ∈ 1o ↔
𝑎 =
∅) |
| 186 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑎 = ∅ → (𝑏‘𝑎) = (𝑏‘∅)) |
| 187 | 185, 186 | sylbi 217 |
. . . . . . . . 9
⊢ (𝑎 ∈ 1o →
(𝑏‘𝑎) = (𝑏‘∅)) |
| 188 | 187 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑎 ∈ 1o →
(𝑏 ∈ (𝐵 ↑m
1o) ↦ (𝑏‘𝑎)) = (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) |
| 189 | 188 | coeq1d 5872 |
. . . . . . 7
⊢ (𝑎 ∈ 1o →
((𝑏 ∈ (𝐵 ↑m
1o) ↦ (𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) = ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤})))) |
| 190 | 189 | eleq1d 2826 |
. . . . . 6
⊢ (𝑎 ∈ 1o →
(((𝑏 ∈ (𝐵 ↑m
1o) ↦ (𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅)) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 191 | 184, 190 | syl5ibrcom 247 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ 1o → ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
| 192 | 191 | imp 406 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 1o) → ((𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
| 193 | 16, 3, 27 | pf1mpf 22356 |
. . . . 5
⊢ (𝐴 ∈ 𝑄 → (𝐴 ∘ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) ∈
ran (1o eval 𝑅)) |
| 194 | 15, 193 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐴 ∘ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) ∈
ran (1o eval 𝑅)) |
| 195 | 3, 21, 22, 25, 80, 104, 106, 108, 110, 112, 114, 116, 118, 177, 192, 194 | mpfind 22131 |
. . 3
⊢ (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑m 1o) ↦
(𝑏‘∅))) ∘
(𝑤 ∈ 𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
| 196 | 20, 195 | eqeltrrd 2842 |
. 2
⊢ (𝜑 → 𝐴 ∈ {𝑥 ∣ 𝜓}) |
| 197 | | pf1ind.wg |
. . . 4
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌)) |
| 198 | 197 | elabg 3676 |
. . 3
⊢ (𝐴 ∈ 𝑄 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜌)) |
| 199 | 15, 198 | syl 17 |
. 2
⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜌)) |
| 200 | 196, 199 | mpbid 232 |
1
⊢ (𝜑 → 𝜌) |