Metamath Proof Explorer

Theorem pj1fval

Description: The left projection function (for a direct product of group subspaces). (Contributed by Mario Carneiro, 15-Oct-2015) (Revised by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses pj1fval.v ⊢ 𝐵 = ( Base ‘ 𝐺 )
pj1fval.a ⊢ + = ( +g ‘ 𝐺 )
pj1fval.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
pj1fval.p ⊢ 𝑃 = ( proj1 ‘ 𝐺 )
Assertion pj1fval ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 𝑃 𝑈 ) = ( 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 pj1fval.v ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 pj1fval.a ⊢ + = ( +g ‘ 𝐺 )
3 pj1fval.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
4 pj1fval.p ⊢ 𝑃 = ( proj1 ‘ 𝐺 )
5 elex ⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V )
6 5 3ad2ant1 ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → 𝐺 ∈ V )
7 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
8 7 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝐵 )
9 8 pweqd ⊢ ( 𝑔 = 𝐺 → 𝒫 ( Base ‘ 𝑔 ) = 𝒫 𝐵 )
10 fveq2 ⊢ ( 𝑔 = 𝐺 → ( LSSum ‘ 𝑔 ) = ( LSSum ‘ 𝐺 ) )
11 10 3 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( LSSum ‘ 𝑔 ) = ⊕ )
12 11 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑡 ( LSSum ‘ 𝑔 ) 𝑢 ) = ( 𝑡 ⊕ 𝑢 ) )
13 fveq2 ⊢ ( 𝑔 = 𝐺 → ( +g ‘ 𝑔 ) = ( +g ‘ 𝐺 ) )
14 13 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( +g ‘ 𝑔 ) = + )
15 14 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
16 15 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑧 = ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ↔ 𝑧 = ( 𝑥 + 𝑦 ) ) )
17 16 rexbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ) )
18 17 riotabidv ⊢ ( 𝑔 = 𝐺 → ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ) = ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ) )
19 12 18 mpteq12dv ⊢ ( 𝑔 = 𝐺 → ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑔 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝑡 ⊕ 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ) ) )
20 9 9 19 mpoeq123dv ⊢ ( 𝑔 = 𝐺 → ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑔 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑔 ) ↦ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑔 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ) ) ) = ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ( 𝑧 ∈ ( 𝑡 ⊕ 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ) ) ) )
21 df-pj1 ⊢ proj1 = ( 𝑔 ∈ V ↦ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑔 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑔 ) ↦ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑔 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ) ) ) )
22 1 fvexi ⊢ 𝐵 ∈ V
23 22 pwex ⊢ 𝒫 𝐵 ∈ V
24 23 23 mpoex ⊢ ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ( 𝑧 ∈ ( 𝑡 ⊕ 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ) ) ) ∈ V
25 20 21 24 fvmpt ⊢ ( 𝐺 ∈ V → ( proj1 ‘ 𝐺 ) = ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ( 𝑧 ∈ ( 𝑡 ⊕ 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ) ) ) )
26 6 25 syl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( proj1 ‘ 𝐺 ) = ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ( 𝑧 ∈ ( 𝑡 ⊕ 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ) ) ) )
27 4 26 syl5eq ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → 𝑃 = ( 𝑡 ∈ 𝒫 𝐵 , 𝑢 ∈ 𝒫 𝐵 ↦ ( 𝑧 ∈ ( 𝑡 ⊕ 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ) ) ) )
28 oveq12 ⊢ ( ( 𝑡 = 𝑇 ∧ 𝑢 = 𝑈 ) → ( 𝑡 ⊕ 𝑢 ) = ( 𝑇 ⊕ 𝑈 ) )
29 28 adantl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑡 = 𝑇 ∧ 𝑢 = 𝑈 ) ) → ( 𝑡 ⊕ 𝑢 ) = ( 𝑇 ⊕ 𝑈 ) )
30 simprl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑡 = 𝑇 ∧ 𝑢 = 𝑈 ) ) → 𝑡 = 𝑇 )
31 simprr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑡 = 𝑇 ∧ 𝑢 = 𝑈 ) ) → 𝑢 = 𝑈 )
32 31 rexeqdv ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑡 = 𝑇 ∧ 𝑢 = 𝑈 ) ) → ( ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) )
33 30 32 riotaeqbidv ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑡 = 𝑇 ∧ 𝑢 = 𝑈 ) ) → ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ) = ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) )
34 29 33 mpteq12dv ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑡 = 𝑇 ∧ 𝑢 = 𝑈 ) ) → ( 𝑧 ∈ ( 𝑡 ⊕ 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 + 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ) )
35 simp2 ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → 𝑇 ⊆ 𝐵 )
36 22 elpw2 ⊢ ( 𝑇 ∈ 𝒫 𝐵 ↔ 𝑇 ⊆ 𝐵 )
37 35 36 sylibr ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → 𝑇 ∈ 𝒫 𝐵 )
38 simp3 ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → 𝑈 ⊆ 𝐵 )
39 22 elpw2 ⊢ ( 𝑈 ∈ 𝒫 𝐵 ↔ 𝑈 ⊆ 𝐵 )
40 38 39 sylibr ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → 𝑈 ∈ 𝒫 𝐵 )
41 ovex ⊢ ( 𝑇 ⊕ 𝑈 ) ∈ V
42 41 mptex ⊢ ( 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ) ∈ V
43 42 a1i ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ) ∈ V )
44 27 34 37 40 43 ovmpod ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 𝑃 𝑈 ) = ( 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ( ℩ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 𝑧 = ( 𝑥 + 𝑦 ) ) ) )