Metamath Proof Explorer


Theorem paddfval

Description: Projective subspace sum operation. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses paddfval.l = ( le ‘ 𝐾 )
paddfval.j = ( join ‘ 𝐾 )
paddfval.a 𝐴 = ( Atoms ‘ 𝐾 )
paddfval.p + = ( +𝑃𝐾 )
Assertion paddfval ( 𝐾𝐵+ = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚𝑛 ) ∪ { 𝑝𝐴 ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( 𝑞 𝑟 ) } ) ) )

Proof

Step Hyp Ref Expression
1 paddfval.l = ( le ‘ 𝐾 )
2 paddfval.j = ( join ‘ 𝐾 )
3 paddfval.a 𝐴 = ( Atoms ‘ 𝐾 )
4 paddfval.p + = ( +𝑃𝐾 )
5 elex ( 𝐾𝐵𝐾 ∈ V )
6 fveq2 ( = 𝐾 → ( Atoms ‘ ) = ( Atoms ‘ 𝐾 ) )
7 6 3 eqtr4di ( = 𝐾 → ( Atoms ‘ ) = 𝐴 )
8 7 pweqd ( = 𝐾 → 𝒫 ( Atoms ‘ ) = 𝒫 𝐴 )
9 eqidd ( = 𝐾𝑝 = 𝑝 )
10 fveq2 ( = 𝐾 → ( le ‘ ) = ( le ‘ 𝐾 ) )
11 10 1 eqtr4di ( = 𝐾 → ( le ‘ ) = )
12 fveq2 ( = 𝐾 → ( join ‘ ) = ( join ‘ 𝐾 ) )
13 12 2 eqtr4di ( = 𝐾 → ( join ‘ ) = )
14 13 oveqd ( = 𝐾 → ( 𝑞 ( join ‘ ) 𝑟 ) = ( 𝑞 𝑟 ) )
15 9 11 14 breq123d ( = 𝐾 → ( 𝑝 ( le ‘ ) ( 𝑞 ( join ‘ ) 𝑟 ) ↔ 𝑝 ( 𝑞 𝑟 ) ) )
16 15 2rexbidv ( = 𝐾 → ( ∃ 𝑞𝑚𝑟𝑛 𝑝 ( le ‘ ) ( 𝑞 ( join ‘ ) 𝑟 ) ↔ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( 𝑞 𝑟 ) ) )
17 7 16 rabeqbidv ( = 𝐾 → { 𝑝 ∈ ( Atoms ‘ ) ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( le ‘ ) ( 𝑞 ( join ‘ ) 𝑟 ) } = { 𝑝𝐴 ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( 𝑞 𝑟 ) } )
18 17 uneq2d ( = 𝐾 → ( ( 𝑚𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ ) ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( le ‘ ) ( 𝑞 ( join ‘ ) 𝑟 ) } ) = ( ( 𝑚𝑛 ) ∪ { 𝑝𝐴 ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( 𝑞 𝑟 ) } ) )
19 8 8 18 mpoeq123dv ( = 𝐾 → ( 𝑚 ∈ 𝒫 ( Atoms ‘ ) , 𝑛 ∈ 𝒫 ( Atoms ‘ ) ↦ ( ( 𝑚𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ ) ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( le ‘ ) ( 𝑞 ( join ‘ ) 𝑟 ) } ) ) = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚𝑛 ) ∪ { 𝑝𝐴 ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( 𝑞 𝑟 ) } ) ) )
20 df-padd +𝑃 = ( ∈ V ↦ ( 𝑚 ∈ 𝒫 ( Atoms ‘ ) , 𝑛 ∈ 𝒫 ( Atoms ‘ ) ↦ ( ( 𝑚𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ ) ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( le ‘ ) ( 𝑞 ( join ‘ ) 𝑟 ) } ) ) )
21 3 fvexi 𝐴 ∈ V
22 21 pwex 𝒫 𝐴 ∈ V
23 22 22 mpoex ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚𝑛 ) ∪ { 𝑝𝐴 ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( 𝑞 𝑟 ) } ) ) ∈ V
24 19 20 23 fvmpt ( 𝐾 ∈ V → ( +𝑃𝐾 ) = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚𝑛 ) ∪ { 𝑝𝐴 ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( 𝑞 𝑟 ) } ) ) )
25 4 24 syl5eq ( 𝐾 ∈ V → + = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚𝑛 ) ∪ { 𝑝𝐴 ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( 𝑞 𝑟 ) } ) ) )
26 5 25 syl ( 𝐾𝐵+ = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚𝑛 ) ∪ { 𝑝𝐴 ∣ ∃ 𝑞𝑚𝑟𝑛 𝑝 ( 𝑞 𝑟 ) } ) ) )