Step |
Hyp |
Ref |
Expression |
1 |
|
pwsle.y |
⊢ 𝑌 = ( 𝑅 ↑s 𝐼 ) |
2 |
|
pwsle.v |
⊢ 𝐵 = ( Base ‘ 𝑌 ) |
3 |
|
pwsle.o |
⊢ 𝑂 = ( le ‘ 𝑅 ) |
4 |
|
pwsle.l |
⊢ ≤ = ( le ‘ 𝑌 ) |
5 |
|
vex |
⊢ 𝑓 ∈ V |
6 |
|
vex |
⊢ 𝑔 ∈ V |
7 |
5 6
|
prss |
⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ↔ { 𝑓 , 𝑔 } ⊆ 𝐵 ) |
8 |
|
eqid |
⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 ) |
9 |
1 8
|
pwsval |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) |
10 |
9
|
fveq2d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) |
11 |
2 10
|
eqtrid |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐵 = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) |
12 |
11
|
sseq2d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( { 𝑓 , 𝑔 } ⊆ 𝐵 ↔ { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) ) |
13 |
7 12
|
syl5bb |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ↔ { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) ) |
14 |
13
|
anbi1d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ ( { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) |
15 |
|
fvconst2g |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 ) |
16 |
15
|
ad4ant14 |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 ) |
17 |
16
|
fveq2d |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = ( le ‘ 𝑅 ) ) |
18 |
17 3
|
eqtr4di |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = 𝑂 ) |
19 |
18
|
breqd |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) 𝑂 ( 𝑔 ‘ 𝑥 ) ) ) |
20 |
19
|
ralbidva |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) 𝑂 ( 𝑔 ‘ 𝑥 ) ) ) |
21 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
22 |
|
simpll |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑅 ∈ 𝑉 ) |
23 |
|
simplr |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑊 ) |
24 |
|
simprl |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ 𝐵 ) |
25 |
1 21 2 22 23 24
|
pwselbas |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
26 |
25
|
ffnd |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 Fn 𝐼 ) |
27 |
|
simprr |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ 𝐵 ) |
28 |
1 21 2 22 23 27
|
pwselbas |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) |
29 |
28
|
ffnd |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 Fn 𝐼 ) |
30 |
|
inidm |
⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼 |
31 |
|
eqidd |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) ) |
32 |
|
eqidd |
⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) |
33 |
26 29 24 27 30 31 32
|
ofrfvalg |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 ∘r 𝑂 𝑔 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) 𝑂 ( 𝑔 ‘ 𝑥 ) ) ) |
34 |
20 33
|
bitr4d |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ 𝑓 ∘r 𝑂 𝑔 ) ) |
35 |
34
|
pm5.32da |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑓 ∘r 𝑂 𝑔 ) ) ) |
36 |
|
brinxp2 |
⊢ ( 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 ↔ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑓 ∘r 𝑂 𝑔 ) ) |
37 |
35 36
|
bitr4di |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 ) ) |
38 |
14 37
|
bitr3d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 ) ) |
39 |
38
|
opabbidv |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → { 〈 𝑓 , 𝑔 〉 ∣ ( { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { 〈 𝑓 , 𝑔 〉 ∣ 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 } ) |
40 |
9
|
fveq2d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( le ‘ 𝑌 ) = ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) |
41 |
4 40
|
eqtrid |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ≤ = ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ) |
42 |
|
eqid |
⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) |
43 |
|
fvexd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝑅 ) ∈ V ) |
44 |
|
simpr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐼 ∈ 𝑊 ) |
45 |
|
snex |
⊢ { 𝑅 } ∈ V |
46 |
|
xpexg |
⊢ ( ( 𝐼 ∈ 𝑊 ∧ { 𝑅 } ∈ V ) → ( 𝐼 × { 𝑅 } ) ∈ V ) |
47 |
44 45 46
|
sylancl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 𝑅 } ) ∈ V ) |
48 |
|
eqid |
⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) |
49 |
|
snnzg |
⊢ ( 𝑅 ∈ 𝑉 → { 𝑅 } ≠ ∅ ) |
50 |
49
|
adantr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → { 𝑅 } ≠ ∅ ) |
51 |
|
dmxp |
⊢ ( { 𝑅 } ≠ ∅ → dom ( 𝐼 × { 𝑅 } ) = 𝐼 ) |
52 |
50 51
|
syl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → dom ( 𝐼 × { 𝑅 } ) = 𝐼 ) |
53 |
|
eqid |
⊢ ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) |
54 |
42 43 47 48 52 53
|
prdsle |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) = { 〈 𝑓 , 𝑔 〉 ∣ ( { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ) |
55 |
41 54
|
eqtrd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ≤ = { 〈 𝑓 , 𝑔 〉 ∣ ( { 𝑓 , 𝑔 } ⊆ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ) |
56 |
|
relinxp |
⊢ Rel ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) |
57 |
56
|
a1i |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → Rel ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) ) |
58 |
|
dfrel4v |
⊢ ( Rel ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) ↔ ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) = { 〈 𝑓 , 𝑔 〉 ∣ 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 } ) |
59 |
57 58
|
sylib |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) = { 〈 𝑓 , 𝑔 〉 ∣ 𝑓 ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) 𝑔 } ) |
60 |
39 55 59
|
3eqtr4d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ≤ = ( ∘r 𝑂 ∩ ( 𝐵 × 𝐵 ) ) ) |