Metamath Proof Explorer

Theorem dsmmval2

Description: Self-referential definition of the module direct sum. (Contributed by Stefan O'Rear, 7-Jan-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypothesis dsmmval2.b ⊢ 𝐵 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
Assertion dsmmval2 ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 )

Proof

Step Hyp Ref Expression
1 dsmmval2.b ⊢ 𝐵 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
2 ssrab2 ⊢ { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } ⊆ ( Base ‘ ( 𝑆 Xs 𝑅 ) )
3 eqid ⊢ ( ( 𝑆 Xs 𝑅 ) ↾s { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } ) = ( ( 𝑆 Xs 𝑅 ) ↾s { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } )
4 eqid ⊢ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) )
5 3 4 ressbas2 ⊢ ( { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } ⊆ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) → { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } = ( Base ‘ ( ( 𝑆 Xs 𝑅 ) ↾s { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } ) ) )
6 2 5 ax-mp ⊢ { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } = ( Base ‘ ( ( 𝑆 Xs 𝑅 ) ↾s { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } ) )
7 6 oveq2i ⊢ ( ( 𝑆 Xs 𝑅 ) ↾s { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } ) = ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( ( 𝑆 Xs 𝑅 ) ↾s { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } ) ) )
8 eqid ⊢ { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin }
9 8 dsmmval ⊢ ( 𝑅 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } ) )
10 9 fveq2d ⊢ ( 𝑅 ∈ V → ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) = ( Base ‘ ( ( 𝑆 Xs 𝑅 ) ↾s { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } ) ) )
11 10 oveq2d ⊢ ( 𝑅 ∈ V → ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ) = ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( ( 𝑆 Xs 𝑅 ) ↾s { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } ) ) ) )
12 7 9 11 3eqtr4a ⊢ ( 𝑅 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ) )
13 ress0 ⊢ ( ∅ ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ) = ∅
14 13 eqcomi ⊢ ∅ = ( ∅ ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
15 reldmdsmm ⊢ Rel dom ⊕m
16 15 ovprc2 ⊢ ( ¬ 𝑅 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ∅ )
17 reldmprds ⊢ Rel dom Xs
18 17 ovprc2 ⊢ ( ¬ 𝑅 ∈ V → ( 𝑆 Xs 𝑅 ) = ∅ )
19 18 oveq1d ⊢ ( ¬ 𝑅 ∈ V → ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ) = ( ∅ ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ) )
20 14 16 19 3eqtr4a ⊢ ( ¬ 𝑅 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ) )
21 12 20 pm2.61i ⊢ ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
22 1 oveq2i ⊢ ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) = ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
23 21 22 eqtr4i ⊢ ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 )