Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . . . . . 7
⊢ 𝑓 ∈ V |
2 | | vex 3176 |
. . . . . . 7
⊢ 𝑔 ∈ V |
3 | 1, 2 | prss 4291 |
. . . . . 6
⊢ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ↔ {𝑓, 𝑔} ⊆ 𝐵) |
4 | | pwsle.v |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑌) |
5 | | pwsle.y |
. . . . . . . . . 10
⊢ 𝑌 = (𝑅 ↑s 𝐼) |
6 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
7 | 5, 6 | pwsval 15969 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = ((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
8 | 7 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Base‘𝑌) = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
9 | 4, 8 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐵 = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
10 | 9 | sseq2d 3596 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ({𝑓, 𝑔} ⊆ 𝐵 ↔ {𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))) |
11 | 3, 10 | syl5bb 271 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ↔ {𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))))) |
12 | 11 | anbi1d 737 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)))) |
13 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑅 ∈ 𝑉) |
14 | | fvconst2g 6372 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑅})‘𝑥) = 𝑅) |
15 | 13, 14 | sylan 487 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑅})‘𝑥) = 𝑅) |
16 | 15 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (le‘((𝐼 × {𝑅})‘𝑥)) = (le‘𝑅)) |
17 | | pwsle.o |
. . . . . . . . . 10
⊢ 𝑂 = (le‘𝑅) |
18 | 16, 17 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (le‘((𝐼 × {𝑅})‘𝑥)) = 𝑂) |
19 | 18 | breqd 4594 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥) ↔ (𝑓‘𝑥)𝑂(𝑔‘𝑥))) |
20 | 19 | ralbidva 2968 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥) ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑂(𝑔‘𝑥))) |
21 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
22 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ 𝑊) |
23 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵) |
24 | 5, 21, 4, 13, 22, 23 | pwselbas 15972 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓:𝐼⟶(Base‘𝑅)) |
25 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑓:𝐼⟶(Base‘𝑅) → 𝑓 Fn 𝐼) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 Fn 𝐼) |
27 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵) |
28 | 5, 21, 4, 13, 22, 27 | pwselbas 15972 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔:𝐼⟶(Base‘𝑅)) |
29 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑔:𝐼⟶(Base‘𝑅) → 𝑔 Fn 𝐼) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 Fn 𝐼) |
31 | | inidm 3784 |
. . . . . . . 8
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
32 | | eqidd 2611 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥)) |
33 | | eqidd 2611 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥)) |
34 | 26, 30, 22, 22, 31, 32, 33 | ofrfval 6803 |
. . . . . . 7
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓 ∘𝑟 𝑂𝑔 ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑂(𝑔‘𝑥))) |
35 | 20, 34 | bitr4d 270 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥) ↔ 𝑓 ∘𝑟 𝑂𝑔)) |
36 | 35 | pm5.32da 671 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑓 ∘𝑟 𝑂𝑔))) |
37 | | brinxp2 5103 |
. . . . . 6
⊢ (𝑓( ∘𝑟
𝑂 ∩ (𝐵 × 𝐵))𝑔 ↔ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ 𝑓 ∘𝑟 𝑂𝑔)) |
38 | | df-3an 1033 |
. . . . . 6
⊢ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ 𝑓 ∘𝑟 𝑂𝑔) ↔ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑓 ∘𝑟 𝑂𝑔)) |
39 | 37, 38 | bitri 263 |
. . . . 5
⊢ (𝑓( ∘𝑟
𝑂 ∩ (𝐵 × 𝐵))𝑔 ↔ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ 𝑓 ∘𝑟 𝑂𝑔)) |
40 | 36, 39 | syl6bbr 277 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ 𝑓( ∘𝑟 𝑂 ∩ (𝐵 × 𝐵))𝑔)) |
41 | 12, 40 | bitr3d 269 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥)) ↔ 𝑓( ∘𝑟 𝑂 ∩ (𝐵 × 𝐵))𝑔)) |
42 | 41 | opabbidv 4648 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥))} = {〈𝑓, 𝑔〉 ∣ 𝑓( ∘𝑟 𝑂 ∩ (𝐵 × 𝐵))𝑔}) |
43 | | pwsle.l |
. . . 4
⊢ ≤ =
(le‘𝑌) |
44 | 7 | fveq2d 6107 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (le‘𝑌) = (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
45 | 43, 44 | syl5eq 2656 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ =
(le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅})))) |
46 | | eqid 2610 |
. . . 4
⊢
((Scalar‘𝑅)Xs(𝐼 × {𝑅})) = ((Scalar‘𝑅)Xs(𝐼 × {𝑅})) |
47 | | fvex 6113 |
. . . . 5
⊢
(Scalar‘𝑅)
∈ V |
48 | 47 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (Scalar‘𝑅) ∈ V) |
49 | | simpr 476 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐼 ∈ 𝑊) |
50 | | snex 4835 |
. . . . 5
⊢ {𝑅} ∈ V |
51 | | xpexg 6858 |
. . . . 5
⊢ ((𝐼 ∈ 𝑊 ∧ {𝑅} ∈ V) → (𝐼 × {𝑅}) ∈ V) |
52 | 49, 50, 51 | sylancl 693 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐼 × {𝑅}) ∈ V) |
53 | | eqid 2610 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
54 | | snnzg 4251 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → {𝑅} ≠ ∅) |
55 | 54 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → {𝑅} ≠ ∅) |
56 | | dmxp 5265 |
. . . . 5
⊢ ({𝑅} ≠ ∅ → dom (𝐼 × {𝑅}) = 𝐼) |
57 | 55, 56 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → dom (𝐼 × {𝑅}) = 𝐼) |
58 | | eqid 2610 |
. . . 4
⊢
(le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) |
59 | 46, 48, 52, 53, 57, 58 | prdsle 15945 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (le‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) = {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥))}) |
60 | 45, 59 | eqtrd 2644 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (Base‘((Scalar‘𝑅)Xs(𝐼 × {𝑅}))) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘((𝐼 × {𝑅})‘𝑥))(𝑔‘𝑥))}) |
61 | | inss2 3796 |
. . . . 5
⊢ (
∘𝑟 𝑂 ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) |
62 | | relxp 5150 |
. . . . 5
⊢ Rel
(𝐵 × 𝐵) |
63 | | relss 5129 |
. . . . 5
⊢ ((
∘𝑟 𝑂 ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) → (Rel (𝐵 × 𝐵) → Rel ( ∘𝑟
𝑂 ∩ (𝐵 × 𝐵)))) |
64 | 61, 62, 63 | mp2 9 |
. . . 4
⊢ Rel (
∘𝑟 𝑂 ∩ (𝐵 × 𝐵)) |
65 | 64 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → Rel ( ∘𝑟
𝑂 ∩ (𝐵 × 𝐵))) |
66 | | dfrel4v 5503 |
. . 3
⊢ (Rel (
∘𝑟 𝑂 ∩ (𝐵 × 𝐵)) ↔ ( ∘𝑟
𝑂 ∩ (𝐵 × 𝐵)) = {〈𝑓, 𝑔〉 ∣ 𝑓( ∘𝑟 𝑂 ∩ (𝐵 × 𝐵))𝑔}) |
67 | 65, 66 | sylib 207 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ( ∘𝑟 𝑂 ∩ (𝐵 × 𝐵)) = {〈𝑓, 𝑔〉 ∣ 𝑓( ∘𝑟 𝑂 ∩ (𝐵 × 𝐵))𝑔}) |
68 | 42, 60, 67 | 3eqtr4d 2654 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = (
∘𝑟 𝑂 ∩ (𝐵 × 𝐵))) |