Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. 2
⊢ (𝐾 ∈ 𝐶 → 𝐾 ∈ V) |
2 | | trnset.t |
. . 3
⊢ 𝑇 = (Trn‘𝐾) |
3 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) |
4 | | trnset.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
5 | 3, 4 | syl6eqr 2662 |
. . . . 5
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) |
6 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (Dil‘𝑘) = (Dil‘𝐾)) |
7 | | trnset.l |
. . . . . . . 8
⊢ 𝐿 = (Dil‘𝐾) |
8 | 6, 7 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (Dil‘𝑘) = 𝐿) |
9 | 8 | fveq1d 6105 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((Dil‘𝑘)‘𝑑) = (𝐿‘𝑑)) |
10 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (WAtoms‘𝑘) = (WAtoms‘𝐾)) |
11 | | trnset.w |
. . . . . . . . 9
⊢ 𝑊 = (WAtoms‘𝐾) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (WAtoms‘𝑘) = 𝑊) |
13 | 12 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((WAtoms‘𝑘)‘𝑑) = (𝑊‘𝑑)) |
14 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (+𝑃‘𝑘) =
(+𝑃‘𝐾)) |
15 | | trnset.p |
. . . . . . . . . . . 12
⊢ + =
(+𝑃‘𝐾) |
16 | 14, 15 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (+𝑃‘𝑘) = + ) |
17 | 16 | oveqd 6566 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) = (𝑞 + (𝑓‘𝑞))) |
18 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 →
(⊥𝑃‘𝑘) = (⊥𝑃‘𝐾)) |
19 | | trnset.o |
. . . . . . . . . . . 12
⊢ ⊥ =
(⊥𝑃‘𝐾) |
20 | 18, 19 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 →
(⊥𝑃‘𝑘) = ⊥ ) |
21 | 20 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 →
((⊥𝑃‘𝑘)‘{𝑑}) = ( ⊥ ‘{𝑑})) |
22 | 17, 21 | ineq12d 3777 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → ((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑}))) |
23 | 16 | oveqd 6566 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) = (𝑟 + (𝑓‘𝑟))) |
24 | 23, 21 | ineq12d 3777 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))) |
25 | 22, 24 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) ↔ ((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑})))) |
26 | 13, 25 | raleqbidv 3129 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) ↔ ∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑})))) |
27 | 13, 26 | raleqbidv 3129 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) ↔ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑})))) |
28 | 9, 27 | rabeqbidv 3168 |
. . . . 5
⊢ (𝑘 = 𝐾 → {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑}))} = {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))}) |
29 | 5, 28 | mpteq12dv 4663 |
. . . 4
⊢ (𝑘 = 𝐾 → (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑}))}) = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))})) |
30 | | df-trnN 34411 |
. . . 4
⊢ Trn =
(𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ ((Dil‘𝑘)‘𝑑) ∣ ∀𝑞 ∈ ((WAtoms‘𝑘)‘𝑑)∀𝑟 ∈ ((WAtoms‘𝑘)‘𝑑)((𝑞(+𝑃‘𝑘)(𝑓‘𝑞)) ∩
((⊥𝑃‘𝑘)‘{𝑑})) = ((𝑟(+𝑃‘𝑘)(𝑓‘𝑟)) ∩
((⊥𝑃‘𝑘)‘{𝑑}))})) |
31 | | fvex 6113 |
. . . . . 6
⊢
(Atoms‘𝐾)
∈ V |
32 | 4, 31 | eqeltri 2684 |
. . . . 5
⊢ 𝐴 ∈ V |
33 | 32 | mptex 6390 |
. . . 4
⊢ (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))}) ∈ V |
34 | 29, 30, 33 | fvmpt 6191 |
. . 3
⊢ (𝐾 ∈ V →
(Trn‘𝐾) = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))})) |
35 | 2, 34 | syl5eq 2656 |
. 2
⊢ (𝐾 ∈ V → 𝑇 = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))})) |
36 | 1, 35 | syl 17 |
1
⊢ (𝐾 ∈ 𝐶 → 𝑇 = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ (𝐿‘𝑑) ∣ ∀𝑞 ∈ (𝑊‘𝑑)∀𝑟 ∈ (𝑊‘𝑑)((𝑞 + (𝑓‘𝑞)) ∩ ( ⊥ ‘{𝑑})) = ((𝑟 + (𝑓‘𝑟)) ∩ ( ⊥ ‘{𝑑}))})) |