Metamath Proof Explorer

Theorem paddcom

Description: Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012)

Ref Expression
Hypotheses padd0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
padd0.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddcom ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 padd0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 padd0.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 uncom ⊢ ( 𝑋 ∪ 𝑌 ) = ( 𝑌 ∪ 𝑋 )
4 3 a1i ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 ∪ 𝑌 ) = ( 𝑌 ∪ 𝑋 ) )
5 simpl1 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → 𝐾 ∈ Lat )
6 simpl2 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → 𝑋 ⊆ 𝐴 )
7 simprl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → 𝑞 ∈ 𝑋 )
8 6 7 sseldd ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → 𝑞 ∈ 𝐴 )
9 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 1 atbase ⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ ( Base ‘ 𝐾 ) )
11 8 10 syl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
12 simpl3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → 𝑌 ⊆ 𝐴 )
13 simprr ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → 𝑟 ∈ 𝑌 )
14 12 13 sseldd ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → 𝑟 ∈ 𝐴 )
15 9 1 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ ( Base ‘ 𝐾 ) )
16 14 15 syl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
17 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
18 9 17 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) = ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) )
19 5 11 16 18 syl3anc ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) = ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) )
20 19 breq2d ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) ) )
21 20 2rexbidva ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) ) )
22 rexcom ⊢ ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) ↔ ∃ 𝑟 ∈ 𝑌 ∃ 𝑞 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) )
23 21 22 bitrdi ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑌 ∃ 𝑞 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) ) )
24 23 rabbidv ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } = { 𝑝 ∈ 𝐴 ∣ ∃ 𝑟 ∈ 𝑌 ∃ 𝑞 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) } )
25 4 24 uneq12d ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) = ( ( 𝑌 ∪ 𝑋 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑟 ∈ 𝑌 ∃ 𝑞 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) } ) )
26 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
27 26 17 1 2 paddval ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) )
28 26 17 1 2 paddval ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑌 + 𝑋 ) = ( ( 𝑌 ∪ 𝑋 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑟 ∈ 𝑌 ∃ 𝑞 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) } ) )
29 28 3com23 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑌 + 𝑋 ) = ( ( 𝑌 ∪ 𝑋 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑟 ∈ 𝑌 ∃ 𝑞 ∈ 𝑋 𝑝 ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) 𝑞 ) } ) )
30 25 27 29 3eqtr4d ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )