| Step | Hyp | Ref
| Expression |
| 1 | | vex 3484 |
. . . . . . 7
⊢ 𝑓 ∈ V |
| 2 | | vex 3484 |
. . . . . . 7
⊢ 𝑔 ∈ V |
| 3 | 1, 2 | prss 4820 |
. . . . . 6
⊢ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ↔ {𝑓, 𝑔} ⊆ 𝐵) |
| 4 | | pwsle.v |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑌) |
| 5 | | pwsle.y |
. . . . . . . . . 10
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
| 6 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
| 7 | 5, 6 | pwsval 17531 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = ((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
| 8 | 7 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑌) = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
| 9 | 4, 8 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐵 = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
| 10 | 9 | sseq2d 4016 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ({𝑓, 𝑔} ⊆ 𝐵 ↔ {𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))) |
| 11 | 3, 10 | bitrid 283 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ↔ {𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))) |
| 12 | 11 | anbi1d 631 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)))) |
| 13 | | fvconst2g 7222 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑅})‘𝑥) = 𝑅) |
| 14 | 13 | ad4ant14 752 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑅})‘𝑥) = 𝑅) |
| 15 | 14 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (le‘((𝐼 × {𝑅})‘𝑥)) = (le‘𝑅)) |
| 16 | | pwsle.o |
. . . . . . . . . 10
⊢ 𝑂 = (le‘𝑅) |
| 17 | 15, 16 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (le‘((𝐼 × {𝑅})‘𝑥)) = 𝑂) |
| 18 | 17 | breqd 5154 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥) ↔ (𝑓‘𝑥)𝑂(𝑔‘𝑥))) |
| 19 | 18 | ralbidva 3176 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥) ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑂(𝑔‘𝑥))) |
| 20 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 21 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑅 ∈ 𝑉) |
| 22 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ 𝑊) |
| 23 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵) |
| 24 | 5, 20, 4, 21, 22, 23 | pwselbas 17534 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓:𝐼⟶(Base‘𝑅)) |
| 25 | 24 | ffnd 6737 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 Fn 𝐼) |
| 26 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵) |
| 27 | 5, 20, 4, 21, 22, 26 | pwselbas 17534 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔:𝐼⟶(Base‘𝑅)) |
| 28 | 27 | ffnd 6737 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 Fn 𝐼) |
| 29 | | inidm 4227 |
. . . . . . . 8
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
| 30 | | eqidd 2738 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥)) |
| 31 | | eqidd 2738 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥)) |
| 32 | 25, 28, 23, 26, 29, 30, 31 | ofrfvalg 7705 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓 ∘r 𝑂𝑔 ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑂(𝑔‘𝑥))) |
| 33 | 19, 32 | bitr4d 282 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥) ↔ 𝑓 ∘r 𝑂𝑔)) |
| 34 | 33 | pm5.32da 579 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑓 ∘r 𝑂𝑔))) |
| 35 | | brinxp2 5763 |
. . . . 5
⊢ (𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔 ↔ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑓 ∘r 𝑂𝑔)) |
| 36 | 34, 35 | bitr4di 289 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ 𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔)) |
| 37 | 12, 36 | bitr3d 281 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ 𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔)) |
| 38 | 37 | opabbidv 5209 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥))} = {〈𝑓, 𝑔〉 ∣ 𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔}) |
| 39 | | pwsle.l |
. . . 4
⊢ ≤ =
(le‘𝑌) |
| 40 | 7 | fveq2d 6910 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (le‘𝑌) = (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
| 41 | 39, 40 | eqtrid 2789 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ =
(le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
| 42 | | eqid 2737 |
. . . 4
⊢
((Scalar‘𝑅)Xs(𝐼 × {𝑅})) = ((Scalar‘𝑅)Xs(𝐼 × {𝑅})) |
| 43 | | fvexd 6921 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Scalar‘𝑅) ∈ V) |
| 44 | | simpr 484 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐼 ∈ 𝑊) |
| 45 | | snex 5436 |
. . . . 5
⊢ {𝑅} ∈ V |
| 46 | | xpexg 7770 |
. . . . 5
⊢ ((𝐼 ∈ 𝑊 ∧ {𝑅} ∈ V) → (𝐼 × {𝑅}) ∈ V) |
| 47 | 44, 45, 46 | sylancl 586 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐼 × {𝑅}) ∈ V) |
| 48 | | eqid 2737 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
| 49 | | snnzg 4774 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → {𝑅} ≠ ∅) |
| 50 | 49 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {𝑅} ≠ ∅) |
| 51 | | dmxp 5939 |
. . . . 5
⊢ ({𝑅} ≠ ∅ → dom (𝐼 × {𝑅}) = 𝐼) |
| 52 | 50, 51 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → dom (𝐼 × {𝑅}) = 𝐼) |
| 53 | | eqid 2737 |
. . . 4
⊢
(le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
| 54 | 42, 43, 47, 48, 52, 53 | prdsle 17507 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥))}) |
| 55 | 41, 54 | eqtrd 2777 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥))}) |
| 56 | | relinxp 5824 |
. . . 4
⊢ Rel (
∘r 𝑂 ∩
(𝐵 × 𝐵)) |
| 57 | 56 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → Rel ( ∘r 𝑂 ∩ (𝐵 × 𝐵))) |
| 58 | | dfrel4v 6210 |
. . 3
⊢ (Rel (
∘r 𝑂 ∩
(𝐵 × 𝐵)) ↔ ( ∘r
𝑂 ∩ (𝐵 × 𝐵)) = {〈𝑓, 𝑔〉 ∣ 𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔}) |
| 59 | 57, 58 | sylib 218 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ( ∘r 𝑂 ∩ (𝐵 × 𝐵)) = {〈𝑓, 𝑔〉 ∣ 𝑓( ∘r 𝑂 ∩ (𝐵 × 𝐵))𝑔}) |
| 60 | 38, 55, 59 | 3eqtr4d 2787 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = ( ∘r
𝑂 ∩ (𝐵 × 𝐵))) |